diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean
index 560116d6..1e469aa8 100644
--- a/SphereEversion/Global/Gromov.lean
+++ b/SphereEversion/Global/Gromov.lean
@@ -40,9 +40,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple' (hRample : R.Ample) (hRopen : IsOpen
   clear! A
   intro A hA 𝓕₀ h𝓕₀
   cases' isEmpty_or_nonempty M with hM hM
-  · refine ⟨emptyHtpyFormalSol R, ?_, ?_, ?_, ?_⟩
-    all_goals try apply eventually_of_forall _
-    all_goals try intro
+  · refine ⟨emptyHtpyFormalSol R, ?_, ?_, ?_, ?_⟩ <;> intro
     all_goals try intro
     all_goals
       first
@@ -194,9 +192,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R
   clear! A
   intro A hA 𝓕₀ h𝓕₀
   cases' isEmpty_or_nonempty M with hM hM
-  · refine ⟨emptyHtpyFormalSol R, ?_, ?_, ?_, ?_⟩
-    all_goals try apply eventually_of_forall _
-    all_goals try intro
+  · refine ⟨emptyHtpyFormalSol R, ?_, ?_, ?_, ?_⟩ <;> intro
     all_goals try intro
     all_goals
       first
diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean
index 3ed69c43..54b7c065 100644
--- a/SphereEversion/Global/Immersion.lean
+++ b/SphereEversion/Global/Immersion.lean
@@ -325,7 +325,6 @@ theorem sphere_eversion :
       (formalEversion E ω) (formalEversion_hol_near_zero_one E ω) with
     ⟨f, h₁, h₂, -, h₅⟩
   have := h₂.forall_mem principal_le_nhdsSet
-  save
   refine ⟨f, h₁, ?_, ?_, ?_/-h₅-/⟩
   · ext x
     rw [this (0, x) (by simp)]
diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean
index c3c9d1b9..28f46a5e 100644
--- a/SphereEversion/Global/SmoothEmbedding.lean
+++ b/SphereEversion/Global/SmoothEmbedding.lean
@@ -424,9 +424,8 @@ theorem smooth_update (f : M' → M → N) (g : M' → X → Y) {k : M' → M} {
   have h₃ : V ∪ U = univ := by
     rw [← compl_subset_iff_union, compl_compl]
     exact image_subset_range φ K
-  have h₄ : ∀ x, k x ∈ U → update φ ψ (f x) (g x) (k x) = (ψ ∘ g x ∘ φ.invFun) (k x) := fun m hm ↦ by
-    intros
-    exact if_pos hm
+  have h₄ (x) : k x ∈ U → update φ ψ (f x) (g x) (k x) = (ψ ∘ g x ∘ φ.invFun) (k x) :=
+    fun hm ↦ if_pos hm
   by_cases hx : k x ∈ U
   · exact ⟨k ⁻¹' U, φ.isOpen_range.preimage hk.continuous, hx,
       (contMDiffOn_congr h₄).mpr <| ψ.smooth_to.comp_contMDiffOn <| hg.comp_contMDiffOn
diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean
index e94d03e8..df407270 100644
--- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean
+++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean
@@ -221,12 +221,9 @@ theorem hasFDerivAt_parametric_primitive_of_contDiff' {F : H → ℝ → E} (hF
     rw [mapsTo']
     rintro ⟨x, s⟩ ⟨x', hx, h⟩; cases h
     exact ⟨ball_subset_closedBall hx, mem_Icc_of_Ioo t_in⟩
-  have cont_x : ∀ x, Continuous (F x) := fun x ↦ hF.continuous.comp (Continuous.Prod.mk x)
-  have int_Icc : ∀ x, IntegrableOn (F x) (Icc a₀ b₀) := fun x ↦
-    (cont_x x).continuousOn.integrableOn_Icc
-  have int_Ioo : ∀ x, IntegrableOn (F x) (Ioo a₀ b₀) := by
-    exact fun x ↦ (int_Icc x).mono_set Ioo_subset_Icc_self
-  save
+  have cont_x (x) : Continuous (F x) := hF.continuous.comp (Continuous.Prod.mk x)
+  have int_Icc (x) : IntegrableOn (F x) (Icc a₀ b₀) := (cont_x x).continuousOn.integrableOn_Icc
+  have int_Ioo (x) : IntegrableOn (F x) (Ioo a₀ b₀) := (int_Icc x).mono_set Ioo_subset_Icc_self
   apply
     hasFDerivAt_parametric_primitive_of_lip' _ _ zero_lt_one ha ht₀
       (fun x _hx ↦ (cont_x x).aestronglyMeasurable) (int_Ioo x₀) (cont_x x₀).continuousAt _ _ _
diff --git a/SphereEversion/ToMathlib/SmoothBarycentric.lean b/SphereEversion/ToMathlib/SmoothBarycentric.lean
index 5708e17a..199d3c7d 100644
--- a/SphereEversion/ToMathlib/SmoothBarycentric.lean
+++ b/SphereEversion/ToMathlib/SmoothBarycentric.lean
@@ -139,7 +139,6 @@ theorem smooth_barycentric [DecidablePred (· ∈ affineBases ι 𝕜 F)] [Finit
     refine contDiff_pi.mpr fun j ↦ contDiff_pi.mpr fun j' ↦ ?_
     simp only [Matrix.updateRow_apply]
     simp only [AffineBasis.toMatrix_apply, AffineBasis.coords_apply]
-    save
     by_cases hij : j = i
     · simp only [hij, if_true, eq_self_iff_true]
       exact (smooth_barycentric_coord b j').fst'