Lean 4.23

1 files changed, 7 insertions, 8 deletions

diff --git a/Day10.lean b/Day10.lean
index 6787658..c95ad12 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -266,7 +266,7 @@ private theorem Area.ParseLine_adds_returned_count (previous : Area.Raw) (pos :
       unfold bind Monad.toBind Except.instMonad at h₃
       simp at h₃
       cases h₄ : (Day10.Area.parseLine.parseCharacter line.front)
-      <;> simp[h₄, Option.toExcept, Except.bind] at h₃
+      <;> simp[h₄, Except.bind] at h₃
       case error => rw[←h₃] at h₂; contradiction
       case ok =>
         split at h₃
@@ -318,7 +318,7 @@ private theorem Area.ParseLine_leaves_width_and_height (previous : Area.Raw) (po
       unfold bind Monad.toBind Except.instMonad at h₃
       simp at h₃
       cases h₄ : (Day10.Area.parseLine.parseCharacter line.front)
-      <;> simp[h₄, Option.toExcept, Except.bind] at h₃
+      <;> simp[h₄, Except.bind] at h₃
       case error => rw[←h₃] at h₂; contradiction
       case ok =>
         split at h₃
@@ -448,7 +448,7 @@ private theorem Array.get_push {α : Type u} (arr : Array α) (v : α) (index :
   cases arr
   unfold Array.push getElem Array.instGetElemNatLtSize
   simp only [List.size_toArray] at h₁
-  simp[List.getElem_append, h₁]
+  simp[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
   unfold Area.parseLine at h₂
@@ -488,7 +488,6 @@ private theorem Area.ParseLine_only_adds_to_fields (previous : Area.Raw) (pos :
           simp at h₅
           rw[←h₅]
           have h₆ : ↑index < (previous.fields.push tile).size := by simp; exact Nat.lt_succ.mpr (Nat.le_of_lt index.isLt)
-          simp[←Array.getElem!_eq_getElem]
           simp[←Array.getElem!_eq_getElem h₆]
           apply Array.get_push
 termination_by previous.width - pos
@@ -682,7 +681,7 @@ private def Area.parse (input : String) : Except Area.ParseError Area :=
         rw[Except.get_unfold']
         exact he
       have sp : vraw.fields[(Coordinate.fromIndex s).toIndex] = Tile.start := by
-        simp[Except.get_unfold' he except_ok] at sp
+        simp at sp
         simp[Coordinate.toIndex_inv_fromIndex]
         rw[Array.getElem!_eq_getElem] at sp ⊢
         have : ((Day10.Except.get (Day10.Area.parseRaw input) _).start.get is_some).val = s.val := by
@@ -1286,13 +1285,13 @@ private theorem Area.PathsPart.join_a_last_last (a b : area.PathsPart) (h₁ : a
   generalize h₂ : (Day10.Area.PathsPart.join area a b h₁) = o
   unfold Area.PathsPart.join at h₂
   split at h₂
-  case h_1 bh ah as _ _ h₄ h₃ _ _ _ _ hb ha _ _ _ _ =>
-    simp[hb, ←h₂, ←ha]
+  case h_1 bh ah as _ _ h₄ h₃ _ _ _ _ _ ha _ _ _ _ =>
+    simp[←h₂, ←ha]
     apply List.getLast_cons
   case h_2 bh b1 bs ah as _ _ h₄ h₃ d4 d3 d2 d1 hb ha d5 d6 d7 d8 =>
     clear d1 d2 d3 d4 d5 d6 d7 d8
     simp only at h₂
-    simp[hb, ←h₂, ←ha]
+    simp[←h₂, ←ha]
     rw[←List.getLast_cons (a := bh) a.list_not_empty]
     have : bs.length + 1 < b.steps.length := by simp only [hb, List.length_cons, Nat.lt_add_one]
     apply Area.PathsPart.join_a_last_last