leanprover-community · Deicyde · May 7, 2026 · May 7, 2026 · May 12, 2026 · May 12, 2026
diff --git a/Counterexamples/Phillips.lean b/Counterexamples/Phillips.lean
@@ -224,6 +224,7 @@ def restrict (f : BoundedAdditiveMeasure α) (t : Set α) : BoundedAdditiveMeasu
 theorem restrict_apply (f : BoundedAdditiveMeasure α) (s t : Set α) : f.restrict s t = f (s ∩ t) :=
   rfl
 
+set_option backward.simpa.using.reducibleClose false in
 /-- There is a maximal countable set of positive measure, in the sense that any countable set
 not intersecting it has nonpositive measure. Auxiliary lemma to prove `exists_discrete_support`. -/
 theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
@@ -456,6 +457,7 @@ along horizontals). Such a set cannot be measurable as it would contradict Fubin
 We need the continuum hypothesis to construct it.
 -/
 
+set_option backward.simpa.using.reducibleClose false in
 -- TODO: deprecate in favor of `Cardinal.exists_rel_mk_fibers_lt`
 theorem sierpinski_pathological_family (Hcont : #ℝ = ℵ₁) :
     ∃ f : ℝ → Set ℝ, (∀ x, (univ \ f x).Countable) ∧ ∀ y, {x : ℝ | y ∈ f x}.Countable := by

diff --git a/Mathlib/Algebra/AffineMonoid/Embedding.lean b/Mathlib/Algebra/AffineMonoid/Embedding.lean
@@ -43,6 +43,6 @@ noncomputable def embedding : M →+ FreeAbelianGroup (Fin (dim M)) :=
       (addMonoidOf ⊤).toAddMonoidHom
 
 lemma embedding_injective : Injective (embedding M) := by
-  simpa [embedding] using mk_left_injective 0
+  simpa [embedding] using! mk_left_injective 0
 
 end AffineAddMonoid
diff --git a/Mathlib/Algebra/Algebra/Epi.lean b/Mathlib/Algebra/Algebra/Epi.lean
@@ -143,7 +143,7 @@ lemma injective_lift_lsmul :
         map_add' m n := tmul_add _ _ _
         map_smul' r m := tmul_smul _ _ _ }
     have aux : f ∘ₗ (lift <| LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = .id := by
-      ext a m; simpa using this a m
+      ext a m; simpa using! this a m
     exact HasLeftInverse.injective ⟨f, fun x ↦ congr($aux x)⟩
   intro a m
   let f : A ⊗[R] A →ₗ[R] A ⊗[R] M := lift
@@ -153,7 +153,7 @@ lemma injective_lift_lsmul :
         map_smul' := by simp }
       map_add' := by intros; ext; simp [add_tmul]
       map_smul' := by intros; ext; simp [smul_tmul'] }
-  simpa [f] using congr_arg f (tmul_comm R 1 a)
+  simpa [f] using! congr_arg f (tmul_comm R 1 a)
 
 /-- A heterogeneous variant of `TensorProduct.lid` when `R → A` is epi. -/
 def _root_.TensorProduct.lid' : A ⊗[R] M ≃ₗ[A] M :=

diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
@@ -153,7 +153,7 @@ Useful to fix definitional equalities. -/
 protected def copy (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) :
     NonUnitalSubalgebra R A :=
   { S.toNonUnitalSubsemiring.copy s hs with
-    smul_mem' r a := by simpa [hs] using S.smul_mem r }
+    smul_mem' r a := by simpa [hs] using! S.smul_mem r }
 
 @[simp, norm_cast]
 theorem coe_copy (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) :
@@ -1171,7 +1171,7 @@ lemma adjoin_le_centralizer_centralizer (s : Set A) :
 lemma commute_of_mem_adjoin_of_forall_mem_commute {a b : A} {s : Set A}
     (hb : b ∈ adjoin R s) (h : ∀ b ∈ s, Commute a b) :
     Commute a b := by
-  have : a ∈ centralizer R s := by simpa only [Commute.symm_iff (a := a)] using h
+  have : a ∈ centralizer R s := by simpa only [Commute.symm_iff (a := a)] using! h
   exact adjoin_le_centralizer_centralizer R s hb a this
 
 lemma commute_of_mem_adjoin_singleton_of_commute {a b c : A}

diff --git a/Mathlib/Algebra/Algebra/Spectrum/Basic.lean b/Mathlib/Algebra/Algebra/Spectrum/Basic.lean
@@ -259,7 +259,7 @@ theorem star_mem_resolventSet_iff {r : R} {a : A} :
 
 protected theorem map_star (a : A) : σ (star a) = star (σ a) := by
   ext
-  simpa only [Set.mem_star, mem_iff, not_iff_not] using star_mem_resolventSet_iff.symm
+  simpa only [Set.mem_star, mem_iff, not_iff_not] using! star_mem_resolventSet_iff.symm
 
 end Star
 
@@ -390,7 +390,7 @@ local notation "↑ₐ" => algebraMap R A
 
 theorem mem_resolventSet_apply (φ : F) {a : A} {r : R} (h : r ∈ resolventSet R a) :
     r ∈ resolventSet R ((φ : A → B) a) := by
-  simpa only [map_sub, AlgHomClass.commutes] using h.map φ
+  simpa only [map_sub, AlgHomClass.commutes] using! h.map φ
 
 theorem spectrum_apply_subset (φ : F) (a : A) : σ ((φ : A → B) a) ⊆ σ a := fun _ =>
   mt (mem_resolventSet_apply φ)

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Operations.lean b/Mathlib/Algebra/Algebra/Subalgebra/Operations.lean
@@ -54,7 +54,7 @@ theorem mem_of_finsetSum_eq_one_of_pow_smul_mem
   have e' : ∑ i ∈ ι', l' i * s' i = 1 := by
     ext
     change S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
-    simpa only [map_sum, map_mul] using e
+    simpa only [map_sum, map_mul] using! e
   have : Ideal.span (s' '' ι') = ⊤ := by
     rw [Ideal.eq_top_iff_one, ← e']
     apply sum_mem

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean b/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
@@ -47,7 +47,7 @@ theorem rank_sup_eq_rank_left_mul_rank_of_free :
 
 theorem finrank_sup_eq_finrank_left_mul_finrank_of_free :
     finrank R ↥(A ⊔ B) = finrank R A * finrank A (Algebra.adjoin A (B : Set S)) := by
-  simpa only [map_mul] using congr(Cardinal.toNat $(rank_sup_eq_rank_left_mul_rank_of_free A B))
+  simpa only [map_mul] using! congr(Cardinal.toNat $(rank_sup_eq_rank_left_mul_rank_of_free A B))
 
 theorem finrank_left_dvd_finrank_sup_of_free :
     finrank R A ∣ finrank R ↥(A ⊔ B) := ⟨_, finrank_sup_eq_finrank_left_mul_finrank_of_free A B⟩

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean b/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
@@ -61,7 +61,7 @@ theorem lift_range_le {f : A →ₙₐ[R] C} {S : Subalgebra R C} :
     exact @h (f x) ⟨x, by simp⟩
   · rintro - ⟨x, rfl⟩
     induction x with
-    | _ r a => simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)
+    | _ r a => simpa using! add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)
 
 theorem lift_range (f : A →ₙₐ[R] C) :
     (lift f).range = Algebra.adjoin R (NonUnitalAlgHom.range f : Set C) :=
@@ -211,7 +211,7 @@ theorem starLift_range_le
     exact @h (f x) ⟨x, by simp⟩
   · rintro - ⟨x, rfl⟩
     induction x with
-    | _ r a => simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)
+    | _ r a => simpa using! add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)
 
 theorem starLift_range (f : A →⋆ₙₐ[R] C) :
     (starLift f).range = StarAlgebra.adjoin R (NonUnitalStarAlgHom.range f : Set C) :=

diff --git a/Mathlib/Algebra/Algebra/Unitization.lean b/Mathlib/Algebra/Algebra/Unitization.lean
@@ -850,8 +850,8 @@ lemma starMap_injective {φ : A →⋆ₙₐ[R] B} (hφ : Function.Injective φ)
     Function.Injective (starMap φ) := by
   intro x y h
   ext
-  · simpa using congr($(h).fst)
-  · exact hφ <| by simpa [algebraMap_eq_inl] using congr($(h).snd)
+  · simpa using! congr($(h).fst)
+  · exact hφ <| by simpa [algebraMap_eq_inl] using! congr($(h).snd)
 
 /-- If `φ : A →⋆ₙₐ[R] B` is surjective, the lift
 `starMap φ : Unitization R A →⋆ₐ[R] Unitization R B` is also surjective. -/

diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean
@@ -702,7 +702,7 @@ theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) ×
   by_cases him : iv < m
   · conv in Sigma.mk _ _ =>
       equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]
