diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean
index 63c75a12..beeeaf67 100644
--- a/SphereEversion/Global/Gromov.lean
+++ b/SphereEversion/Global/Gromov.lean
@@ -149,7 +149,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R
       · calc
           dist (F' t x).1.2 (𝓕₀.bs x) ≤ dist (F' t x).1.2 (F.bs x) + dist (F.bs x) (𝓕₀.bs x) :=
             dist_triangle _ _ _
-          _ < η x + dist (F.bs x) (𝓕₀.bs x) := (add_lt_add_right (hF'η t x) _)
+          _ < η x + dist (F.bs x) (𝓕₀.bs x) := (add_lt_add_left (hF'η t x) _)
           _ = τ x := by simp [F, η]
     · rw [union_assoc, Eventually.union_nhdsSet, image_preimage_eq_of_subset K₀φ] at hF'hol
       exact hF'hol.2
diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean
index 96be287a..12c62401 100644
--- a/SphereEversion/Global/Relation.lean
+++ b/SphereEversion/Global/Relation.lean
@@ -469,7 +469,6 @@ theorem OpenSmoothEmbedding.smooth_transfer :
   intro x
   refine ContMDiffAt.oneJetBundle_map (φ.contMDiff_to.contMDiffAt.comp _ contMDiffAt_snd)
      (ψ.contMDiff_to.contMDiffAt.comp _ contMDiffAt_snd) ?_ contMDiffAt_id
-
   have' :=
     ContMDiffAt.mfderiv (fun _ ↦ φ.invFun) (fun x : OneJetBundle IX X IY Y ↦ φ x.1.1)
       ((φ.contMDiffAt_inv <| _).comp (x, φ x.1.1) contMDiffAt_snd)
diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean
index f0570a6a..998e1e25 100644
--- a/SphereEversion/Indexing.lean
+++ b/SphereEversion/Indexing.lean
@@ -135,7 +135,7 @@ theorem IndexType.induction_from {P : IndexType n → Prop} {i₀ : IndexType n}
     rw [← IndexType.succ_castSuccEmb]
     refine ih _ ?_ ?_ ?_
     · rwa [ge_iff_le, le_castSucc_iff]
-    · exact not_isMax_of_lt (castSucc_lt_succ i)
+    · exact not_isMax_of_lt castSucc_lt_succ
     · apply hi; rwa [ge_iff_le, le_castSucc_iff]
 
 @[elab_as_elim]
@@ -166,7 +166,7 @@ theorem IndexType.exists_by_induction {α : Type*} (P : IndexType n → α → P
       refine fun i ↦ Fin.induction hf₀ ?_ i
       intro i hi
       simp_rw [f, induction_succ, ← IndexType.succ_castSuccEmb]
-      exact hF _ _ hi (not_isMax_of_lt (castSucc_lt_succ i))
+      exact hF _ _ hi (not_isMax_of_lt castSucc_lt_succ)
     refine ⟨f, fun i ↦ ⟨key i, fun hi ↦ ?_⟩⟩
     convert hF' _ _ (key i) hi
     rcases i.exists_castSucc_eq hi with ⟨i, rfl⟩
diff --git a/SphereEversion/Local/Corrugation.lean b/SphereEversion/Local/Corrugation.lean
index 44506916..9c66ba21 100644
--- a/SphereEversion/Local/Corrugation.lean
+++ b/SphereEversion/Local/Corrugation.lean
@@ -168,7 +168,7 @@ theorem corrugation.fderiv_eq {N : ℝ} (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ)
   erw [fderiv_const_smul key.differentiableAt, key.fderiv, smul_add, add_comm]
   congr 1
   rw [fderiv_fun_const_smul (hπ_diff.differentiable le_rfl).differentiableAt N, π.fderiv]
-  simp only [smul_smul, inv_mul_cancel₀ hN, one_div, Algebra.id.smul_eq_mul, one_smul,
+  simp only [smul_smul, inv_mul_cancel₀ hN, one_div, smul_eq_mul, one_smul,
     ContinuousLinearMap.comp_smul]
 
 theorem corrugation.fderiv_apply (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) (x v : E) :
diff --git a/SphereEversion/Local/DualPair.lean b/SphereEversion/Local/DualPair.lean
index dd173032..7ac983ac 100644
--- a/SphereEversion/Local/DualPair.lean
+++ b/SphereEversion/Local/DualPair.lean
@@ -109,7 +109,7 @@ theorem inf_eq_bot (p : DualPair E) : ker p.π ⊓ p.spanV = ⊥ := bot_unique <
   have : p.π x = 0 ∧ ∃ a : ℝ, a • p.v = x := by
     simpa [DualPair.spanV, Submodule.mem_span_singleton] using hx
   rcases this with ⟨H, t, rfl⟩
-  rw [p.π.map_smul, p.pairing, Algebra.id.smul_eq_mul, mul_one] at H
+  rw [p.π.map_smul, p.pairing, smul_eq_mul, mul_one] at H
   simp [H]
 
 theorem sup_eq_top (p : DualPair E) : ker p.π ⊔ p.spanV = ⊤ := by
diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean
index e2e9d156..f89612ec 100644
--- a/SphereEversion/Loops/Basic.lean
+++ b/SphereEversion/Loops/Basic.lean
@@ -209,7 +209,7 @@ theorem range_ofPath {x : X} (γ : Path x x) : range (ofPath γ) = range γ := b
       rw [fract_eq_iff]
       refine ⟨t.2.1, t.2.2.lt_of_ne ht1, ⟨0, ?_⟩⟩
       rw [Int.cast_zero, sub_self]
-    simp only [this, γ.extend_extends t.2]
+    simp only [this, γ.extend_apply t.2]
 
 /-- `Loop.ofPath` is continuous, general version. -/
 @[fun_prop]
@@ -220,7 +220,7 @@ theorem _root_.Continuous.ofPath (x : X → Y) (t : X → ℝ) (γ : ∀ i, Path
   · have : Continuous (fun x : X × ℝ ↦ (x.1, projIcc 0 1 zero_le_one x.2)) :=
       continuous_id.prodMap continuous_projIcc
     exact (hγ.comp this).continuousOn
-  · simp only [Icc.mk_zero, zero_le_one, Path.target, Path.extend_extends, imp_true_iff,
+  · simp only [Icc.mk_zero, zero_le_one, Path.target, Path.extend_apply, imp_true_iff,
       Path.source, right_mem_Icc, left_mem_Icc, Icc.mk_one]
 
 /-- `Loop.ofPath` is continuous, where the endpoints of `γ` are fixed. TODO: remove -/
@@ -273,7 +273,7 @@ theorem roundTripFamily_zero {x y : X} {γ : Path x y} :
     (roundTripFamily γ) 0 = ofPath (Path.refl x) := by
   simp only [roundTripFamily, roundTrip, Path.truncate_zero_zero, ofPath]
   congr with t
-  simp
+  simp [← Path.cast_symm, ← Path.cast_trans]
 
 theorem roundTripFamily_one {x y : X} {γ : Path x y} : (roundTripFamily γ) 1 = roundTrip γ := by
   simp only [roundTripFamily, roundTrip, Path.truncate_zero_one, ofPath]
diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean
index b64f6897..52ea713c 100644
--- a/SphereEversion/Loops/DeltaMollifier.lean
+++ b/SphereEversion/Loops/DeltaMollifier.lean
@@ -125,7 +125,7 @@ theorem ContDiff.periodize {f : ℝ → E} {n : ℕ∞} (h : ContDiff ℝ n f) (
     refine (ProperlyDiscontinuousVAdd.finite_disjoint_inter_image
       (isCompact_Icc : IsCompact <| Icc (y - 1) (y + 1)) h').subset ?_
     intro i hi
-    rw [mem_setOf_eq, ← nonempty_iff_ne_empty]
+    rw [mem_setOf_eq]
     apply Nonempty.mono _ hi
     gcongr
     · rw [show (e i : ℝ → ℝ) = VAdd.vadd i by ext x; exact add_comm x i]
diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean
index e95accbe..27800860 100644
--- a/SphereEversion/Loops/Reparametrization.lean
+++ b/SphereEversion/Loops/Reparametrization.lean
@@ -238,13 +238,14 @@ theorem approxSurroundingPointsAt_mem_affineBases (hy : y ∈ γ.localCenteringD
   (Classical.choose_spec
       (γ.approxSurroundingPointsAt_of_localCenteringDensityNhd x y hy)).mem_affineBases
 
+section DecidablePred
+
 variable [DecidablePred (· ∈ affineBases ι ℝ F)]
 
 @[simp]
 theorem localCenteringDensity_pos (hy : y ∈ γ.localCenteringDensityNhd x) (t : ℝ) :
     0 < γ.localCenteringDensity x y t := by
-  simp only [γ.localCenteringDensity_spec x, Fintype.sum_apply, Pi.smul_apply,
-    Algebra.id.smul_eq_mul]
+  simp only [γ.localCenteringDensity_spec x, Fintype.sum_apply, Pi.smul_apply, smul_eq_mul]
   refine Finset.sum_pos (fun i _ ↦ mul_pos ?_ (deltaMollifier_pos _)) Finset.univ_nonempty
   obtain ⟨w, hw⟩ := γ.approxSurroundingPointsAt_of_localCenteringDensityNhd x y hy
   convert hw.w_pos i
@@ -262,7 +263,7 @@ theorem contDiffOn_localCenteringDensity :
   let h₀ (yt : E × ℝ) (_ : yt ∈ γ.localCenteringDensityNhd x ×ˢ (univ : Set ℝ)) :=
     congr_fun (γ.localCenteringDensity_spec x yt.fst) yt.snd
   refine ContDiffOn.congr ?_ h₀
-  simp only [Fintype.sum_apply, Pi.smul_apply, Algebra.id.smul_eq_mul]
+  simp only [Fintype.sum_apply, Pi.smul_apply, smul_eq_mul]
   refine ContDiffOn.sum fun i _ ↦ ContDiffOn.mul ?_ (ContDiff.contDiffOn ?_)
   · let w : F × (ι → F) → ℝ := fun z ↦ evalBarycentricCoords ι ℝ F z.1 z.2 i
     let z : E → F × (ι → F) :=
@@ -298,13 +299,12 @@ theorem localCenteringDensity_continuous (hy : y ∈ γ.localCenteringDensityNhd
 theorem localCenteringDensity_integral_eq_one (hy : y ∈ γ.localCenteringDensityNhd x) :
     ∫ s in (0 : ℝ)..1, γ.localCenteringDensity x y s = 1 := by
   let n := γ.localCenteringDensityMp x
-  simp only [γ.localCenteringDensity_spec x, Fintype.sum_apply, Pi.smul_apply,
-    Algebra.id.smul_eq_mul]
+  simp only [γ.localCenteringDensity_spec x, Fintype.sum_apply, Pi.smul_apply, smul_eq_mul]
   rw [intervalIntegral.integral_finset_sum]
   · have h : γ.approxSurroundingPointsAt x y n ∈ affineBases ι ℝ F :=
       γ.approxSurroundingPointsAt_mem_affineBases x y hy
     simp_rw [← smul_eq_mul, intervalIntegral.integral_smul, deltaMollifier_integral_eq_one,
-      Algebra.id.smul_eq_mul, mul_one]
+      smul_eq_mul, mul_one]
     rw [evalBarycentricCoords_apply_of_mem_bases ι ℝ F (g y) h]
     simp_rw [AffineBasis.coords_apply, AffineBasis.sum_coord_apply_eq_one]
   · simp_rw [← smul_eq_mul]
@@ -315,8 +315,8 @@ theorem localCenteringDensity_integral_eq_one (hy : y ∈ γ.localCenteringDensi
 theorem localCenteringDensity_average (hy : y ∈ γ.localCenteringDensityNhd x) :
     ∫ s in (0 : ℝ)..1, γ.localCenteringDensity x y s • γ y s = g y := by
   let n := γ.localCenteringDensityMp x
-  simp only [γ.localCenteringDensity_spec x, Fintype.sum_apply, Pi.smul_apply,
-    Algebra.id.smul_eq_mul, Finset.sum_smul]
+  simp only [γ.localCenteringDensity_spec x, Fintype.sum_apply, Pi.smul_apply, smul_eq_mul,
+    Finset.sum_smul]
   rw [intervalIntegral.integral_finset_sum]
   · simp_rw [mul_smul, intervalIntegral.integral_smul]
     change ∑ i, _ • γ.approxSurroundingPointsAt x y n i = _
@@ -329,6 +329,8 @@ theorem localCenteringDensity_average (hy : y ∈ γ.localCenteringDensityNhd x)
     refine fun i hi ↦ ((Continuous.smul ?_ (γ.continuous y)).const_smul _).intervalIntegrable 0 1
     exact contDiff_deltaMollifier.continuous
 
+end DecidablePred
+
 /-- Given `γ : SmoothSurroundingFamily g`, together with a point `x : E` and a map `f : ℝ → ℝ`,
 `γ.is_centeringDensity x f` is the proposition that `f` is periodic, strictly positive, and
 has integral one and that the average of `γₓ` with respect to the measure that `f` defines on
@@ -342,7 +344,7 @@ structure IsCenteringDensity (x : E) (f : ℝ → ℝ) : Prop where
   average : ∫ s in (0 : ℝ)..1, f s • γ x s = g x
   Continuous : Continuous f
 
-omit [FiniteDimensional ℝ F] [DecidablePred fun x ↦ x ∈ affineBases ι ℝ F] in
+omit [FiniteDimensional ℝ F] in
 -- Can drop if/when have `intervalIntegrable.smul_continuous_on`
 theorem isCenteringDensity_convex (x : E) : Convex ℝ { f | γ.IsCenteringDensity x f } := by
   classical
@@ -375,8 +377,10 @@ variable [FiniteDimensional ℝ E]
 theorem exists_smooth_isCenteringDensity (x : E) :
     ∃ U ∈ 𝓝 x,
       ∃ f : E → ℝ → ℝ,
-        ContDiffOn ℝ ∞ (uncurry f) (U ×ˢ (univ : Set ℝ)) ∧ ∀ y ∈ U, γ.IsCenteringDensity y (f y) :=
-  ⟨γ.localCenteringDensityNhd x,
+        ContDiffOn ℝ ∞ (uncurry f) (U ×ˢ (univ : Set ℝ)) ∧
+          ∀ y ∈ U, γ.IsCenteringDensity y (f y) := by
+  classical
+  exact ⟨γ.localCenteringDensityNhd x,
     mem_nhds_iff.mpr
       ⟨_, Subset.rfl, γ.localCenteringDensityNhd_isOpen x, γ.localCenteringDensityNhd_self_mem x⟩,
     γ.localCenteringDensity x, γ.contDiffOn_localCenteringDensity x, fun y hy ↦
diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean
index 52ff2052..d8be7593 100644
--- a/SphereEversion/Loops/Surrounding.lean
+++ b/SphereEversion/Loops/Surrounding.lean
@@ -574,7 +574,7 @@ theorem continuous_path {X : Type*} [TopologicalSpace X] (h : SurroundingFamily
 @[simp]
 theorem path_extend_fract (h : SurroundingFamily g b γ U) (t s : ℝ) (x : E) :
     (h.path x t).extend (fract s) = γ x t s := by
-  rw [extend_extends _ (unitInterval.fract_mem s), ← Loop.fract_eq]; rfl
+  rw [extend_apply _ (unitInterval.fract_mem s), ← Loop.fract_eq]; rfl
 
 @[simp]
 theorem range_path (h : SurroundingFamily g b γ U) (x : E) (t : ℝ) :
@@ -795,7 +795,7 @@ theorem surroundingFamily_sfHomotopy [NormedSpace ℝ E] [FiniteDimensional ℝ
     SurroundingFamily g b (sfHomotopy h₀ h₁ τ) U := by
   constructor
   · intro x t;
-    simp only [sfHomotopy, Icc.mk_zero, zero_le_one, extend_extends, Path.source, Loop.ofPath_apply,
+    simp only [sfHomotopy, Icc.mk_zero, zero_le_one, extend_apply, Path.source, Loop.ofPath_apply,
       left_mem_Icc, fract_zero]
   · intro x s
     -- have h2t : ρ τ * t ≤ 0 := mul_nonpos_of_nonneg_of_nonpos (ρ_nonneg τ) ht,
diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
index d5d5d822..e6676f6a 100644
--- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
+++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
@@ -40,7 +40,7 @@ theorem finite_of_finprod_ne_one {M : Type*} {ι : Sort _} [CommMonoid M] {f : 
   classical
   rw [finprod_def] at h
   contrapose h
-  rw [Classical.not_not, dif_neg h]
+  rw [dif_neg h]
 
 theorem support_finite_of_finsum_eq_of_neZero {M : Type*} {ι : Sort _} [AddCommMonoid M]
     {f : ι → M} {x : M} [NeZero x] (h : ∑ᶠ i, f i = x) : (support f).Finite := by
diff --git a/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean b/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean
index ef1a2e34..6bd50bb3 100644
--- a/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean
+++ b/SphereEversion/ToMathlib/Analysis/NormedSpace/Misc.lean
@@ -1,4 +1,5 @@
 import Mathlib.Analysis.InnerProductSpace.EuclideanDist
+import Mathlib.Topology.OpenPartialHomeomorph.Constructions
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
diff --git a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
index 8318025a..d9548d8f 100644
--- a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
+++ b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
@@ -20,13 +20,6 @@ theorem ContinuousLinearMap.le_opNorm_of_le' {𝕜 : Type*} {𝕜₂ : Type*} {E
   apply le_of_mul_le_mul_right (h.trans (f.le_opNorm x))
   rwa [norm_pos_iff]
 
-@[simp]
-theorem ContinuousLinearMap.toSpanSingleton_zero (𝕜 : Type*) {E : Type*}
-    [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] :
-    ContinuousLinearMap.toSpanSingleton 𝕜 (0 : E) = 0 := by
-  ext
-  simp only [ContinuousLinearMap.toSpanSingleton_apply, ContinuousLinearMap.zero_apply, smul_zero]
-
 @[simp]
 theorem ContinuousLinearMap.comp_toSpanSingleton_apply {E : Type*} [NormedAddCommGroup E]
     [NormedSpace ℝ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : E →L[ℝ] ℝ) (v : E)
diff --git a/SphereEversion/ToMathlib/Equivariant.lean b/SphereEversion/ToMathlib/Equivariant.lean
index 885c2f95..216fa200 100644
--- a/SphereEversion/ToMathlib/Equivariant.lean
+++ b/SphereEversion/ToMathlib/Equivariant.lean
@@ -55,13 +55,13 @@ protected theorem monotone (h : MonotoneOn φ I) : Monotone φ := fun x y hxy 
   rw [← φ.fract_add_floor x, ← φ.fract_add_floor y]
   obtain (h2 | h2) := (floor_mono hxy).eq_or_lt
   · rw [h2]
-    refine add_le_add_right (h (unitInterval.fract_mem _) (unitInterval.fract_mem _) ?_) _
+    refine add_le_add_left (h (unitInterval.fract_mem _) (unitInterval.fract_mem _) ?_) _
     simp_rw [fract, h2]
     gcongr
-  · refine (add_le_add_right (h (unitInterval.fract_mem _) unitInterval.one_mem
+  · refine (add_le_add_left (h (unitInterval.fract_mem _) unitInterval.one_mem
       (fract_lt_one _).le) _).trans
       (le_trans ?_ <|
-        add_le_add_right (h unitInterval.zero_mem (unitInterval.fract_mem _) (fract_nonneg _)) _)
+        add_le_add_left (h unitInterval.zero_mem (unitInterval.fract_mem _) (fract_nonneg _)) _)
     rw [φ.one, add_assoc, add_comm (1 : ℝ)]
     gcongr
     norm_cast
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean
index 92ce2bb1..64276ced 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean
@@ -10,6 +10,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimension
 
 /-- A metric defining the topology on a σ-compact T₂ real manifold. -/
 def manifoldMetric [T2Space M] [SigmaCompactSpace M] : MetricSpace M :=
-  TopologicalSpace.metrizableSpaceMetric (h := Manifold.metrizableSpace I M)
+  letI := Manifold.metrizableSpace I M
+  TopologicalSpace.metrizableSpaceMetric _
 
 end
diff --git a/SphereEversion/ToMathlib/SmoothBarycentric.lean b/SphereEversion/ToMathlib/SmoothBarycentric.lean
index cf39a529..0b07797f 100644
--- a/SphereEversion/ToMathlib/SmoothBarycentric.lean
+++ b/SphereEversion/ToMathlib/SmoothBarycentric.lean
@@ -56,14 +56,14 @@ theorem evalBarycentricCoords_eq_det [Fintype ι] [DecidableEq ι] (S : Type*) [
       (b.toMatrix v).det⁻¹ • (b.toMatrix v)ᵀ.cramer (b.coords p) := by
   ext i
   by_cases h : v ∈ affineBases ι S P
-  · simp only [evalBarycentricCoords, h, dif_pos, Algebra.id.smul_eq_mul, Pi.smul_apply,
+  · simp only [evalBarycentricCoords, h, dif_pos, smul_eq_mul, Pi.smul_apply,
       AffineBasis.coords_apply]
     erw [← b.det_smul_coords_eq_cramer_coords ⟨v, h.1, h.2⟩ p]
-    simp only [Pi.smul_apply, AffineBasis.coords_apply, Algebra.id.smul_eq_mul]
+    simp only [Pi.smul_apply, AffineBasis.coords_apply, smul_eq_mul]
     have hu := b.isUnit_toMatrix ⟨v, h.1, h.2⟩
     rw [Matrix.isUnit_iff_isUnit_det] at hu
     erw [← mul_assoc, ← Ring.inverse_eq_inv, Ring.inverse_mul_cancel _ hu, one_mul]
-  · simp only [evalBarycentricCoords, h, Algebra.id.smul_eq_mul, Pi.zero_apply, inv_eq_zero,
+  · simp only [evalBarycentricCoords, h, smul_eq_mul, Pi.zero_apply, inv_eq_zero,
       dif_neg, not_false_iff, zero_eq_mul, Pi.smul_apply]
     left
     rwa [mem_affineBases_iff ι S P b v, Matrix.isUnit_iff_isUnit_det, isUnit_iff_ne_zero,
diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean
index 431409e9..b8d83093 100644
--- a/SphereEversion/ToMathlib/Topology/Misc.lean
+++ b/SphereEversion/ToMathlib/Topology/Misc.lean
@@ -77,14 +77,15 @@ instance : ProperlyDiscontinuousVAdd ℤ ℝ :=
     rcases eq_empty_or_nonempty K with (rfl | hK') <;>
         rcases eq_empty_or_nonempty L with (rfl | hL') <;>
       try simp only [image_empty, inter_self, setOf_false, finite_empty, empty_inter, inter_empty,
-        ne_eq, not_true_eq_false]
+        Set.not_nonempty_empty, image_inter_nonempty_iff]
     have hSK := (hK.isLUB_sSup hK').1
     have hIK := (hK.isGLB_sInf hK').1
     have hSL := (hL.isLUB_sSup hL').1
     have hIL := (hL.isGLB_sInf hL').1
     apply (finite_Icc ⌈sInf L - sSup K⌉ ⌊sSup L - sInf K⌋).subset
-    rintro n (hn : VAdd.vadd n '' K ∩ L ≠ ∅)
-    rcases nonempty_iff_ne_empty.mpr hn with ⟨l, ⟨k, hk, rfl⟩, hnk : (n : ℝ) + k ∈ L⟩
+    intro n hn
+    simp only [mem_setOf_eq, Set.Nonempty, mem_inter_iff, mem_preimage] at hn
+    obtain ⟨x, hk, hnk : (n : ℝ) + x ∈ L⟩ := hn
     constructor
     · rw [Int.ceil_le]
       linarith [hIL hnk, hSK hk]
diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean
index 3233d481..dc53804c 100644
--- a/SphereEversion/ToMathlib/Topology/Path.lean
+++ b/SphereEversion/ToMathlib/Topology/Path.lean
@@ -31,7 +31,7 @@ def strans (γ γ' : Path x x) (t₀ : I) : Path x x where
     · continuity
     · continuity
     · simp only [extend_div_self, Icc.mk_zero, zero_le_one, zero_div, forall_eq,
-        extend_extends, Path.source, left_mem_Icc, sub_self]
+        extend_apply, Path.source, left_mem_Icc, sub_self]
   source' := by simp
   target' := by
     simp +contextual only [unitInterval.le_one'.ge_iff_eq.trans eq_comm,
@@ -45,7 +45,7 @@ theorem strans_def {x : X} {t₀ t : I} (γ γ' : Path x x) :
       else γ' ⟨(t - t₀) / (1 - t₀),
         unitInterval.div_mem (sub_nonneg.mpr <| le_of_not_ge h) (sub_nonneg.mpr t₀.2.2)
           (sub_le_sub_right t.2.2 t₀)⟩ := by
-  split_ifs with h <;> simp [strans, h, ← extend_extends]
+  split_ifs with h <;> simp [strans, h, ← extend_apply]
 
 @[simp]
 theorem strans_of_ge {t t₀ : I} (h : t₀ ≤ t) :
diff --git a/lake-manifest.json b/lake-manifest.json
index c8cbde9e..4d70864d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c98ae54af00eaefe79c51b2b278361ca94e59bfb",
+   "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0203092c2e5e26edf967000f0e177cf31c72e17a",
+   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
+   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3611075024b3529e5798e53c733671039f06f0bd",
+   "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "45777338ffb69576c945dfe9466665b8023a8b8c",
+   "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.80+lean-v4.25.2",
+   "inputRev": "v0.0.83",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a2e4d9e9aebdbdce1ce6b6f0a19dd49e0120c990",
+   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9bff22d64abde45944c7b1f55bce6c89dd8307e6",
+   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ffad3f5b7ebe1ac3e09779ec8a863a5138c1246c",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "cd188c6ecfbf6c00cf639e4d4fb18bf773ce8c2c",
+   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.1",
+   "inputRev": "v4.26.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "SphereEversion",
diff --git a/lean-toolchain b/lean-toolchain
index 7a22c3f3..2654c20b 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.25.2
\ No newline at end of file
+leanprover/lean4:v4.26.0
\ No newline at end of file
diff --git a/scripts/build_docs.sh b/scripts/build_docs.sh
index 97acba98..0d1347b2 100755
--- a/scripts/build_docs.sh
+++ b/scripts/build_docs.sh
@@ -22,7 +22,7 @@ path = "../"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.25.1"
+rev = "TOOLCHAIN"
 EOF
 }
 
@@ -33,8 +33,7 @@ mkdir -p docbuild
 template > docbuild/lakefile.toml
 
 # Substitute the toolchain from lean-toolchain into docbuild/lakefile.toml
-# Temporarily disabled for 4.25.2.
-# sed -i s/TOOLCHAIN/`grep -oP 'v4\..*' lean-toolchain`/ docbuild/lakefile.toml
+sed -i s/TOOLCHAIN/`grep -oP 'v4\..*' lean-toolchain`/ docbuild/lakefile.toml
 
 # Initialise docbuild as a Lean project
 cd docbuild