diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean
index 7038d413..66ed8d5c 100644
--- a/SphereEversion/Local/SphereEversion.lean
+++ b/SphereEversion/Local/SphereEversion.lean
@@ -368,7 +368,7 @@ theorem locFormalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) {x : E} (hx : smoot
     locFormalEversion_φ, smoothStep.of_gt ht, hx]
   intro v
   have : (fun x : E ↦ ((1 : ℝ) - 2) • x) = fun x ↦ -x := by ext x; norm_num
-  simp [this]
+  simp only [mul_one, this, coe_orthogonalProjection_apply, one_smul]
   obtain ⟨v', hv', v, hv, rfl⟩ := Submodule.exists_add_mem_mem_orthogonal (K := ℝ ∙ x) v
   simp_rw [ContinuousLinearMap.map_add, ω.rot_one _ hv, ω.rot_eq_of_mem_span (1, x) hv']
   rw [fderiv_fun_neg, fderiv_id']
diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean
index 07073e95..6d9f9fe6 100644
--- a/SphereEversion/Loops/Exists.lean
+++ b/SphereEversion/Loops/Exists.lean
@@ -290,7 +290,7 @@ theorem exist_loops [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : IsOpe
       ((hγ₃.comp₃ contDiff_const contDiff_const contDiff_id).continuous.intervalIntegrable ..).smul
         _
     have h3 : (γ₃ 1 x).average = g x := γ₂.reparametrize_average x
-    simp [γ, γ₃, h1, h2, h3]
+    simp only [h1, h2, Loop.average_add, Loop.average_smul, Loop.average_const, h3, γ, γ₃]
     rcases h0χ x with (⟨hx, -⟩ | hx)
     · rw [hx, smul_add_one_sub_smul]
     · simp [hx]
@@ -306,6 +306,7 @@ theorem exist_loops [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : IsOpe
     rcases h0χ x with (⟨_hx, h2x⟩ | hx)
     · refine h2x t (γ₂.reparametrize x s) ?_
       simp [γ, γ₃, dist_smul_add_one_sub_smul_le (h2χ x)]
-    · simp [γ, hx]; exact hγ₁.val_in (mem_univ _)
+    · simp only [hx, zero_smul, sub_zero, one_smul, zero_add, γ]
+      exact hγ₁.val_in (mem_univ _)
   · exact (hχ.fst'.snd'.smul hb.fst'.snd').add ((contDiff_const.sub hχ.fst'.snd').smul hγ₃)
   · exact h1χ.mono fun x (hx : χ x = 1) ↦ by simp [γ, hx]
diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean
index e4958f5a..52ff2052 100644
--- a/SphereEversion/Loops/Surrounding.lean
+++ b/SphereEversion/Loops/Surrounding.lean
@@ -227,7 +227,8 @@ theorem smooth_surrounding [FiniteDimensional ℝ F] {x : F} {p : ι → F} {w :
     ((smooth_barycentric ι ℝ F hι).mono inter_subset_left).of_le le_top⟩, ?_, ?_, ?_⟩
   · simpa [V] using hyq'
   · simp [hq]
-  · simp [hq]; exact AffineBasis.linear_combination_coord_eq_self _ y
+  · simp only [hq, evalBarycentricCoords_apply_of_mem_bases, AffineBasis.coords_apply]
+    exact AffineBasis.linear_combination_coord_eq_self _ y
 
 theorem smooth_surroundingPts [FiniteDimensional ℝ F] {x : F} {p : ι → F} {w : ι → ℝ}
     (h : SurroundingPts x p w) :
@@ -823,8 +824,10 @@ theorem sfHomotopy_in' {ι} (h₀ : SurroundingFamily g b γ₀ U) (h₁ : Surro
     (h_in₀ : ∀ i, x i ∈ V → ∀ t ∈ I, ∀ (s : ℝ), τ i ≠ 1 → (x i, γ₀ (x i) t s) ∈ Ω)
     (h_in₁ : ∀ i, x i ∈ V → ∀ t ∈ I, ∀ (s : ℝ), τ i ≠ 0 → (x i, γ₁ (x i) t s) ∈ Ω) :
     (x i, sfHomotopy h₀ h₁ (τ i) (x i) t s) ∈ Ω := by
-  by_cases hτ0 : τ i = 0; · simp [hτ0]; exact h_in₀ i hx t ht s (by norm_num [hτ0])
-  by_cases hτ1 : τ i = 1; · simp [hτ1]; exact h_in₁ i hx t ht s (by norm_num [hτ1])
+  by_cases hτ0 : τ i = 0
+  · simp only [hτ0, sfHomotopy_zero]; exact h_in₀ i hx t ht s (by norm_num [hτ0])
+  by_cases hτ1 : τ i = 1
+  · simp only [hτ1, sfHomotopy_one]; exact h_in₁ i hx t ht s (by norm_num [hτ1])
   generalize hy : sfHomotopy h₀ h₁ (τ i) (x i) t s = y
   have h2y : y ∈ range (sfHomotopy h₀ h₁ (τ i) (x i) t) := by rw [← hy]; exact mem_range_self _
   rw [sfHomotopy, Loop.range_ofPath, projI_eq_self.mpr ht] at h2y
diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
index 0915bb47..d5d5d822 100644
--- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
+++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
@@ -68,7 +68,7 @@ theorem finsum_sum_filter {α β M : Type*} [AddCommMonoid M] (f : β → α) (s
   · intro x hx
     rw [mem_support] at hx
     obtain ⟨a, h, -⟩ := Finset.exists_ne_zero_of_sum_ne_zero hx
-    simp at h ⊢
+    simp only [Finset.mem_filter, Finset.coe_image, mem_image, SetLike.mem_coe] at h ⊢
     exact ⟨a, h⟩
 
 theorem sum_mem_reallyConvexHull [IsOrderedRing 𝕜]
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
index 5d9a684c..4c628b39 100644
--- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
+++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
@@ -108,9 +108,7 @@ theorem norm_crossProduct (u : E) (v : (ℝ ∙ u)ᗮ) : ‖u×₃v‖ = ‖u‖
     have h1 : ⟪u, v⟫ = 0 := v.2 _ (Submodule.mem_span_singleton_self _)
     have h2 : ⟪(v : E), w⟫ = 0 := w.2 _ (Submodule.subset_span (by simp))
     have h3 : ⟪u, w⟫ = 0 := w.2 _ (Submodule.subset_span (by simp))
-    fin_cases i <;> fin_cases j <;> norm_num at hij <;> simp [h1, h2, h3] <;>
-        rw [real_inner_comm] <;>
-      assumption
+    fin_cases i <;> fin_cases j <;> simp_all [real_inner_comm]
   refine le_of_mul_le_mul_right ?_ (by rwa [norm_pos_iff] : 0 < ‖w‖)
   -- Cauchy-Schwarz inequality for `u ×₃ v` and `w`
   simpa [inner_crossProduct_apply, ω.abs_volumeForm_apply_of_pairwise_orthogonal H,
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean
index dea3a11f..a6e353aa 100644
--- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean
+++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean
@@ -108,7 +108,8 @@ theorem orthogonalProjection_orthogonal_singleton {x y : E} :
       ⟨y - (⟪x, y⟫ / ⟪x, x⟫) • x, by
         rcases eq_or_ne x 0 with (rfl | hx)
         · simp
-        simp [mem_orthogonal_span_singleton_iff]
+        simp only [inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id_eq,
+          mem_orthogonal_span_singleton_iff]
         rw [inner_sub_right, inner_smul_right]
         simp [norm_ne_zero_iff.mpr hx]⟩ := by
   apply Subtype.ext
diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean
index a60b855f..431409e9 100644
--- a/SphereEversion/ToMathlib/Topology/Misc.lean
+++ b/SphereEversion/ToMathlib/Topology/Misc.lean
@@ -76,7 +76,8 @@ instance : ProperlyDiscontinuousVAdd ℤ ℝ :=
   ⟨fun {K L} hK hL ↦ by
     rcases eq_empty_or_nonempty K with (rfl | hK') <;>
         rcases eq_empty_or_nonempty L with (rfl | hL') <;>
-      try simp
+      try simp only [image_empty, inter_self, setOf_false, finite_empty, empty_inter, inter_empty,
+        ne_eq, not_true_eq_false]
     have hSK := (hK.isLUB_sSup hK').1
     have hIK := (hK.isGLB_sInf hK').1
     have hSL := (hL.isLUB_sSup hL').1
diff --git a/lakefile.toml b/lakefile.toml
index ba83c495..a81f4756 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,6 +6,7 @@ pp.unicode.fun = true
 autoImplicit = false
 relaxedAutoImplicit = false
 linter.mathlibStandardSet = true
+linter.flexible = true
 
 [[require]]
 name = "mathlib"