Lean 4.23

1 files changed, 1 insertions, 1 deletions

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 :=