-    simpa using ih _
+    simpa using! ih _
   · replace him := Nat.eq_of_lt_succ_of_not_lt hi him
     subst him
     conv in Sigma.mk _ _ =>

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
@@ -393,7 +393,7 @@ theorem prod_map_toList (s : Finset ι) (f : ι → M) : (s.toList.map f).prod =
 @[to_additive (attr := simp, grind =)]
 theorem prod_toList {M : Type*} [CommMonoid M] (s : Finset M) :
     s.toList.prod = ∏ x ∈ s, x := by
-  simpa using s.prod_map_toList id
+  simpa using! s.prod_map_toList id
 
 end ToList
 

diff --git a/Mathlib/Algebra/BigOperators/Module.lean b/Mathlib/Algebra/BigOperators/Module.lean
@@ -49,7 +49,7 @@ theorem sum_Ioc_by_parts (hmn : m < n) :
       f n • G (n + 1) - f (m + 1) • G (m + 1)
         - ∑ i ∈ Ioc m (n - 1), (f (i + 1) - f i) • G (i + 1) := by
   simpa only [← Ico_add_one_add_one_eq_Ioc, Nat.sub_add_cancel (Nat.one_le_of_lt hmn),
-    add_tsub_cancel_right] using sum_Ico_by_parts f g (Nat.succ_lt_succ hmn)
+    add_tsub_cancel_right] using! sum_Ico_by_parts f g (Nat.succ_lt_succ hmn)
 
 variable (n)
 

diff --git a/Mathlib/Algebra/Category/AlgCat/Limits.lean b/Mathlib/Algebra/Category/AlgCat/Limits.lean
@@ -101,7 +101,7 @@ def limitCone : Cone F where
     { app := fun j ↦ ofHom <| limitπAlgHom F j
       naturality := fun _ _ f => by
         ext
-        simpa using (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _ }
+        simpa using! (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _ }
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Witness that the limit cone in `AlgCat R` is a limit cone.

diff --git a/Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean b/Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean
@@ -49,8 +49,8 @@ variable {R : Type u} [CommRing R]
 noncomputable instance (X : CoalgCat R) : ComonObj (ModuleCat.of R X) where
   counit := ModuleCat.ofHom Coalgebra.counit
   comul := ModuleCat.ofHom Coalgebra.comul
-  counit_comul := ModuleCat.hom_ext <| by simpa using Coalgebra.rTensor_counit_comp_comul
-  comul_counit := ModuleCat.hom_ext <| by simpa using Coalgebra.lTensor_counit_comp_comul
+  counit_comul := ModuleCat.hom_ext <| by simpa using! Coalgebra.rTensor_counit_comp_comul
+  comul_counit := ModuleCat.hom_ext <| by simpa using! Coalgebra.lTensor_counit_comp_comul
   comul_assoc := ModuleCat.hom_ext <| by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm
 
 /-- An `R`-coalgebra is a comonoid object in the category of `R`-modules. -/

diff --git a/Mathlib/Algebra/Category/Grp/Colimits.lean b/Mathlib/Algebra/Category/Grp/Colimits.lean
@@ -259,7 +259,7 @@ theorem Quot.desc_colimitCocone [DecidableEq J] (F : J ⥤ AddCommGrpCat.{w}) [S
     Quot.desc F (colimitCocone F) = (Shrink.addEquiv (α := Quot F)).symm.toAddMonoidHom := by
   refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)
   simpa only [colimitCocone_pt, AddEquiv.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe]
-    using Quot.ι_desc F (colimitCocone F) j x
+    using! Quot.ι_desc F (colimitCocone F) j x
 
 /-- (internal implementation) The fact that the candidate colimit cocone constructed in
 `colimitCocone` is the colimit.

diff --git a/Mathlib/Algebra/Category/Grp/Kernels.lean b/Mathlib/Algebra/Category/Grp/Kernels.lean
@@ -48,6 +48,6 @@ def cokernelIsColimit : IsColimit <| cokernelCocone f :=
       congr_arg Hom.hom (CokernelCofork.condition s))
     (fun _ => rfl)
     (fun _ _ h => have : Epi (cokernelCocone f).π := (epi_iff_surjective _).mpr <| mk'_surjective _
-      (cancel_epi (cokernelCocone f).π).mp <| by simpa only [parallelPair_obj_one] using h)
+      (cancel_epi (cokernelCocone f).π).mp <| by simpa only [parallelPair_obj_one] using! h)
 
 end AddCommGrpCat
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -150,7 +150,7 @@ lemma hom_ext {M N : ModuleCat.{v} R} {f g : M ⟶ N} (hf : f.hom = g.hom) : f =
 
 lemma hom_bijective {M N : ModuleCat.{v} R} :
     Function.Bijective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) where
