From 4fbeb023e0b2c58895e8df8d169035e274159537 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 2 Nov 2025 17:52:59 +0100
Subject: Lean 4.21

---
 Day10.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'Day10.lean')

diff --git a/Day10.lean b/Day10.lean
index cea307b..6787658 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -440,13 +440,14 @@ private theorem Except.get_pure {α : Type u1} (ε : Type u2) (v : α) : Except.
 
 private theorem Array.getElem!_eq_getElem {α : Type u} [Inhabited α] {a : Array α} {index : Nat} (h : index < a.size ): a[index] = a[index]! := by
   unfold getElem getElem! Array.instGetElemNatLtSize Array.instGetElem?NatLtSize Array.get!Internal Array.getInternal Array.getD
-  simp
+  simp only
   split
   <;> rfl
 
 private theorem Array.get_push {α : Type u} (arr : Array α) (v : α) (index : Nat) (h₁ : index < arr.size) : arr[index] = (arr.push v)[index]'(by simp[Nat.lt_succ.mpr (Nat.le_of_lt h₁)]) := by
   cases arr
   unfold Array.push getElem Array.instGetElemNatLtSize
+  simp only [List.size_toArray] at h₁
   simp[List.getElem_append, h₁]
 
 private theorem Area.ParseLine_leaves_start_if_some (previous : Area.Raw) (pos : Nat) (line : Substring) (h₁ : previous.height > 0) {res : (Nat × Area.Raw)} (h₂ : (Area.parseLine previous pos line h₁) = Except.ok res) (h₃ : previous.start.isSome) : Fin.val <$> res.2.start = Fin.val <$> previous.start := by
@@ -516,7 +517,8 @@ private theorem Area.ParseLine_start_at_tile (previous : Area.Raw) (pos : Nat) (
             case isFalse h₇ =>
               have h₈ : (previous.fields.push t)[previous.width * (previous.height - 1) + pos]! = t := by
                 have : (previous.fields.push t)[previous.fields.size] = t := Array.getElem_push_eq
-                simp[h₂, Array.getElem!_eq_getElem] at this
+                simp[h₂] at this
+                rw[Array.getElem!_eq_getElem] at this
                 assumption
               have : t = Tile.start := beq_iff_eq.mp h₆
               subst t
-- 
cgit v1.2.3

