feat(Tactic): convert now discharges side goals at reducible transparency

Mathlib/Algebra/AffineMonoid/Irreducible.lean

@@ -74,7 +74,7 @@ lemma Submonoid.closure_irreducible [Monoid.FG M] :
   -- Pick a minimal set `S` generating `M`.
   obtain ⟨S, hSgen, hSmax⟩ := Submonoid.exists_minimal_closure_eq_top M
   -- We claim that `S` is the set of irreducible elements of `M`.
-  convert! hSgen
+  convert hSgen
   -- We already know that `S` contains all irreducible elements...
   refine (irreducible_subset_of_submonoidClosure_eq_top hSgen).antisymm fun r hrS ↦ ?_
   -- So let us for contradiction assume that `r ∈ S` is reducible.

Mathlib/Algebra/Algebra/Operations.lean

@@ -902,7 +902,7 @@ protected theorem map_div {B : Type*} [CommSemiring B] [Algebra R B] (I J : Subm
   · rintro hx
     refine ⟨h.symm x, fun z hz => ?_, h.apply_symm_apply x⟩
     obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩
-    convert! xz_mem
+    convert xz_mem
     apply h.injective
     rw [map_mul, h.apply_symm_apply, hxz]
 

Mathlib/Algebra/Algebra/Spectrum/Pi.lean

@@ -57,12 +57,12 @@ def PreQuasiregular.toProd [NonUnitalSemiring A] [NonUnitalSemiring B] :
 lemma isQuasiregular_pi_iff [∀ i, NonUnitalSemiring (κ i)] (x : ∀ i, κ i) :
     IsQuasiregular x ↔ ∀ i, IsQuasiregular (x i) := by
   simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toPi κ), Pi.isUnit_iff]
-  congr!
+  congr! (config := { postTransparency := .default })
 
 lemma isQuasiregular_prod_iff [NonUnitalSemiring A] [NonUnitalSemiring B] (a : A) (b : B) :
     IsQuasiregular (⟨a, b⟩ : A × B) ↔ IsQuasiregular a ∧ IsQuasiregular b := by
   simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toProd A B), Prod.isUnit_iff]
-  congr!
+  congr! (config := { postTransparency := .default })
 
 lemma quasispectrum.mem_iff_of_isUnit [CommSemiring R] [NonUnitalRing A]
     [Module R A] {a : A} {r : R} (hr : IsUnit r) :

Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

@@ -156,13 +156,13 @@ def unitsFstOne_mulEquiv_quasiregular : unitsFstOne R A ≃* (PreQuasiregular A)
       { val := 1 + PreQuasiregular.equiv.symm x.val
         inv := 1 + PreQuasiregular.equiv.symm x⁻¹.val
         val_inv := by
-          convert! congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A)) using 1
+          convert congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A)) using 1
           · simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
               add_mul, inr_add, inr_mul]
             abel
           · simp only [inr_zero, add_zero]
         inv_val := by
-          convert! congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A)) using 1
+          convert congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A)) using 1
           · simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
               add_mul, inr_add, inr_mul]
             abel
