From 2a9261d1ba962deff9fcc1784be44563af513af5 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 10 Oct 2025 00:30:19 +0200
Subject: Lean 4.18

---
 Day16.lean | 2 --
 1 file changed, 2 deletions(-)

(limited to 'Day16.lean')

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
-- 
cgit v1.2.3