From 6d10b7594f487bdfbef99d05bda34405dd85c8b8 Mon Sep 17 00:00:00 2001 From: Andreas Grois 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