-  left f g h := by cases f; cases g; simpa using h
+  left f g h := by cases f; cases g; simpa using! h
   right f := ⟨⟨f⟩, rfl⟩
 
 /-- Convenience shortcut for `ModuleCat.hom_bijective.injective`. -/

diff --git a/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean b/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean
@@ -158,7 +158,7 @@ private noncomputable def lequivProdOfLeftSplitExact' {f : M →ₗ[R] A} (hg :
   ((ShortComplex.Splitting.ofExactOfRetraction _
     (ShortComplex.Exact.moduleCat_of_range_eq_ker (ModuleCat.ofHom j)
     (ModuleCat.ofHom g) exac) (ModuleCat.ofHom f) (hom_ext h)
-    (by simpa only [ModuleCat.epi_iff_surjective] using hg)).isoBinaryBiproduct ≪≫
+    (by simpa only [ModuleCat.epi_iff_surjective] using! hg)).isoBinaryBiproduct ≪≫
     biprodIsoProd _ _).symm.toLinearEquiv
 
 end universe_monomorphic

diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -91,7 +91,7 @@ instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
     (restrictScalars.{v} f).Faithful where
   map_injective h := by
     ext x
-    simpa only using DFunLike.congr_fun (ModuleCat.hom_ext_iff.mp h) x
+    simpa only using! DFunLike.congr_fun (ModuleCat.hom_ext_iff.mp h) x
 
 instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
     (restrictScalars.{v} f).PreservesMonomorphisms where

diff --git a/Mathlib/Algebra/Category/ModuleCat/Colimits.lean b/Mathlib/Algebra/Category/ModuleCat/Colimits.lean
@@ -178,7 +178,7 @@ def finsuppCoconeIsColimit : IsColimit (finsuppCocone R M ι) where
   fac := by aesop (add simp finsuppCocone)
   uniq s f h := by
     ext : 1
