Lean 4.20.1

1 files changed, 4 insertions, 7 deletions

diff --git a/Day10.lean b/Day10.lean
index 327bdb2..cea307b 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -1099,28 +1099,28 @@ private def Area.Paths.fromPathStarts {area : Area} (starts : Area.PathStarts ar
     west := starts.west.map λ ⟨c, ⟨h₁, _⟩⟩ ↦ toPathsPart c h₁
     north_valid := λn h₁ ↦ by
       have : (starts.north.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨n,h₁⟩).symm).symm).fst.current = n.steps.getLast n.list_not_empty :=
-        let ⟨w, h₁⟩ := Option.map_eq_some'.mp h₁
+        let ⟨w, h₁⟩ := Option.map_eq_some_iff.mp h₁
         by simp only [toPathsPart, h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton]
       have h₂ := (starts.north.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨n,h₁⟩).symm).symm).snd.snd
       simp[this] at h₂
       assumption
     east_valid := λe h₁ ↦ by
       have : (starts.east.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨e,h₁⟩).symm).symm).fst.current = e.steps.getLast e.list_not_empty :=
-        let ⟨w, h₁⟩ := Option.map_eq_some'.mp h₁
+        let ⟨w, h₁⟩ := Option.map_eq_some_iff.mp h₁
         by simp only [toPathsPart, h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton]
       have h₂ := (starts.east.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨e,h₁⟩).symm).symm).snd.snd
       simp[this] at h₂
       assumption
     south_valid := λs h₁ ↦ by
       have : (starts.south.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨s,h₁⟩).symm).symm).fst.current = s.steps.getLast s.list_not_empty :=
-        let ⟨w, h₁⟩ := Option.map_eq_some'.mp h₁
+        let ⟨w, h₁⟩ := Option.map_eq_some_iff.mp h₁
         by simp only [toPathsPart, h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton]
       have h₂ := (starts.south.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨s,h₁⟩).symm).symm).snd.snd
       simp[this] at h₂
       assumption
     west_valid := λw h₁ ↦ by
       have : (starts.west.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨w,h₁⟩).symm).symm).fst.current = w.steps.getLast w.list_not_empty :=
-        let ⟨w, h₁⟩ := Option.map_eq_some'.mp h₁
+        let ⟨w, h₁⟩ := Option.map_eq_some_iff.mp h₁
         by simp only [toPathsPart, h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton]
       have h₂ := (starts.west.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨w,h₁⟩).symm).symm).snd.snd
       simp[this] at h₂
@@ -1275,9 +1275,6 @@ private theorem Area.PathsPart.join_b_last_head (a b : area.PathsPart) (h₁ : a
     clear d1 d2 d3 d4 d5 d6 d7 d8
     simp only at h₂
     simp[hb]
-    have : ∀ g₁ g₂, (bh :: b1 ::bs).getLast g₁ = (b1 :: bs).getLast g₂ := by intros; exact List.getLast_cons (by simp : b1 :: bs ≠ [])
-    rw[this]
-    case g₂ => simp
     subst o
     have : bs.length + 1 < b.steps.length := by simp only [hb, List.length_cons, Nat.lt_add_one]
     apply Area.PathsPart.join_b_last_head