diff --git a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean b/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean
index 4b849f14821d8..9110373e9c67a 100644
--- a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean
+++ b/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean
@@ -240,7 +240,7 @@ lemma InjectiveResolution.iso_hom_naturality {X Y : C} (f : X ⟶ Y)
       I.iso.hom ≫ (HomotopyCategory.quotient _ _).map φ := by
   apply HomotopyCategory.eq_of_homotopy
   apply descHomotopy f
-  simp
+  all_goals aesop
 
 @[reassoc]
 lemma InjectiveResolution.iso_inv_naturality {X Y : C} (f : X ⟶ Y)
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
index a6834c27400d2..ddd0fc6d43918 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
@@ -79,7 +79,7 @@ lemma IsPullback.of_iso {sq₁ sq₂ : Square C} (h : sq₁.IsPullback)
   refine CategoryTheory.IsPullback.of_iso h
     (evaluation₁.mapIso e) (evaluation₂.mapIso e)
     (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-  simp
+  all_goals simp
 
 lemma IsPullback.iff_of_iso {sq₁ sq₂ : Square C} (e : sq₁ ≅ sq₂) :
     sq₁.IsPullback ↔ sq₂.IsPullback :=
@@ -90,7 +90,7 @@ lemma IsPushout.of_iso {sq₁ sq₂ : Square C} (h : sq₁.IsPushout)
   refine CategoryTheory.IsPushout.of_iso h
     (evaluation₁.mapIso e) (evaluation₂.mapIso e)
     (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-  simp
+  all_goals simp
 
 lemma IsPushout.iff_of_iso {sq₁ sq₂ : Square C} (e : sq₁ ≅ sq₂) :
     sq₁.IsPushout ↔ sq₂.IsPushout :=
diff --git a/Mathlib/Probability/StrongLaw.lean b/Mathlib/Probability/StrongLaw.lean
index b17898d7f7abc..af74169d09b3b 100644
--- a/Mathlib/Probability/StrongLaw.lean
+++ b/Mathlib/Probability/StrongLaw.lean
@@ -426,7 +426,7 @@ theorem strong_law_aux1 {c : ℝ} (c_one : 1 < c) {ε : ℝ} (εpos : 0 < ε) :
         · simp only [mem_sigma, mem_range, filter_congr_decidable, mem_filter, and_imp,
             Sigma.forall]
           exact fun a b haN hb ↦ ⟨hb.trans_le <| u_mono <| Nat.le_pred_of_lt haN, haN, hb⟩
-        simp
+        all_goals simp
       _ ≤ ∑ j ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2 * Var[Y j] := by
         apply sum_le_sum fun j hj => ?_
         rcases @eq_zero_or_pos _ _ j with (rfl | hj)