Lean 4.18

1 files changed, 9 insertions, 7 deletions

diff --git a/Day10.lean b/Day10.lean
index fe61825..d9a72f6 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -439,16 +439,14 @@ private theorem Except.get_unfold' {α : Type u1} {ε : Type u2} {e : Except ε
 private theorem Except.get_pure {α : Type u1} (ε : Type u2) (v : α) : Except.get (α := α) (ε := ε) (pure v) (rfl) = v := rfl
 
 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! instGetElem?OfGetElemOfDecidable Array.instGetElemNatLtSize decidableGetElem?
+  unfold getElem getElem! Array.instGetElemNatLtSize Array.instGetElem?NatLtSize Array.get!Internal Array.getInternal Array.getD
   simp
   split
-  <;> rename_i blah
-  <;> simp[h] at blah
-  assumption
+  <;> 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 Array.get
+  unfold Array.push getElem Array.instGetElemNatLtSize
   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
@@ -537,7 +535,7 @@ private theorem Area.ParseLine_start_at_tile (previous : Area.Raw) (pos : Nat) (
               simp[←h₉]
               assumption
           case isFalse =>
-            have : (previous.fields.push t).size = previous.width * (previous.height - 1) + (pos + 1) := by simp_arith[h₂]
+            have : (previous.fields.push t).size = previous.width * (previous.height - 1) + (pos + 1) := by simp +arith[h₂]
             have h₆ := Area.ParseLine_start_at_tile { width := previous.width, height := previous.height, start := previous.start, fields := previous.fields.push t } (pos + 1) (line.drop 1) h₁ this h₃ h₄
             simp[hindex] at h₆
             assumption
@@ -630,7 +628,7 @@ private theorem Area.ParseRaw_start_position_aux :
       case isFalse => rw[←hr] at h₁; contradiction
       case isTrue =>
         rename_i hs _
-        have : 0 < (String.splitTrim (fun x => x == '\n') input.trim).length := by let hs := List.isEmpty_eq_false.mpr hs; unfold List.isEmpty at hs; split at hs; contradiction; rename_i hx; simp[hx]
+        have : 0 < (String.splitTrim (fun x => x == '\n') input.trim).length := by let hs := List.isEmpty_eq_false_iff.mpr hs; unfold List.isEmpty at hs; split at hs; contradiction; rename_i hx; simp[hx]
         have := Area.ParseLines_start_position { width := (String.splitTrim (fun x => x == '\n') input.trim)[0].length, height := 0, start := none, fields := #[] } (String.splitTrim (fun x => x == '\n') input.trim) (hr.substr h₁)
         simp at this
         subst r
@@ -1007,7 +1005,11 @@ private def removePathsMet {area : Area} : (List $ Area.PathHead area) → (List
 termination_by x => x.length
 decreasing_by
   all_goals
+    rw[List.unattach_filter (g := λs ↦ s.current ≠ p.current)]
+    simp
     exact Nat.lt_succ.mpr $ List.listFilterSmallerOrEqualList _ _
+    intros x xe
+    simp
 
 
 private def noSolution {area : Area} : (List $ Area.PathHead area) → Bool