From 6aaa70943202efaa1e6b4ff8b6b8b6b94a564040 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 12 Oct 2025 18:44:32 +0200 Subject: Lean 4.19 --- Day10.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Day10.lean') 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 [] -- cgit v1.2.3