-    exact Finsupp.lhom_ext' fun i ↦ LinearMap.ext fun x ↦ by simpa using congr($(h ⟨i⟩) (x : M))
+    exact Finsupp.lhom_ext' fun i ↦ LinearMap.ext fun x ↦ by simpa using! congr($(h ⟨i⟩) (x : M))
 
 end
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean b/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
@@ -156,7 +156,7 @@ def colimitCocone : Cocone F where
     { app := coconeMorphism F
       naturality _ _ f := by
         ext
-        simpa using (Types.TypeMax.colimitCocone
+        simpa using! (Types.TypeMax.colimitCocone
           (F ⋙ forget (ModuleCat R))).ι.naturality_apply f _ }
 
 set_option backward.isDefEq.respectTransparency false in

diff --git a/Mathlib/Algebra/Category/ModuleCat/Kernels.lean b/Mathlib/Algebra/Category/ModuleCat/Kernels.lean
@@ -78,7 +78,7 @@ def isColimitCokernelCofork (f : M ⟶ N) (g : N ⟶ P) (H : Function.Exact f.ho
     Cocone.ext (((Submodule.quotEquivOfEq _ _ (LinearMap.exact_iff.mp H)).toModuleIso).symm
     ≪≫ ((LinearMap.quotKerEquivOfSurjective _ H₂).toModuleIso)) ?_
   · rintro ⟨⟩ <;> ext x
-    · simpa using (Function.Exact.apply_apply_eq_zero H x).symm
+    · simpa using! (Function.Exact.apply_apply_eq_zero H x).symm
     · rfl
 
 end
@@ -137,6 +137,6 @@ theorem range_mkQ_cokernelIsoRangeQuotient_inv :
 theorem cokernel_π_ext {M N : ModuleCat.{u} R} (f : M ⟶ N) {x y : N} (m : M) (w : x = y + f m) :
     cokernel.π f x = cokernel.π f y := by
   subst w
-  simpa only [map_add, add_eq_left] using cokernel.condition_apply f m
+  simpa only [map_add, add_eq_left] using! cokernel.condition_apply f m
 
 end ModuleCat
diff --git a/Mathlib/Algebra/Category/ModuleCat/Limits.lean b/Mathlib/Algebra/Category/ModuleCat/Limits.lean
@@ -102,7 +102,7 @@ def limitCone : Cone F where
     { app j := ofHom (limitπLinearMap F j)
       naturality _ _ f := by
         ext
-        simpa using (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _ }
+        simpa using! (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _ }
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
@@ -188,7 +188,7 @@ instance forget₂AddCommGroup_reflectsLimit :
   reflects {c} hc := ⟨by
     have : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) := ⟨_, hc⟩
     have : Small.{w} (Functor.sections (F ⋙ forget (ModuleCat R))) := by
-      simpa only [AddCommGrpCat.hasLimit_iff_small_sections] using this
+      simpa only [AddCommGrpCat.hasLimit_iff_small_sections] using! this
     have := reflectsLimit_of_reflectsIsomorphisms F (forget₂ (ModuleCat R) AddCommGrpCat)
     exact isLimitOfReflects _ hc⟩
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean
@@ -66,7 +66,7 @@ noncomputable def freeObjDesc (φ : F ⟶ G.presheaf ⋙ forget _) : freeObj F
   naturality {X Y} f := by
     dsimp
     ext x
-    simpa using NatTrans.naturality_apply φ f x
+    simpa using! NatTrans.naturality_apply φ f x
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in

diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
@@ -329,7 +329,7 @@ noncomputable def sheafify : SheafOfModules.{v} R where
 /-- The canonical morphism from a presheaf of modules to its associated sheaf. -/
 noncomputable def toSheafify : M₀ ⟶ (restrictScalars α).obj (sheafify α φ).val :=
   homMk φ (fun X r₀ m₀ ↦ by
-    simpa using (Sheafify.map_smul_eq α φ (α.app _ r₀) (φ.app _ m₀) (𝟙 _)
+    simpa using! (Sheafify.map_smul_eq α φ (α.app _ r₀) (φ.app _ m₀) (𝟙 _)
       r₀ (by simp) m₀ (by simp)).symm)
 
 lemma toSheafify_app_apply (X : Cᵒᵖ) (x : M₀.obj X) :
@@ -396,7 +396,7 @@ noncomputable def sheafifyMap (fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ
     sheafify α φ ⟶ sheafify α φ' where
   val := homMk τ.hom (fun X r m ↦ by
     let f := (sheafifyHomEquiv' α φ (by exact A'.property)).symm (τ₀ ≫ toSheafify α φ')
-    suffices τ.hom = (toPresheaf _).map f by simpa only [this] using (f.app X).hom.map_smul r m
+    suffices τ.hom = (toPresheaf _).map f by simpa only [this] using! (f.app X).hom.map_smul r m
     apply ((J.W_of_isLocallyBijective φ).homEquiv _ A'.property).injective
     dsimp [f]
     erw [comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom]

diff --git a/Mathlib/Algebra/Category/ModuleCat/Products.lean b/Mathlib/Algebra/Category/ModuleCat/Products.lean
@@ -81,14 +81,14 @@ def coproductCoconeIsColimit : IsColimit (coproductCocone Z) where
     rintro s ⟨i⟩
     ext (x : Z i)
     simpa only [Discrete.functor_obj_eq_as, coproductCocone, Cofan.mk_pt, Functor.const_obj_obj,
-      Cofan.mk_ι_app, hom_comp, LinearMap.coe_comp, Function.comp_apply] using
+      Cofan.mk_ι_app, hom_comp, LinearMap.coe_comp, Function.comp_apply] using!
       DirectSum.toModule_lof (ι := ι) R (M := fun i ↦ Z i) i x
   uniq := by
     rintro s f h
     ext : 1
     refine DirectSum.linearMap_ext _ fun i ↦ ?_
     ext x
-    simpa only [LinearMap.coe_comp, Function.comp_apply, hom_ofHom, toModule_lof] using
+    simpa only [LinearMap.coe_comp, Function.comp_apply, hom_ofHom, toModule_lof] using!
       congr($(h ⟨i⟩) x)
 
 variable [HasCoproduct Z]

diff --git a/Mathlib/Algebra/Category/ModuleCat/Semi.lean b/Mathlib/Algebra/Category/ModuleCat/Semi.lean
@@ -143,7 +143,7 @@ lemma hom_ext {M N : SemimoduleCat.{v} R} {f g : M ⟶ N} (hf : f.hom = g.hom) :
 
 lemma hom_bijective {M N : SemimoduleCat.{v} R} :
     Function.Bijective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) where
-  left f g h := by cases f; cases g; simpa using h
+  left f g h := by cases f; cases g; simpa using! h
   right f := ⟨⟨f⟩, rfl⟩
 
 /-- Convenience shortcut for `SemimoduleCat.hom_bijective.injective`. -/

diff --git a/Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean b/Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean
@@ -77,7 +77,7 @@ def generatorsOfIsCokernelFree {M : SheafOfModules.{u} R}
     (H' : IsColimit (CokernelCofork.ofπ g H)) : M.GeneratingSections where
   I := σ
   s := M.freeHomEquiv g
-  epi := by simpa using epi_of_isColimit_cofork H'
+  epi := by simpa using! epi_of_isColimit_cofork H'
 
 @[simp]
 theorem generatorsOfIsCokernelFree_π {M : SheafOfModules.{u} R}

diff --git a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean b/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
@@ -177,7 +177,7 @@ theorem colimit_mul_mk_eq (x y : Σ j, F.obj j) (k : J) (f : x.1 ⟶ k) (g : y.1
 @[to_additive]
 lemma colimit_mul_mk_eq' {j : J} (x y : F.obj j) :
     M.mk.{v, u} F ⟨j, x⟩ * M.mk.{v, u} F ⟨j, y⟩ = M.mk.{v, u} F ⟨j, x * y⟩ := by
-  simpa using colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, y⟩ j (𝟙 _) (𝟙 _)
+  simpa using! colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, y⟩ j (𝟙 _) (𝟙 _)
 
 @[to_additive]
 noncomputable instance colimitMulOneClass : MulOneClass (M.{v, u} F) :=

diff --git a/Mathlib/Algebra/Category/Ring/Epi.lean b/Mathlib/Algebra/Category/Ring/Epi.lean
@@ -38,7 +38,7 @@ lemma CommRingCat.epi_iff_epi {R S : Type u} [CommRing R] [CommRing S] [Algebra
     let f' : S →ₐ[R] T := ⟨f.hom, RingHom.congr_fun (congrArg Hom.hom e)⟩
     let g' : S →ₐ[R] T := ⟨g.hom, fun _ ↦ rfl⟩
     ext s
-    simpa using congr(Algebra.TensorProduct.lift f' g' (fun _ _ ↦ .all _ _) $(H s))
+    simpa using! congr(Algebra.TensorProduct.lift f' g' (fun _ _ ↦ .all _ _) $(H s))
 
 @[deprecated (since := "2026-01-13")]
 alias CommRingCat.epi_iff_tmul_eq_tmul := CommRingCat.epi_iff_epi

diff --git a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean
@@ -124,7 +124,7 @@ def colimitCocone : Cocone F where
               (F ⋙ forget₂ SemiRingCat.{max v u} AddCommMonCat)).ι.app j).hom with }
       naturality _ _ f := by
         ext
-        simpa using (Types.TypeMax.colimitCocone (F ⋙ forget SemiRingCat)).ι.naturality_apply f _ }
+        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget SemiRingCat)).ι.naturality_apply f _ }
 
 namespace colimitCoconeIsColimit
 
