Lean 4.19

1 files changed, 3 insertions, 3 deletions

diff --git a/Day10.lean b/Day10.lean
index d9a72f6..327bdb2 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -515,7 +515,7 @@ private theorem Area.ParseLine_start_at_tile (previous : Area.Raw) (pos : Nat) (
             split at h₄; contradiction
             case isFalse h₇ =>
               have h₈ : (previous.fields.push t)[previous.width * (previous.height - 1) + pos]! = t := by
-                have := Array.getElem_push_eq previous.fields t
+                have : (previous.fields.push t)[previous.fields.size] = t := Array.getElem_push_eq
                 simp[h₂, Array.getElem!_eq_getElem] at this
                 assumption
               have : t = Tile.start := beq_iff_eq.mp h₆
@@ -1060,7 +1060,7 @@ private theorem Area.PathsPart.tail_connect_start {area : Area} (pp : area.Paths
   match hs : pp.steps, pp.list_not_empty, pp.connected with
   | _ :: [], _, h₁ => h₁
   | s :: ss :: sss, _, ⟨_,h₂⟩ =>
-    have : (ss :: sss).length < pp.steps.length := hs.substr $ (List.length_cons s (ss :: sss)).substr $ Nat.lt.base (ss :: sss).length
+    have : (ss :: sss).length < pp.steps.length := hs.substr $ (List.length_cons).substr $ Nat.lt.base (ss :: sss).length
     Area.PathsPart.tail_connect_start ⟨ss::sss,h₂⟩
 termination_by pp.steps.length
 
@@ -1558,7 +1558,7 @@ where
         let ⟨(_ : t ≠ Tile.ground), (_ : t ≠ Tile.start)⟩ := Area.can_connect_to_imp_not_start_not_ground s_connects_to_ss.left
         match t with
         | Tile.pipe p =>
-          have : (ss :: sss).length < pp.steps.length := hs.substr $ (List.length_cons s (ss :: sss)).substr $ Nat.lt_add_one (ss :: sss).length
+          have : (ss :: sss).length < pp.steps.length := hs.substr $ (List.length_cons).substr $ Nat.lt_add_one (ss :: sss).length
           worker { steps := ss :: sss, connected := rest_is_connected } $ {coordinate := s, pipe :=p} :: o
       termination_by x => x.steps.length
     worker cp.toPathsPart []