From 6aaa70943202efaa1e6b4ff8b6b8b6b94a564040 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 12 Oct 2025 18:44:32 +0200
Subject: Lean 4.19

---
 Day13.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Day13.lean')

diff --git a/Day13.lean b/Day13.lean
index 25f1f37..a17b602 100644
--- a/Day13.lean
+++ b/Day13.lean
@@ -62,7 +62,7 @@ match parse input with
       cases List.mapM' (Parsing.RectangularGrid.ofSubstring Day13.Tile.ofChar?) bs
       case error e => exact True.intro
       case ok ts =>
-        have h₄ := List.length_cons t ts
+        have h₄ : (t :: ts).length = ts.length + 1 := List.length_cons
         unfold bind Monad.toBind Except.instMonad
         simp only [Except.bind, Except.map, h₄, Nat.zero_lt_succ]
 
-- 
cgit v1.2.3