@@ -223,7 +223,7 @@ def colimitCocone : Cocone F where
           (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})).ι.app X).hom
       naturality _ _ f := by
         ext
-        simpa using (Types.TypeMax.colimitCocone
+        simpa using! (Types.TypeMax.colimitCocone
           (F ⋙ forget CommSemiRingCat)).ι.naturality_apply f _ }
 
 /-- The proposed colimit cocone is a colimit in `CommSemiRingCat`. -/
@@ -281,7 +281,7 @@ def colimitCocone : Cocone F where
           (F ⋙ forget₂ RingCat SemiRingCat.{max v u})).ι.app X).hom
       naturality _ _ f := by
         ext
-        simpa using (Types.TypeMax.colimitCocone (F ⋙ forget RingCat)).ι.naturality_apply f _ }
+        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget RingCat)).ι.naturality_apply f _ }
 
 /-- The proposed colimit cocone is a colimit in `Ring`. -/
 def colimitCoconeIsColimit : IsColimit <| colimitCocone.{v, u} F :=
@@ -344,7 +344,7 @@ def colimitCocone : Cocone F where
           (F ⋙ forget₂ CommRingCat RingCat.{max v u})).ι.app X).hom
       naturality _ _ f := by
         ext
-        simpa using (Types.TypeMax.colimitCocone (F ⋙ forget CommRingCat)).ι.naturality_apply f _ }
+        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget CommRingCat)).ι.naturality_apply f _ }
 
 /-- The proposed colimit cocone is a colimit in `CommRingCat`. -/
 def colimitCoconeIsColimit : IsColimit <| colimitCocone.{v, u} F :=