From 6d10b7594f487bdfbef99d05bda34405dd85c8b8 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 16 Nov 2025 14:24:46 +0100
Subject: Lean 4.23

---
 Day16.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Day16.lean')

diff --git a/Day16.lean b/Day16.lean
index abefc51..3777521 100644
--- a/Day16.lean
+++ b/Day16.lean
@@ -300,7 +300,7 @@ private theorem OpticsTable.findFirstExitDirectionNotSeenInQueue_notContains {ta
       have h₂ := Option.some.inj h₁
       subst result
       generalize { x := Fin.cast _ b.snd.x, y := Fin.cast _ b.snd.y : seenDirections.Coordinate } = c at *
-      have h₂ : ed ∈ List.filter (fun d => !seenDirections.toRectangularGrid[c].contains d) (OpticsElement.outputDirections table[b.snd] b.fst) := by simp only [heq, List.mem_singleton, List.mem_cons, true_or]
+      have h₂ : ed ∈ List.filter (fun d => !seenDirections.toRectangularGrid[c].contains d) (OpticsElement.outputDirections table[b.snd] b.fst) := by simp only [heq, List.mem_cons, true_or]
       exact (Bool.not_eq_true' _).mp (List.mem_filter.mp h₂).right
 
 private def OpticsTable.followPath {table : OpticsTable} (seenDirections : SeenExitDirections table) (beams : List (EnterDirection × table.Coordinate)) : SeenExitDirections table :=
-- 
cgit v1.2.3

