Lean 4.18

1 files changed, 0 insertions, 2 deletions

diff --git a/Day16.lean b/Day16.lean
index 7e5d3a9..8bd4bf8 100644
--- a/Day16.lean
+++ b/Day16.lean
@@ -170,8 +170,6 @@ private theorem SeenExitDirection.setDirection_increasesCountDirection (a : Seen
     unfold contains at h₁
     simp[countDirection, setDirection, setTop, setLeft, setRight, setBottom, left, right, bottom, top] at h₁ ⊢
     simp[h₁, BitVec.setBitTrue, Fin.val_three]
-    unfold getElem BitVec.instGetElemNatBoolLt BitVec.getLsb' Nat.testBit
-    simp
 
 private structure SeenExitDirections (table : OpticsTable) extends Parsing.RectangularGrid SeenExitDirection where
   sameWidth : width = table.width