diff options
Diffstat (limited to 'Day16.lean')
| -rw-r--r-- | Day16.lean | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 := |