@@ -216,8 +216,8 @@ lemma IsQuasiregular.isUnit_one_add {R : Type*} [Semiring R] {x : R} (hx : IsQua
     IsUnit (1 + x) := by
   obtain ⟨y, hy₁, hy₂⟩ := isQuasiregular_iff.mp hx
   refine ⟨⟨1 + x, 1 + y, ?_, ?_⟩, rfl⟩
-  · convert! congr(1 + $(hy₁)) using 1 <;> [noncomm_ring; simp]
-  · convert! congr(1 + $(hy₂)) using 1 <;> [noncomm_ring; simp]
+  · convert congr(1 + $(hy₁)) using 1 <;> [noncomm_ring; simp]
+  · convert congr(1 + $(hy₂)) using 1 <;> [noncomm_ring; simp]
 
 lemma isQuasiregular_iff_isUnit {R : Type*} [Ring R] {x : R} :
     IsQuasiregular x ↔ IsUnit (1 + x) := by
@@ -229,7 +229,7 @@ lemma isQuasiregular_iff_isUnit {R : Type*} [Ring R] {x : R} :
   case' h.right => have := congr($(hx.val_inv_mul) - 1)
   all_goals
     rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this
-    convert! this using 1
+    convert this using 1
     noncomm_ring
 
 -- interestingly, this holds even in the semiring case.
@@ -314,7 +314,7 @@ lemma spectrum_subset_quasispectrum (R : Type*) {A : Type*} [CommSemiring R] [Ri
 
 lemma quasispectrum_eq_spectrum_union_zero (R : Type*) {A : Type*} [Semifield R] [Ring A]
     [Algebra R A] (a : A) : quasispectrum R a = spectrum R a ∪ {0} := by
-  convert! quasispectrum_eq_spectrum_union R a
+  convert quasispectrum_eq_spectrum_union R a
   simp
 
 lemma mem_quasispectrum_iff {R A : Type*} [Semifield R] [Ring A]
@@ -518,10 +518,10 @@ protected lemma comp {R₁ R₂ R₃ A : Type*} [Semifield R₁] [Field R₂] [F
     (hf : QuasispectrumRestricts a f) (hg : QuasispectrumRestricts a g) :
     QuasispectrumRestricts a e where
   left_inv := by
-    convert! hfge ▸ hf.left_inv.comp hg.left_inv
+    convert hfge ▸ hf.left_inv.comp hg.left_inv
     congrm (⇑$(IsScalarTower.algebraMap_eq R₁ R₂ R₃))
   rightInvOn := by
-    convert! hfge ▸ hg.rightInvOn.comp hf.rightInvOn fun _ ↦ hf.apply_mem
+    convert hfge ▸ hg.rightInvOn.comp hf.rightInvOn fun _ ↦ hf.apply_mem
     congrm (⇑$(IsScalarTower.algebraMap_eq R₁ R₂ R₃))
 
 end NonUnital

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -725,7 +725,7 @@ scoped instance faithfulSMul :
     letI := (inclusion h).toModule; FaithfulSMul S T :=
   letI := (inclusion h).toModule
   ⟨fun {x y} h ↦ Subtype.ext <| by
-    convert! Subtype.ext_iff.mp (h 1) using 1 <;> exact (mul_one _).symm⟩
+    convert Subtype.ext_iff.mp (h 1) using 1 <;> exact (mul_one _).symm⟩
 
 end inclusion
 

Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean

@@ -111,7 +111,7 @@ lemma centralizer_coe_image_includeRight_eq_center_tensorProduct
       (Subalgebra.centralizer R (S : Set B)).val).range := by
   have eq1 := centralizer_coe_image_includeLeft_eq_center_tensorProduct R B A S
   apply_fun Subalgebra.comap (Algebra.TensorProduct.comm R A B).toAlgHom at eq1
-  convert! eq1
+  convert eq1
   · ext x
     simpa [mem_centralizer_iff] using
       ⟨fun h b hb ↦ (Algebra.TensorProduct.comm R A B).symm.injective <| by aesop, fun h b hb ↦

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -713,7 +713,7 @@ theorem mem_adjoin_of_map_mul {s} {x : A} {f : A →ₗ[R] B} (hf : ∀ a₁ a
   | algebraMap r =>
     have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
       subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
-    convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
+    convert Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
     rw [algebraMap_eq_smul_one]
     exact f.map_smul _ _
   | add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
@@ -860,8 +860,8 @@ theorem eqOn_adjoin_iff {φ ψ : A →ₐ[R] B} {s : Set A} :
 theorem adjoin_ext {s : Set A} ⦃φ₁ φ₂ : adjoin R s →ₐ[R] B⦄
     (h : ∀ x hx, φ₁ ⟨x, subset_adjoin hx⟩ = φ₂ ⟨x, subset_adjoin hx⟩) : φ₁ = φ₂ :=
   ext fun ⟨x, hx⟩ ↦ adjoin_induction h (fun _ ↦ φ₂.commutes _ ▸ φ₁.commutes _)
-    (fun _ _ _ _ h₁ h₂ ↦ by convert! congr_arg₂ (· + ·) h₁ h₂ <;> rw [← map_add] <;> rfl)
-    (fun _ _ _ _ h₁ h₂ ↦ by convert! congr_arg₂ (· * ·) h₁ h₂ <;> rw [← map_mul] <;> rfl) hx
+    (fun _ _ _ _ h₁ h₂ ↦ by convert congr_arg₂ (· + ·) h₁ h₂ <;> rw [← map_add] <;> rfl)
+    (fun _ _ _ _ h₁ h₂ ↦ by convert congr_arg₂ (· * ·) h₁ h₂ <;> rw [← map_mul] <;> rfl) hx
 
 theorem ext_of_eq_adjoin {S : Subalgebra R A} {s : Set A} (hS : S = adjoin R s) ⦃φ₁ φ₂ : S →ₐ[R] B⦄
     (h : ∀ x hx, φ₁ ⟨x, hS.ge (subset_adjoin hx)⟩ = φ₂ ⟨x, hS.ge (subset_adjoin hx)⟩) :
@@ -977,7 +977,7 @@ theorem comap_map_eq (f : A →ₐ[R] B) (S : Subalgebra R A) :
 
 theorem comap_map_eq_self {f : A →ₐ[R] B} {S : Subalgebra R A}
     (h : f ⁻¹' {0} ⊆ S) : (S.map f).comap f = S := by
-  convert! comap_map_eq f S
+  convert comap_map_eq f S
   rwa [left_eq_sup, Algebra.adjoin_le_iff]
 
 end Subalgebra

Mathlib/Algebra/BigOperators/Fin.lean

@@ -663,7 +663,7 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
         simp_rw [Fin.val_zero, Fintype.prod_empty, Nat.div_one, mul_one, Fin.cons_zero,
           Fin.prod_univ_succ, Fin.castLE_zero, Fin.cons_zero, ← Nat.div_div_eq_div_mul,
           mul_left_comm (_ % _ : ℕ), ← mul_sum]
-        convert! Nat.mod_add_div _ _
+        convert Nat.mod_add_div _ _
         exact ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq (Fin.prod_univ_succ _)))
 
 theorem finPiFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (f : ∀ i : Fin m, Fin (n i)) :

Mathlib/Algebra/BigOperators/Group/Finset/Piecewise.lean

@@ -191,7 +191,7 @@ theorem prod_inter_mul_prod_diff [DecidableEq ι] (s t : Finset ι) (f : ι →
 theorem prod_eq_mul_prod_diff_singleton [DecidableEq ι] {s : Finset ι} (i : ι) (f : ι → M)
     (h : i ∉ s → f i = 1) : ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x := by
   by_cases hs : i ∈ s
-  · convert! (s.prod_inter_mul_prod_diff { i } f).symm
+  · convert (s.prod_inter_mul_prod_diff { i } f).symm
     simp [hs]
   · simp_all only [not_false_eq_true, forall_const, one_mul]
     apply Finset.prod_congr <;> aesop

Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean

@@ -93,7 +93,7 @@ theorem prod_hom (s : Multiset M) {F : Type*} [FunLike F M N]
 theorem prod_hom' (s : Multiset ι) {F : Type*} [FunLike F M N]
     [MonoidHomClass F M N] (f : F)
     (g : ι → M) : (s.map fun i => f <| g i).prod = f (s.map g).prod := by
-  convert! (s.map g).prod_hom f
+  convert (s.map g).prod_hom f
   exact (map_map _ _ _).symm
 
 @[to_additive]

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -256,8 +256,7 @@ lemma Finset.prod_fin_Icc_eq_prod_nat_Icc [CommMonoid α] {n : ℕ} (a b : Fin n
 lemma Fin.prod_Iic_div [CommGroup M] {n : ℕ} (a : Fin n) (f : Fin (n + 1) → M) :
     ∏ i ∈ Iic a, (f i.succ / f i.castSucc) = f a.succ / f 0 := by
   rw [← prod_ite_mem_eq, prod_fin_eq_prod_range]
-  convert! prod_range_div (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1) (a + 1) using 1 with k
-    hk
+  convert prod_range_div (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1) (a + 1) using 1 with k hk
   · exact prod_congr_of_eq_on_inter (by grind) (by grind) (by simp_all; grind)
   · grind
 

Mathlib/Algebra/BigOperators/Ring/Finset.lean

@@ -164,7 +164,7 @@ lemma sum_prod_piFinset [Fintype ι] (s : Finset κ) (g : ι → κ → R) :
 
 lemma sum_pow' (s : Finset κ) (f : κ → R) (n : ℕ) :
     (∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i : Fin n ↦ s, ∏ i, f (p i) := by
-  convert! @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp
+  convert @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp
 
 /-- The product of `f a + g a` over all of `s` is the sum over the powerset of `s` of the product of
 `f` over a subset `t` times the product of `g` over the complement of `t` -/
@@ -266,7 +266,7 @@ lemma prod_sub_ordered [LinearOrder ι] (s : Finset ι) (f g : ι → R) :
       (∏ i ∈ s, f i) -
         ∑ i ∈ s, g i * (∏ j ∈ s with j < i, (f j - g j)) * ∏ j ∈ s with i < j, f j := by
   simp only [sub_eq_add_neg]
-  convert! prod_add_ordered s f fun i => -g i
+  convert prod_add_ordered s f fun i => -g i
   simp
 
 /-- `∏ i, (1 - f i) = 1 - ∑ i, f i * (∏ j < i, 1 - f j)`. This formula is useful in construction of

Mathlib/Algebra/Category/Grp/EpiMono.lean

@@ -245,7 +245,7 @@ theorem h_apply_fromCoset_nin_range (x : B) (hx : x ∈ f.hom.range) (b : B) (hb
       (fromCoset ⟨b • ↑f.hom.range, b, rfl⟩) (fromCoset_ne_of_nin_range _ hb) (by simp)]
   simp only [g_apply_fromCoset, leftCoset_assoc]
   refine Equiv.swap_apply_of_ne_of_ne (fromCoset_ne_of_nin_range _ fun r => hb ?_) (by simp)
-  convert! Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r
+  convert Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r
   rw [← mul_assoc, inv_mul_cancel, one_mul]
 
 theorem agree : f.hom.range = { x | h x = g x } := by

Mathlib/Algebra/Category/ModuleCat/Descent.lean

@@ -60,7 +60,7 @@ def comonadicExtendScalars (hf : f.FaithfullyFlat) :
     ComonadicLeftAdjoint (extendScalars f) := by
   have := preservesFiniteLimits_extendScalars_of_flat hf.flat
   have := reflectsIsomorphisms_extendScalars_of_faithfullyFlat hf
-  convert!
+  convert
     Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms
       (extendRestrictScalarsAdj f)
   · exact ⟨inferInstance⟩

Mathlib/Algebra/Category/ModuleCat/EpiMono.lean

@@ -38,14 +38,14 @@ theorem range_eq_top_of_epi [Epi f] : LinearMap.range f.hom = ⊤ :=
 
 theorem mono_iff_ker_eq_bot : Mono f ↔ LinearMap.ker f.hom = ⊥ :=
   ⟨fun _ => ker_eq_bot_of_mono _, fun hf =>
-    ConcreteCategory.mono_of_injective _ <| by convert! LinearMap.ker_eq_bot.1 hf⟩
+    ConcreteCategory.mono_of_injective _ <| by convert LinearMap.ker_eq_bot.1 hf⟩
 
 theorem mono_iff_injective : Mono f ↔ Function.Injective f := by
   rw [mono_iff_ker_eq_bot, LinearMap.ker_eq_bot]
 
 theorem epi_iff_range_eq_top : Epi f ↔ LinearMap.range f.hom = ⊤ :=
   ⟨fun _ => range_eq_top_of_epi _, fun hf =>
-    ConcreteCategory.epi_of_surjective _ <| by convert! LinearMap.range_eq_top.1 hf⟩
+    ConcreteCategory.epi_of_surjective _ <| by convert LinearMap.range_eq_top.1 hf⟩
 
 theorem epi_iff_surjective : Epi f ↔ Function.Surjective f := by
   rw [epi_iff_range_eq_top, LinearMap.range_eq_top]

Mathlib/Algebra/Category/ModuleCat/Free.lean

@@ -84,7 +84,7 @@ theorem linearIndependent_shortExact {w : ι' → S.X₃} (hw : LinearIndependen
     LinearIndependent R (Sum.elim (S.f ∘ v) (S.g.hom.toFun.invFun ∘ w)) := by
   apply linearIndependent_leftExact hS'.exact hv _ hS'.mono_f rfl
   dsimp
-  convert! hw
+  convert hw
   ext
   apply Function.rightInverse_invFun ((epi_iff_surjective _).mp hS'.epi_g)
 
@@ -144,7 +144,7 @@ theorem span_rightExact {w : ι' → S.X₃} (hv : ⊤ ≤ span R (range v))
     ⊤ ≤ span R (range (Sum.elim (S.f ∘ v) (S.g.hom.toFun.invFun ∘ w))) := by
   refine span_exact hS ?_ hv ?_
   · simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]
-  · convert! hw
+  · convert hw
     simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
     rw [ModuleCat.epi_iff_surjective] at hE
     rw [← Function.comp_assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE),

Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackFree.lean

@@ -107,7 +107,7 @@ instance [F.Final] : IsIso (pullbackObjUnitToUnit φ) := by
   intro M
   rw [← ((pullbackPushforwardAdjunction.{u} φ).homEquiv _ _).bijective.of_comp_iff',
     ← (unitHomEquiv _).bijective.of_comp_iff']
-  convert! (bijective_pushforwardSections φ M).comp (unitHomEquiv _).bijective
+  convert (bijective_pushforwardSections φ M).comp (unitHomEquiv _).bijective
   ext f : 1
   dsimp
   rw [pushforwardSections_unitHomEquiv, EmbeddingLike.apply_eq_iff_eq,

Mathlib/Algebra/Category/ModuleCat/Subobject.lean

@@ -47,9 +47,10 @@ noncomputable def subobjectModule : Subobject M ≃o Submodule R M :=
         · ext x
           rfl)
       left_inv := fun N => by
-        convert!
+        convert
           congr_arg LinearMap.range
-            (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype))) using 1
+            (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype))) using
+          1
         · have :
             (underlyingIso (ofHom N.subtype)).inv =
               ofHom (underlyingIso (ofHom N.subtype)).symm.toLinearEquiv.toLinearMap := by
@@ -59,7 +60,7 @@ noncomputable def subobjectModule : Subobject M ≃o Submodule R M :=
         · exact (Submodule.range_subtype _).symm
       map_rel_iff' := fun {S T} => by
         refine ⟨fun h => ?_, fun h => mk_le_mk_of_comm (↟(Submodule.inclusion h)) rfl⟩
-        convert! LinearMap.range_comp_le_range (ofMkLEMk _ _ h).hom (ofHom T.subtype).hom
+        convert LinearMap.range_comp_le_range (ofMkLEMk _ _ h).hom (ofHom T.subtype).hom
         · rw [← hom_comp, ofMkLEMk_comp]
           exact (Submodule.range_subtype _).symm
         · exact (Submodule.range_subtype _).symm }

Mathlib/Algebra/Category/Ring/Instances.lean

@@ -48,7 +48,7 @@ theorem CommRingCat.isLocalHom_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S 
 
 theorem isLocalHom_of_iso {R S : CommRingCat} (f : R ≅ S) : IsLocalHom f.hom.hom :=
   { map_nonunit := fun a ha => by
-      convert! f.inv.hom.isUnit_map ha
+      convert f.inv.hom.isUnit_map ha
       simp }
 
 -- see Note [lower instance priority]

Mathlib/Algebra/Category/Ring/Topology.lean

@@ -97,7 +97,7 @@ lemma isClosedEmbedding_precomp_of_surjective
   refine ⟨isEmbedding_precomp_of_surjective f hf, ?_⟩
   have : IsClosed (⋂ i : RingHom.ker f.hom, { f : A ⟶ R | f i = 0 }) :=
     isClosed_iInter fun x ↦ (isClosed_singleton (x := 0)).preimage (continuous_apply (R := R) x.1)
-  convert! this
+  convert this
   ext x
   simp only [Set.mem_range, Set.mem_iInter, Set.mem_setOf_eq, Subtype.forall, RingHom.mem_ker]
   constructor
@@ -179,7 +179,7 @@ lemma isEmbedding_pushout [IsTopologicalRing R] (φ : A ⟶ B) (ψ : A ⟶ C) :
     ((isEmbedding_graph continuous_id).prodMap Homeomorph.sumArrowHomeomorphProdArrow.isEmbedding)
   have H := (mvPolynomialHomeomorph B R A).symm.isEmbedding.prodMap
     (mvPolynomialHomeomorph C R A).symm.isEmbedding
-  convert!
+  convert
     ((H.comp hF).comp (mvPolynomialHomeomorph _ R A).isEmbedding).comp
       (isEmbedding_precomp_of_surjective (R := R) fBC hfBC)
   have (s : _) : (pushout.inr φ ψ).hom (ψ.hom s) = (pushout.inl φ ψ).hom (φ.hom s) :=

Mathlib/Algebra/CharP/Basic.lean

@@ -145,7 +145,7 @@ instance Nat.lcm.charP [CharP S q] : CharP (R × S) (Nat.lcm p q) where
 /-- The characteristic of the product of two rings of the same characteristic
   is the same as the characteristic of the rings -/
 instance Prod.charP [CharP S p] : CharP (R × S) p := by
-  convert! Nat.lcm.charP R S p p; simp
+  convert Nat.lcm.charP R S p p; simp
 
 instance Prod.charZero_of_left [CharZero R] : CharZero (R × S) where
   cast_injective _ _ h := CharZero.cast_injective congr(Prod.fst $h)

Mathlib/Algebra/Field/IsField.lean

@@ -77,7 +77,7 @@ noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R)
   __ := h
   inv a := if ha : a = 0 then 0 else Classical.choose (h.mul_inv_cancel ha)
   inv_zero := dif_pos rfl
-  mul_inv_cancel a ha := by convert! Classical.choose_spec (h.mul_inv_cancel ha); exact dif_neg ha
+  mul_inv_cancel a ha := by convert Classical.choose_spec (h.mul_inv_cancel ha); exact dif_neg ha
   nnqsmul := _
   nnqsmul_def _ _ := rfl
 

Mathlib/Algebra/Field/Subfield/Basic.lean

@@ -275,7 +275,7 @@ theorem sInf_toSubring (s : Set (Subfield K)) :
 theorem isGLB_sInf (S : Set (Subfield K)) : IsGLB S (sInf S) := by
   have : ∀ {s t : Subfield K}, (s : Set K) ≤ t ↔ s ≤ t := by simp [SetLike.coe_subset_coe]
   refine IsGLB.of_image this ?_
-  convert! isGLB_biInf (s := S) (f := SetLike.coe)
+  convert isGLB_biInf (s := S) (f := SetLike.coe)
   exact coe_sInf _
 
 /-- Subfields of a ring form a complete lattice. -/

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -624,7 +624,7 @@ theorem isUnit_gcd_of_eq_mul_gcd {α : Type*} [CommMonoidWithZero α] [GCDMonoid
     IsUnit (gcd x' y') := by
   rw [← associated_one_iff_isUnit]
   refine Associated.of_mul_left ?_ (Associated.refl <| gcd x y) h
-  convert! (gcd_mul_left' (gcd x y) x' y').symm using 1
+  convert (gcd_mul_left' (gcd x y) x' y').symm using 1
   rw [← ex, ← ey, mul_one]
 
 theorem extract_gcd {α : Type*} [CommMonoidWithZero α] [GCDMonoid α] (x y : α) :

Mathlib/Algebra/GCDMonoid/IntegrallyClosed.lean

@@ -28,7 +28,7 @@ theorem IsLocalization.surj_of_gcd_domain [GCDMonoid R] (M : Submonoid R) [IsLoc
   obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y
   use x', y', hu
   rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]
-  convert! IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2
+  convert IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2
   grind
 
 instance (priority := 100) GCDMonoid.toIsIntegrallyClosed

Mathlib/Algebra/Group/Action/Basic.lean

@@ -150,7 +150,8 @@ variable (M α) in
 @[to_additive
 /-- Embedding of `α` into functions `M → α` induced by an additive action of `M` on `α`. -/]
 def toFun : α ↪ M → α :=
-  ⟨fun y x ↦ x • y, fun y₁ y₂ H ↦ one_smul M y₁ ▸ one_smul M y₂ ▸ by convert! congr_fun H 1⟩
+  ⟨fun y x ↦ x • y, fun y₁ y₂ H ↦ one_smul M y₁ ▸ one_smul M y₂ ▸ by convert
+    congr_fun H 1⟩
 
 @[to_additive (attr := simp)]
 lemma toFun_apply (x : M) (y : α) : MulAction.toFun M α y x = x • y := rfl

Mathlib/Algebra/Group/Action/Equidecomp.lean

@@ -191,7 +191,7 @@ theorem IsDecompOn.of_leftInvOn {f g : X → X} {A : Set X} {S : Finset G}
 noncomputable def symm (f : Equidecomp X G) : Equidecomp X G where
   toPartialEquiv := f.toPartialEquiv.symm
   isDecompOn' := by classical exact ⟨f.witness⁻¹, by
-    convert! f.isDecompOn.of_leftInvOn f.leftInvOn
+    convert f.isDecompOn.of_leftInvOn f.leftInvOn
     rw [image_source_eq_target, symm_source]⟩
 
 theorem map_target {f : Equidecomp X G} {x : X} (h : x ∈ f.target) :