diff options
Diffstat (limited to 'Day10.lean')
| -rw-r--r-- | Day10.lean | 11 |
1 files changed, 4 insertions, 7 deletions
@@ -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 |