feat(Tactic): convert discharges side goals reducibly (leanprover-community#39928)

Vierkantor · ReemMelamed · commit f181353e6ba0 · 2026-06-20T15:19:45.000+03:00
This PR implements the main behaviour change from leanprover-community#39039: `convert` now discharges side goals at reducible transparency. `convert!`, which we previously switched all calls inside Mathlib to, keeps the old behaviour of working at default transparency. (Everything discussed in this PR holds analogously for the other tactics in the family: `convert_to` and `ac_change`). The main trick in this PR is in allowing `convert!` to have different configuration options than `convert`, but still allow the user to override those options too. So `convert! (postTransparency := .instances)` will have transparency set to `.instances`, not `.default`. We achieve this by having two new structures that copy `Congr!.Config` but set different default values, and choosing between the corresponding elaborators for those configs based on the presence of an `!`. I got this trick from Jovan's leanprover-community#38071 which also changes settings in `Convert.Config`. This PR should be mostly compatible with leanprover-community#38071 and I'd like to get both this one and leanprover-community#38071 in before wrapping up leanprover-community#39039 by replacing unnecessary calls to `convert!` with `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
diff --git a/Counterexamples/Phillips.lean b/Counterexamples/Phillips.lean
@@ -283,7 +283,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
   have I1 : ∀ n, ε / 2 ≤ f (↑(s (n + 1)) \ ↑(s n)) := by
     intro n
     rw [div_le_iff₀' (show (0 : ℝ) < 2 by simp), hε]
-    convert hF (s n) u using 2
+    convert! hF (s n) u using 2
     · ext x
       simp only [u, not_exists, mem_iUnion, mem_diff]
       tauto
diff --git a/Mathlib/Algebra/Lie/Weights/Chain.lean b/Mathlib/Algebra/Lie/Weights/Chain.lean
@@ -239,7 +239,7 @@ lemma exists_forall_mem_corootSpace_smul_add_eq_zero
   subst a b N
   erw [LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup _ h₁ h₂ (genWeightSpaceChain M α χ p q) h₃]
   simp_rw [LieSubmodule.toEnd_restrict_eq_toEnd]
-  convert_to _ =
+  convert_to! _ =
     ∑ k ∈ Finset.Ioo p q, (LinearMap.trace R { x // x ∈ (genWeightSpace M (k • α + χ)) })
       ((toEnd R { x // x ∈ H } { x // x ∈ genWeightSpace M (k • α + χ) }) x)
   simp_rw [trace_toEnd_genWeightSpace, Pi.add_apply, Pi.smul_apply, smul_add,
diff --git a/Mathlib/Algebra/Lie/Weights/Killing.lean b/Mathlib/Algebra/Lie/Weights/Killing.lean
@@ -608,7 +608,7 @@ lemma finrank_rootSpace_eq_one (α : Weight K H L) (hα : α.IsNonZero) :
     finrank K (rootSpace H α) = 1 := by
   suffices ¬ 1 < finrank K (rootSpace H α) by
     have h₀ : finrank K (rootSpace H α) ≠ 0 := by
-      convert_to finrank K (rootSpace H α).toSubmodule ≠ 0
+      convert_to! finrank K (rootSpace H α).toSubmodule ≠ 0
       simpa using! α.genWeightSpace_ne_bot
     lia
   intro contra
diff --git a/Mathlib/Algebra/SkewPolynomial/Basic.lean b/Mathlib/Algebra/SkewPolynomial/Basic.lean
@@ -360,7 +360,7 @@ lemma coeff_X_of_ne_one {n : ℕ} (hn : n ≠ 1) : coeff (X : SkewPolynomial R)
   rw [coeff_X, if_neg hn.symm]
 
 lemma coeff_C : coeff (C a) n = ite (n = 0) a 0 := by
-  convert coeff_monomial using 2; simp [eq_comm]
+  convert! coeff_monomial using 2; simp [eq_comm]
 
 @[simp] lemma coeff_C_zero : coeff (C a) 0 = a := coeff_monomial
 
diff --git a/Mathlib/AlgebraicGeometry/Cover/Open.lean b/Mathlib/AlgebraicGeometry/Cover/Open.lean
@@ -193,7 +193,7 @@ lemma OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom
   simp only [Cover.pullbackHom, pullbackCoverAffineRefinementObjIso, Iso.trans_inv, asIso_inv,
     Iso.symm_inv, Category.assoc, pullbackSymmetry_inv_comp_snd, IsIso.inv_comp_eq, limit.lift_π,
     PullbackCone.mk_π_app, Category.comp_id]
-  convert pullbackSymmetry_inv_comp_fst ((𝒰.X i.1).affineCover.f i.2) (pullback.fst _ _)
+  convert! pullbackSymmetry_inv_comp_fst ((𝒰.X i.1).affineCover.f i.2) (pullback.fst _ _)
   exact pullbackRightPullbackFstIso_hom_fst _ _ _
 
 /-- A family of elements spanning the unit ideal of `R` gives an affine open cover of `Spec R`. -/
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean b/Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean
@@ -167,7 +167,7 @@ nonrec instance (priority := low) [IsIntegral Y] [Subsingleton Y] :
   obtain ⟨ψ, rfl⟩ := Spec.map_surjective g
   algebraize [φ.hom, ψ.hom]
   refine (MorphismProperty.cancel_left_of_respectsIso _ (pullbackSpecIso K R S).inv _).mp ?_
-  convert_to topologically _ (Spec.map <| CommRingCat.ofHom (algebraMap R (TensorProduct K R S)))
+  convert_to! topologically _ (Spec.map <| CommRingCat.ofHom (algebraMap R (TensorProduct K R S)))
   · exact pullbackSpecIso_inv_fst ..
   let := hK.toField
   exact PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field
diff --git a/Mathlib/AlgebraicGeometry/Normalization.lean b/Mathlib/AlgebraicGeometry/Normalization.lean
@@ -290,7 +290,7 @@ instance [IsIntegralHom f] : IsIso f.toNormalization := by
   rw [← MorphismProperty.cancel_left_of_respectsIso (.isomorphisms _)
     (e ≪≫ (U.2.preimage f).isoSpec).inv]
   letI := (f.app U.1).hom.toAlgebra
-  convert_to IsIso (Spec.map (CommRingCat.ofHom
+  convert_to! IsIso (Spec.map (CommRingCat.ofHom
       (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1)).val.toRingHom))
   · rw [← cancel_mono (f.normalizationOpenCover.f U), ← cancel_epi (U.2.preimage f).isoSpec.hom]
     simp [e, -Iso.cancel_iso_hom_left, IsAffineOpen.isoSpec_hom,
diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -468,7 +468,7 @@ theorem _root_.AlgebraicGeometry.isIso_iff_isIso_stalkMap {X Y : Scheme.{u}} (f
     IsOpenImmersion.iff_isIso_stalkMap, and_comm, ← and_assoc]
   refine and_congr ⟨?_, ?_⟩ Iff.rfl
   · rintro ⟨h₁, h₂⟩
-    convert_to
+    convert_to!
       IsIso
         (TopCat.isoOfHomeo
           (Equiv.toHomeomorphOfContinuousOpen
diff --git a/Mathlib/AlgebraicGeometry/PointsPi.lean b/Mathlib/AlgebraicGeometry/PointsPi.lean
@@ -88,7 +88,7 @@ lemma isIso_of_comp_eq_sigmaSpec {V : Scheme}
     infer_instance
   obtain ⟨I, e, rfl⟩ := IsClosedImmersion.Spec_iff.mp this
   obtain rfl := eq_bot_of_comp_quotientMk_eq_sigmaSpec R I (f ≫ e.hom) (by rwa [Category.assoc])
-  convert_to IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot _).toCommRingCatIso.inv)
+  convert_to! IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot _).toCommRingCatIso.inv)
   infer_instance
 
 variable (X : Scheme)
diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean
@@ -1079,7 +1079,7 @@ theorem comapₗ_eq_localRingHom (f : R →+* S) (U : Opens (PrimeSpectrum.Top R
   induction m using LocalizedModule.induction_on with | h m s =>
   trans LocalizedModule.mk (f m) ⟨f ↑s, s.2⟩
   · simp
-  convert_to Localization.mk _ _ = Localization.localRingHom _ _ _ _ (Localization.mk _ _)
+  convert_to! Localization.mk _ _ = Localization.localRingHom _ _ _ _ (Localization.mk _ _)
   simp [Localization.mk_eq_mk']
 
 /-- For a ring homomorphism `f : R →+* S` and open sets `U` and `V` of the prime spectra of `R` and
@@ -1124,7 +1124,7 @@ theorem comap_const (f : R →+* S) (U : Opens (PrimeSpectrum.Top R))
       const (f a) (f b) V fun p hpV => hb (PrimeSpectrum.comap f p) (hUV hpV) :=
   Subtype.ext <| funext fun p => by
     rw [comap_apply, const_apply, const_apply]
-    convert_to Localization.localRingHom _ _ _ _ (Localization.mk _ _) = Localization.mk _ _
+    convert_to! Localization.localRingHom _ _ _ _ (Localization.mk _ _) = Localization.mk _ _
     simp [Localization.mk_eq_mk']
 
 /-- For an inclusion `i : V ⟶ U` between open sets of the prime spectrum of `R`, the comap of the
diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean
@@ -33,7 +33,7 @@ end Path
 namespace FundamentalGroupoid
 
 instance {x y : FundamentalGroupoid PUnit} : Subsingleton (x ⟶ y) := by
-  convert_to Subsingleton (Path.Homotopic.Quotient PUnit.unit PUnit.unit)
+  convert_to! Subsingleton (Path.Homotopic.Quotient PUnit.unit PUnit.unit)
   apply Quotient.instSubsingletonQuotient
 
 /-- Equivalence of groupoids between fundamental groupoid of punit and punit -/
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean
@@ -216,7 +216,7 @@ lemma nonempty_compStruct_iff {x₀ x₁ x₂ : C}
   refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨by rwa [← h]⟩⟩
   rw [← Arrow.mk_inj]
   apply ComposableArrows.arrowEquiv.symm.injective
-  convert_to (nerve C).δ 1 h'.simplex = (nerve C).δ 1 h.simplex
+  convert_to! (nerve C).δ 1 h'.simplex = (nerve C).δ 1 h.simplex
   · exact (h'.d₁).symm
   · exact (h.d₁).symm
   · have h₀ := h.d₀
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@@ -238,7 +238,7 @@ lemma toNNReal_apply (f : C(X, ℝ)₀) (x : X) : f.toNNReal x = Real.toNNReal (
 @[fun_prop]
 lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := by
   rw [continuous_induced_rng]
-  convert_to Continuous (ContinuousMap.toNNReal ∘ ((↑) : C(X, ℝ)₀ → C(X, ℝ))) using 1
+  convert_to! Continuous (ContinuousMap.toNNReal ∘ ((↑) : C(X, ℝ)₀ → C(X, ℝ))) using 1
   exact ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom
 
 lemma toContinuousMapHom_toNNReal (f : C(X, ℝ)₀) :
diff --git a/Mathlib/Analysis/Calculus/Deriv/Inverse.lean b/Mathlib/Analysis/Calculus/Deriv/Inverse.lean
@@ -73,7 +73,7 @@ theorem OpenPartialHomeomorph.hasStrictDerivAt_symm (f : OpenPartialHomeomorph 
 theorem HasDerivAt.of_comp_left {f g h : 𝕜 → 𝕜} {f' h' a : 𝕜} (hst : ContinuousAt g a)
     (hf : HasDerivAt f f' (g a)) (hh : HasDerivAt h h' a) (hf' : f' ≠ 0)
     (hcomp : f ∘ g =ᶠ[𝓝 a] h) : HasDerivAt g (h' / f') a := by
-  convert hf.hasFDerivAt.of_comp_of_leftInverse hst hh hcomp (f'symm := .toSpanSingleton 𝕜 f'⁻¹)
+  convert! hf.hasFDerivAt.of_comp_of_leftInverse hst hh hcomp (f'symm := .toSpanSingleton 𝕜 f'⁻¹)
     (fun _ ↦ by simp [hf']) |>.hasDerivAt using 1
   simp [div_eq_mul_inv]
 
diff --git a/Mathlib/Analysis/Complex/CoveringMap.lean b/Mathlib/Analysis/Complex/CoveringMap.lean
@@ -90,7 +90,7 @@ theorem isCoveringMapOn_zpow (n : ℤ) (hn : (n : 𝕜) ≠ 0) :
   refine .of_isCoveringMap_restrictPreimage _ (by simp) ?_ ?_
   · convert! isClosed_singleton (x := (0 : 𝕜)).isOpen_compl using 1
     ext; simp [this]
-  · convert (isCoveringMap_zpow n hn).comp_homeomorph (.setCongr _) using 1
+  · convert! (isCoveringMap_zpow n hn).comp_homeomorph (.setCongr _) using 1
     ext; simpa using! (this _).not
 
 attribute [-instance] Units.mulAction'
diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@@ -793,7 +793,7 @@ lemma hasDerivAt_fourier
   have h_int : Integrable fun v ↦ fourierSMulRight L f v := by
     suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
       simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using! this.smul (-2 * π * I)
-    convert ((ContinuousLinearMap.toSpanSingletonLIE ℝ
+    convert! ((ContinuousLinearMap.toSpanSingletonLIE ℝ
       E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v
     apply ContinuousLinearMap.ext_ring
     rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply,
diff --git a/Mathlib/Analysis/InnerProductSpace/ProdL2.lean b/Mathlib/Analysis/InnerProductSpace/ProdL2.lean
@@ -149,7 +149,7 @@ def quotientEquivOrthogonal : (E ⧸ K) ≃ₗᵢ[𝕜] ↥Kᗮ where
       coe_norm, starProjection_minimal, eq_comm]
     have h : ‖Quotient.mk (f y).val‖ = sInf ((fun (x : E) ↦ ‖(f y).val + x‖) '' K.toAddSubgroup) :=
       quotient_norm_mk_eq K.toAddSubgroup (f y).1
-    convert h using 2
+    convert! h using 2
     · simp [f]
     · rw [sInf_image', ← Equiv.iInf_comp (Equiv.neg K)]
       simp
diff --git a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
@@ -328,7 +328,7 @@ theorem isOpen_setOf_affineIndependent {ι : Type*} [Finite ι] :
     let ι' := { x // x ≠ i₀ }
     cases nonempty_fintype ι
     haveI : Fintype ι' := Subtype.fintype _
-    convert_to
+    convert_to!
       IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})
     exact isOpen_setOf_linearIndependent.preimage (by fun_prop)
 
diff --git a/Mathlib/Analysis/Normed/Operator/Extend.lean b/Mathlib/Analysis/Normed/Operator/Extend.lean
@@ -195,7 +195,7 @@ theorem extendOfNorm_eq (h_dense : DenseRange e) (h_norm : ∃ C, ∀ x, ‖f x
     (x : E) : f.extendOfNorm e (e x) = f x := by
   have := (f.compLeftInverse e).extend_eq (e := (LinearMap.range e).subtypeL)
     (by simpa using! h_dense) isUniformEmbedding_subtype_val.isUniformInducing
-  convert this ⟨e x, LinearMap.mem_range_self e x⟩
+  convert! this ⟨e x, LinearMap.mem_range_self e x⟩
   exact (compLeftInverse_apply_of_bdd _ _ h_norm _ _ rfl).symm
 
 theorem norm_extendOfNorm_apply_le (h_dense : DenseRange e) (C : ℝ)
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean
@@ -168,7 +168,7 @@ theorem hasFPowerSeriesAt_clog_one :
     HasFPowerSeriesAt log (.ofScalars ℂ (fun n ↦ -(-1 : ℂ) ^ n / n)) 1 := by
   suffices ((FormalMultilinearSeries.ofScalars ℂ (fun n ↦ -(-1 : ℂ) ^ n / n)) =
       FormalMultilinearSeries.ofScalars ℂ (fun n ↦ iteratedDeriv n log 1 / (n.factorial : ℂ))) by
-    convert AnalyticAt.hasFPowerSeriesAt _ using 1 <;> try infer_instance
+    convert! AnalyticAt.hasFPowerSeriesAt _ using 1 <;> try infer_instance
     exact analyticAt_clog (by simp)
   ext n
   simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff, Finset.prod_const_one,
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
@@ -413,7 +413,7 @@ theorem log_doublingGamma_eq :
 
 theorem doublingGamma_log_convex_Ioi : ConvexOn ℝ (Ioi (0 : ℝ)) (log ∘ doublingGamma) := by
   refine (((ConvexOn.add ?_ ?_).add ?_).add_const _).congr log_doublingGamma_eq.symm
-  · convert
+  · convert!
       convexOn_log_Gamma.comp_affineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap
       using 1
     · simpa only [zero_div] using! (preimage_const_mul_Ioi₀ (0 : ℝ) one_half_pos).symm
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean
@@ -76,7 +76,7 @@ private theorem nthRoot.lt_pow_go_succ_aux0 (hb : b ≠ 0) :
     (ha := by positivity) (Hsq := by positivity) (Hsq' := by positivity) (H := by omega)
     (n := n + 1)
   rw [← sub_nonneg] at h ⊢
-  convert h using 1
+  convert! h using 1
   rw [pow_succ]; push_cast; ring1
 
 private theorem nthRoot.always_exists (n a : ℕ) :
diff --git a/Mathlib/CategoryTheory/Category/PartialFun.lean b/Mathlib/CategoryTheory/Category/PartialFun.lean
@@ -174,5 +174,5 @@ noncomputable def typeToPartialFunIsoPartialFunToPointed :
     fun f =>
     Pointed.Hom.ext <|
       funext fun a => Option.recOn a rfl fun a => by
-        convert Part.some_toOption _
+        convert! Part.some_toOption _
         simpa using! (Part.get_eq_iff_mem (by trivial)).mp rfl
diff --git a/Mathlib/CategoryTheory/Galois/Decomposition.lean b/Mathlib/CategoryTheory/Galois/Decomposition.lean
@@ -256,7 +256,7 @@ private lemma selfProdTermIncl_fib_eq (b : F.obj A) :
   · simp only [selfProdProj, map_comp, FintypeCat.comp_apply]; rfl
   · dsimp only [selfProdPermIncl, Pi.whiskerEquiv]
     rw [map_comp, FintypeCat.comp_apply, h]
-    convert_to F.map (selfProdProj u t) b =
+    convert_to! F.map (selfProdProj u t) b =
       (F.map (Pi.map' (fiberPerm h b) fun _ ↦ 𝟙 X) ≫
       F.map (Pi.π (fun _ ↦ X) t)) (mkSelfProdFib F X)
     rw [← map_comp, Pi.map'_comp_π, Category.comp_id, mkSelfProdFib_map_π F X (fiberPerm h b t)]
diff --git a/Mathlib/Combinatorics/SimpleGraph/Trails.lean b/Mathlib/Combinatorics/SimpleGraph/Trails.lean
@@ -130,7 +130,7 @@ theorem IsEulerian.even_degree_iff {x u v : V} {p : G.Walk u v} (ht : p.IsEuleri
   rw [← Multiset.coe_countP, Multiset.countP_eq_card_filter, ← card_incidenceFinset_eq_degree]
   change Multiset.card _ = _
   congr 1
-  convert_to _ = (ht.isTrail.edgesFinset.filter (x ∈ ·)).val
+  convert_to! _ = (ht.isTrail.edgesFinset.filter (x ∈ ·)).val
   rw [ht.edgesFinset_eq, G.incidenceFinset_eq_filter x]
 
 theorem IsEulerian.card_filter_odd_degree [Fintype V] [DecidableRel G.Adj] {u v : V}
diff --git a/Mathlib/Data/Finsupp/BigOperators.lean b/Mathlib/Data/Finsupp/BigOperators.lean
@@ -101,7 +101,7 @@ theorem Multiset.support_sum_eq [AddCommMonoid M] (s : Multiset (ι →₀ M))
   induction s using Quot.inductionOn with | _ a
   obtain ⟨l, hl, hd⟩ := hs
   suffices a.Pairwise (_root_.Disjoint on Finsupp.support) by
-    convert List.support_sum_eq a this
+    convert! List.support_sum_eq a this
     simp only [quot_mk_to_coe'', map_coe, sup_coe,
       Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]
   simp only [Multiset.quot_mk_to_coe'', Multiset.coe_eq_coe] at hl
diff --git a/Mathlib/FieldTheory/IntermediateField/ExtendRight.lean b/Mathlib/FieldTheory/IntermediateField/ExtendRight.lean
@@ -87,7 +87,7 @@ noncomputable instance algebra : Algebra S (F.extendRight M) where
   algebraMap := (algebraMap S M).codRestrict (F.extendRight M).toSubalgebra (algebraMap_mem F M ·)
   commutes' _ _ := Subtype.ext <| by simp [Algebra.commutes]
   smul_def' s x := Subtype.ext <| by
-    convert_to s • (x : M) = _
+    convert_to! s • (x : M) = _
     rw [MulMemClass.coe_mul, RingHom.codRestrict_apply, ← Algebra.smul_def]
 
 -- Check there is no diamond
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean b/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
@@ -510,15 +510,15 @@ lemma mvfderivWithin_smul {a : M → 𝕜} (ha : MDiffAt[s] a x) {g : M → F} (
     d[s](a • g) x =
       a x • d[s] g x + (d[s] a x).smulRight (g x) := by
   refine HasMFDerivWithinAt.mfderivWithin ⟨ha.1.smul hg.1, ?_⟩ hs
-  convert ha.hasMFDerivWithinAt.2.smul hg.hasMFDerivWithinAt.2
+  convert! ha.hasMFDerivWithinAt.2.smul hg.hasMFDerivWithinAt.2
   simp
   rfl
 
 @[simp, to_fun mvfderivWithin_fun_mul]
 lemma mvfderivWithin_mul {f g : M → 𝕜} {x : M} (hf : MDiffAt[s] f x) (hg : MDiffAt[s] g x)
     (hs : UniqueMDiffWithinAt I s x) :
     d[s](f * g) x = f x • d[s]g x + (g x) • (d[s]f x) := by
-  convert mvfderivWithin_smul hf hg hs
+  convert! mvfderivWithin_smul hf hg hs
   ext v
   simp [mul_comm]
 
diff --git a/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean b/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
@@ -124,7 +124,7 @@ theorem exists_int_int_abs_mul_sub_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
     refine
       ⟨⌊ξ * y⌋ - ⌊ξ * x⌋, y - x, sub_pos_of_lt x_lt_y,
         sub_le_iff_le_add.mpr <| le_add_of_le_of_nonneg (mem_Icc.mp hy).2 (mem_Icc.mp hx).1, ?_⟩
-    convert_to |fract (ξ * y) * (n + 1) - fract (ξ * x) * (n + 1)| ≤ 1
+    convert_to! |fract (ξ * y) * (n + 1) - fract (ξ * x) * (n + 1)| ≤ 1
     · congr; push_cast; simp only [fract]; ring
     exact (abs_sub_lt_one_of_floor_eq_floor hxy.symm).le
 
diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
@@ -681,7 +681,7 @@ theorem rat_dense' (q : ℚ_[p]) {ε : ℚ} (hε : 0 < ε) : ∃ r : ℚ, padicN
     ⟨q' N, by
       classical
       dsimp [padicNormE]
-      convert_to PadicSeq.norm (q' - const _ (q' N)) < ε -- `change` times out here.
+      convert_to! PadicSeq.norm (q' - const _ (q' N)) < ε -- `change` times out here.
       rcases Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq | hne'
       · simpa only [heq, PadicSeq.norm, dif_pos]
       · simp only [PadicSeq.norm, dif_neg hne']
diff --git a/Mathlib/Order/Filter/AtTopBot/Finite.lean b/Mathlib/Order/Filter/AtTopBot/Finite.lean
@@ -136,7 +136,7 @@ theorem eventually_pow_lt_factorial_sub (c d : ℕ) : ∀ᶠ n in atTop, c ^ n <
   obtain (rfl | c0) := c.eq_zero_or_pos
   · simp [Nat.two_mul, ← Nat.add_assoc, Nat.add_right_comm _ 1, Nat.factorial_pos]
   refine (Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d') c0)).trans_lt ?_
-  convert_to (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
+  convert_to! (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
   · rw [← pow_mul, ← pow_add]
     congr 1
     lia
diff --git a/Mathlib/Order/RelSeries.lean b/Mathlib/Order/RelSeries.lean
@@ -995,8 +995,8 @@ theorem exists_relSeries_covBy
         obtain rfl : m = 0 := by simpa [t₃] using! (congr_arg Fin.val eq).trans_lt (i j).2
         cases (h (.last _)).ne' (h₂.symm.trans h₁)
     · refine funext (Fin.lastCases ?_ fun j ↦ ?_)
-      · convert h₂; simpa using! RelSeries.last_smash ..
-      convert congr_fun ht j using 1
+      · convert! h₂; simpa using! RelSeries.last_smash ..
+      convert! congr_fun ht j using 1
       simp [RelSeries.smash_castLE]
     all_goals simp [Fin.snoc, Fin.castPred_zero, hi₁]
 
diff --git a/Mathlib/RepresentationTheory/Action.lean b/Mathlib/RepresentationTheory/Action.lean
@@ -154,7 +154,7 @@ lemma μ_comp_assoc : ((linearizeMap (α_ X Y Z).hom).comp
     TensorProduct.assoc_tmul, LinearMap.lTensor_tmul, toLinearMap_apply]
   -- after fixing the defeq problems in `Action` and in the monoidal category structure of `types`
   -- this line should close the goal so this is left as an indicator.
-  with_reducible convert! dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)
+  convert dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)
   all_goals with_reducible simp
 
 variable (X) in
diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
@@ -830,7 +830,7 @@ lemma val_awayMap_eq_aux (a) : (awayMap 𝒜 hg hx a).val = awayMapAux 𝒜 ⟨_
   let e := RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x))
     (h := (val_injective _).hasLeftInverse.choose_spec)
   dsimp [awayMap]
-  convert_to (e (e.symm ⟨awayMapAux 𝒜 (f := f) ⟨_, hx⟩ a,
+  convert_to! (e (e.symm ⟨awayMapAux 𝒜 (f := f) ⟨_, hx⟩ a,
     range_awayMapAux_subset 𝒜 hg hx ⟨_, rfl⟩⟩)).1 = _
   rw [e.apply_symm_apply]
 
diff --git a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
@@ -320,7 +320,7 @@ lemma Ideal.exists_finset_card_eq_height_of_isNoetherianRing (p : Ideal R) [p.Is
   refine le_antisymm ?_ ?_
   · rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I)] at hr
     exact Cardinal.nat_le_ofENat.mp hr
-  · convert_to p.height ≤ I.spanRank.toENat
+  · convert_to! p.height ≤ I.spanRank.toENat
     · symm
       simpa [Submodule.fg_iff_spanRank_eq_spanFinrank] using (IsNoetherian.noetherian I)
     · exact I.height_le_spanRank_toENat_of_mem_minimalPrimes _ hI
diff --git a/Mathlib/RingTheory/Localization/Algebra.lean b/Mathlib/RingTheory/Localization/Algebra.lean
@@ -78,7 +78,7 @@ is localizing. In other words, localization commutes with taking kernels. -/
 lemma RingHom.toKerIsLocalization_isLocalizedModule (hT : Submonoid.map g M = T) :
     IsLocalizedModule M (toKerIsLocalization S Q g (hT.symm ▸ Submonoid.le_comap_map M)) := by
   let e := LinearEquiv.ofEq _ _ (IsLocalization.ker_map (S := S) Q g hT).symm
-  convert_to IsLocalizedModule M ((e.restrictScalars R).toLinearMap ∘ₗ
+  convert_to! IsLocalizedModule M ((e.restrictScalars R).toLinearMap ∘ₗ
     Algebra.idealMap S (RingHom.ker g))
   apply IsLocalizedModule.of_linearEquiv
 
diff --git a/Mathlib/RingTheory/Polynomial/GaussNorm.lean b/Mathlib/RingTheory/Polynomial/GaussNorm.lean
@@ -242,7 +242,7 @@ private theorem mul_gaussNorm_le_gaussNorm_mul (p q : R[X]) :
   intro x hx hneq
   apply lt_of_mul_lt_mul_right _ <| pow_nonneg hc0 (i + j)
   have : x + (i + j - x) = i + j := by simp_all
-  convert_to v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) <
+  convert_to! v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) <
     v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)
   · grind
   · grind
diff --git a/Mathlib/RingTheory/Polynomial/Vieta.lean b/Mathlib/RingTheory/Polynomial/Vieta.lean
@@ -161,7 +161,7 @@ theorem MvPolynomial.prod_X_add_C_coeff (k : ℕ) (h : k ≤ card σ) :
     rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
   rw [this] at h ⊢
   rw [MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
-  convert Multiset.prod_X_add_C_coeff s h
+  convert! Multiset.prod_X_add_C_coeff s h
   simp_rw [s, Multiset.map_map, Function.comp_apply]
 
 end MvPolynomial
diff --git a/Mathlib/RingTheory/PowerSeries/PiTopology.lean b/Mathlib/RingTheory/PowerSeries/PiTopology.lean
@@ -326,7 +326,7 @@ variable {R}
 theorem hasSum_of_monomials_self (f : PowerSeries R) :
     HasSum (fun d : ℕ => monomial d (coeff d f)) f := by
   rw [← (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.hasSum_iff]
-  convert MvPowerSeries.WithPiTopology.hasSum_of_monomials_self f
+  convert! MvPowerSeries.WithPiTopology.hasSum_of_monomials_self f
   simp only [LinearEquiv.coe_toEquiv, comp_apply, monomial, coeff]
   congr
   all_goals { ext; simp }
diff --git a/Mathlib/RingTheory/Valuation/ExtendToLocalization.lean b/Mathlib/RingTheory/Valuation/ExtendToLocalization.lean
diff --git a/Mathlib/RingTheory/Valuation/ValuationSubring.lean b/Mathlib/RingTheory/Valuation/ValuationSubring.lean
diff --git a/Mathlib/Tactic/CongrExclamation.lean b/Mathlib/Tactic/CongrExclamation.lean
diff --git a/Mathlib/Tactic/Convert.lean b/Mathlib/Tactic/Convert.lean
diff --git a/Mathlib/Topology/Category/TopCat/Limits/Products.lean b/Mathlib/Topology/Category/TopCat/Limits/Products.lean
diff --git a/MathlibTest/Tactic/Convert/Basic.lean b/MathlibTest/Tactic/Convert/Basic.lean
diff --git a/MathlibTest/Tactic/Convert/Bugfix7945.lean b/MathlibTest/Tactic/Convert/Bugfix7945.lean
diff --git a/MathlibTest/ValuedCSP.lean b/MathlibTest/ValuedCSP.lean
