1 files changed, 1 insertions, 1 deletions
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]