Fixes

Vierkantor · Vierkantor · commit 835153f6c895 · 2026-05-13T12:32:28.000+02:00
diff --git a/Mathlib/Algebra/Module/GradedModule.lean b/Mathlib/Algebra/Module/GradedModule.lean
@@ -224,6 +224,5 @@ def linearEquiv [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] [DirectSum
     (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j)) from DirectSum.Gmodule.smul_def _ _ _ _]
   simp only [decomposeAddEquiv_apply, decompose_coe, Gmodule.smulAddMonoidHom_apply_of_of]
   convert! DirectSum.decompose_coe 𝓜 _
-  rfl
 
 end GradedModule
diff --git a/Mathlib/Algebra/Module/LocalizedModule/Basic.lean b/Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@@ -491,7 +491,6 @@ noncomputable def divBy (s : S) : LocalizedModule S M →ₗ[R] LocalizedModule
     refine x.induction_on (fun _ _ ↦ ?_)
     simp_rw [smul'_mk, liftOn_mk, smul'_mk]
     congr!
-    simp
 
 theorem divBy_mul_by (s : S) (p : LocalizedModule S M) :
     divBy s (algebraMap R (Module.End R (LocalizedModule S M)) s p) = p :=
diff --git a/Mathlib/Algebra/Polynomial/Splits.lean b/Mathlib/Algebra/Polynomial/Splits.lean
@@ -467,7 +467,6 @@ lemma map_sub_sprod_roots_eq_prod_map_eval
   conv_rhs => rw [this]
   simp_rw [eval_multiset_prod, Multiset.prod_map_product_eq_prod_prod, Multiset.map_map]
   congr! with x hx
-  · rfl
   ext; simp
 
 lemma map_sub_roots_sprod_eq_prod_map_eval
diff --git a/Mathlib/AlgebraicGeometry/FunctionField.lean b/Mathlib/AlgebraicGeometry/FunctionField.lean
@@ -129,7 +129,7 @@ theorem IsAffineOpen.primeIdealOf_genericPoint {X : Scheme} [IsIntegral X] {U :
           ((genericPoint_spec X).mem_open_set_iff U.isOpen).mpr (by simpa using h)⟩ =
       genericPoint (Spec Γ(X, U)) := by
   delta IsAffineOpen.primeIdealOf
-  convert
+  convert!
     genericPoint_eq_of_isOpenImmersion
       (U.toScheme.isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op))
   -- Porting note: this was `ext1`
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean b/Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
@@ -111,7 +111,6 @@ theorem HasAffineProperty.diagonal_of_diagonal_of_isPullback
   convert! HasAffineProperty.of_isPullback (P := P) (.of_hasPullback _ _) H
   · apply pullback.hom_ext <;> simp
   · infer_instance
-  · infer_instance
 
 theorem HasAffineProperty.diagonal_iff
     (P) {Q} [HasAffineProperty P Q] {X Y : Scheme.{u}} {f : X ⟶ Y} [IsAffine Y] :
diff --git a/Mathlib/AlgebraicGeometry/Normalization.lean b/Mathlib/AlgebraicGeometry/Normalization.lean
@@ -237,7 +237,7 @@ lemma toNormalization_app_preimage (U : Y.affineOpens) :
   have H : f.toNormalization ⁻¹ᵁ f.fromNormalization ⁻¹ᵁ U =
       (f ⁻¹ᵁ U).ι ''ᵁ (((f ⁻¹ᵁ U).ι ≫ f.toNormalization) ⁻¹ᵁ f.fromNormalization ⁻¹ᵁ U) := by
     simp [← Scheme.Hom.comp_preimage]
-  convert! congr($(Scheme.Hom.congr_app (f.ι_toNormalization U) (f.fromNormalization ⁻¹ᵁ U)) ≫
+  convert congr($(Scheme.Hom.congr_app (f.ι_toNormalization U) (f.fromNormalization ⁻¹ᵁ U)) ≫
     X.presheaf.map (eqToHom H).op) using 1
   · simp [Hom.app_eq_appLE]
   dsimp
diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean
@@ -969,7 +969,7 @@ def Localizations.comapFun (y : PrimeSpectrum.Top S) :
       have := IsLocalizedModule.map_units (S := y.asIdeal.primeCompl)
         (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ⟨σ x, x.2⟩
       rw [Module.End.isUnit_iff] at this ⊢
-      convert! this using 2 with a
+      convert this using 2 with a
       exact (IsScalarTower.algebraMap_smul ..).symm)
   { __ := g,
     map_smul' r x := by simpa [Localizations] using (IsScalarTower.algebraMap_smul ..).symm }
diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
@@ -548,11 +548,11 @@ theorem filter_true : (π.filter fun _ => True) = π :=
 theorem iUnion_filter_not (π : Prepartition I) (p : Box ι → Prop) :
     (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion := by
   simp only [Prepartition.iUnion]
-  convert
+  convert!
     (@Set.biUnion_diff_biUnion_eq (ι → ℝ) (Box ι) π.boxes (π.filter p).boxes (↑) _).symm using 4
   · simp +contextual
   · rw [Set.PairwiseDisjoint]
-    convert! π.pairwiseDisjoint
+    convert π.pairwiseDisjoint
     rw [Set.union_eq_left, filter_boxes, coe_filter]
     exact fun _ ⟨h, _⟩ => h
 
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Operations.lean b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
@@ -79,7 +79,7 @@ theorem hasFTaylorSeriesUpToOn_pi' {n : ℕ∞ω} :
       ∀ i, HasFTaylorSeriesUpToOn n (fun x => Φ x i)
         (fun x m => (@ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _ i).compContinuousMultilinearMap
           (P' x m)) s := by
-  convert! hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i); ext; rfl
+  convert! hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i)
 
 theorem contDiffWithinAt_pi :
     ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x := by
diff --git a/Mathlib/Analysis/Complex/Exponential.lean b/Mathlib/Analysis/Complex/Exponential.lean
@@ -93,7 +93,7 @@ variable (x y : ℂ)
 theorem exp_zero : exp 0 = 1 := by
   rw [exp]
   refine lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => ?_⟩
-  convert! (config := .unfoldSameFun) ε0 -- ε0 : ε > 0 but goal is _ < ε
+  convert (config := { __ := Congr!.Config.unfoldSameFun }) ε0 -- ε0 : ε > 0 but goal is _ < ε
   rcases j with - | j
   · exact absurd hj (not_le_of_gt zero_lt_one)
   · dsimp [exp']
diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean
@@ -259,7 +259,7 @@ theorem coeFn_fourierLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (n : ℤ) :
 `Lp ℂ p haarAddCircle`. -/
 theorem span_fourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p ≠ ∞) :
     (span ℂ (range (@fourierLp T _ p _))).topologicalClosure = ⊤ := by
-  convert
+  convert!
     (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) ℂ hp).topologicalClosure_map_submodule
       span_fourier_closure_eq_top
   rw [map_span]
diff --git a/Mathlib/Analysis/Fourier/Convolution.lean b/Mathlib/Analysis/Fourier/Convolution.lean
@@ -60,7 +60,6 @@ theorem integrable_prod_sub (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {f₁ : E
   rw [integral_mul_const]
   congr 1
   convert! integral_sub_right_eq_self _ x (μ := volume)
-  rfl
 
 open FourierTransform
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
@@ -200,7 +200,7 @@ alias ⟨_, _root_.Set.Countable.preimage_cexp⟩ := countable_preimage_exp
 
 theorem tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0)
     (him : z.im = 0) : Tendsto log (𝓝[{ z : ℂ | z.im < 0 }] z) (𝓝 <| Real.log ‖z‖ - π * I) := by
-  convert
+  convert!
     (continuous_ofReal.continuousAt.comp_continuousWithinAt
             (continuous_norm.continuousWithinAt.log _)).tendsto.add
       (((continuous_ofReal.tendsto _).comp <|
@@ -212,7 +212,7 @@ theorem tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re
 
 theorem continuousWithinAt_log_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :
     ContinuousWithinAt log { z : ℂ | 0 ≤ z.im } z := by
-  convert
+  convert!
     (continuous_ofReal.continuousAt.comp_continuousWithinAt
             (continuous_norm.continuousWithinAt.log _)).tendsto.add
       ((continuous_ofReal.continuousAt.comp_continuousWithinAt <|
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
@@ -354,7 +354,7 @@ theorem Gamma_strictAntiOn_Ioc : StrictAntiOn Gamma (Ioc 0 1) :=
     Gamma_one.symm ▸ Gamma_three_div_two_lt_one
 
 theorem Gamma_strictMonoOn_Ici : StrictMonoOn Gamma (Ici 2) := by
-  convert
+  convert!
     convexOn_Gamma.strictMonoOn (by simp : (0 : ℝ) < 3 / 2)
       (by norm_num : (3 / 2 : ℝ) < 2) (Gamma_two.symm ▸ Gamma_three_div_two_lt_one)
   symm
@@ -416,15 +416,15 @@ 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
     · ext1 x
       simp only [LinearMap.coe_toAffineMap, Function.comp_apply, DistribSMul.toLinearMap_apply]
       rw [smul_eq_mul, mul_comm, mul_one_div]
   · refine ConvexOn.subset ?_ (Ioi_subset_Ioi <| neg_one_lt_zero.le) (convex_Ioi _)
-    convert
+    convert!
       convexOn_log_Gamma.comp_affineMap
         ((DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap +
           AffineMap.const ℝ ℝ (1 / 2 : ℝ)) using 1
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
@@ -1268,7 +1268,7 @@ theorem sinh_add_pi_mul_I (z : ℂ) : sinh (z + π * I) = -sinh z :=
   sinh_antiperiodic z
 
 theorem sinh_periodic : Function.Periodic sinh (2 * π * I) := by
-  convert sinh_antiperiodic.periodic_two_mul using 1
+  convert! sinh_antiperiodic.periodic_two_mul using 1
   ring
 
 @[simp]
@@ -1283,7 +1283,7 @@ theorem cosh_add_pi_mul_I (z : ℂ) : cosh (z + π * I) = -cosh z :=
   cosh_antiperiodic z
 
 theorem cosh_periodic : Function.Periodic cosh (2 * π * I) := by
-  convert cosh_antiperiodic.periodic_two_mul using 1
+  convert! cosh_antiperiodic.periodic_two_mul using 1
   ring
 
 @[simp]
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean
@@ -102,7 +102,7 @@ theorem abs_eval_T_real_eq_one_iff {n : ℕ} (hn : n ≠ 0) (x : ℝ) :
       gcongr
       exact div_le_one_of_le₀ (arccos_le_pi x) (by positivity)
     refine ⟨k, by simpa using hkn, ?_⟩
-    convert! congr(cos ($hk.symm / n))
+    convert congr(cos ($hk.symm / n))
     rw [mul_div_cancel_left₀ _ (by simpa), cos_arccos (by grind) (by grind)]
   · rintro ⟨k, hk, rfl⟩
     rw [T_real_cos, abs_cos_eq_one_iff]
diff --git a/Mathlib/CategoryTheory/Abelian/Basic.lean b/Mathlib/CategoryTheory/Abelian/Basic.lean
@@ -380,7 +380,7 @@ set_option backward.isDefEq.respectTransparency false in
 See `CategoryTheory.Abelian.ofCoimageImageComparisonIsIso` for the converse.
 -/
 instance : IsIso (coimageImageComparison f) := by
-  convert
+  convert!
     Iso.isIso_hom
       (IsImage.isoExt (coimageStrongEpiMonoFactorisation f).toMonoIsImage
         (imageStrongEpiMonoFactorisation f).toMonoIsImage)
diff --git a/Mathlib/CategoryTheory/Filtered/Basic.lean b/Mathlib/CategoryTheory/Filtered/Basic.lean
@@ -685,7 +685,8 @@ theorem _root_.CategoryTheory.Functor.ranges_directed (F : C ⥤ Type*) (j : C)
   let ⟨l, li, lk, e⟩ := cospan ij kj
   refine ⟨⟨l, lk ≫ kj⟩, e ▸ ?_, ?_⟩ <;>
     simp_rw [F.map_comp] <;>
-    convert! Set.range_comp_subset_range _ _
+    convert Set.range_comp_subset_range _ _ <;>
+    rfl
 
 /-- Given a "bowtie" of morphisms
 ```
diff --git a/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean b/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
@@ -138,7 +138,7 @@ theorem matrixDecomposition_id (o : HomOrthogonal s) {α : Type} [Finite α] {f
   · cases h
     simp
   · simp only [Subtype.mk.injEq] at h
-    convert! comp_zero
+    convert comp_zero
     simpa using biproduct.ι_π_ne _ (Ne.symm h)
 
 set_option backward.isDefEq.respectTransparency false in
@@ -159,10 +159,10 @@ theorem matrixDecomposition_comp (o : HomOrthogonal s) {α β γ : Type} [Finite
   · intro b nm
     simp only [Set.mem_preimage, Set.mem_singleton_iff] at nm
     simp only [Category.assoc]
-    convert! comp_zero
-    convert! comp_zero
-    convert! comp_zero
-    convert! comp_zero
+    convert comp_zero
+    convert comp_zero
+    convert comp_zero
+    convert comp_zero
     simp only [o.eq_zero nm]
 
 section
diff --git a/Mathlib/Combinatorics/SimpleGraph/Trails.lean b/Mathlib/Combinatorics/SimpleGraph/Trails.lean
@@ -126,11 +126,12 @@ theorem IsEulerian.edgesFinset_eq [Fintype G.edgeSet] {u v : V} {p : G.Walk u v}
 
 theorem IsEulerian.even_degree_iff {x u v : V} {p : G.Walk u v} (ht : p.IsEulerian) [Fintype V]
     [DecidableRel G.Adj] : Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v := by
-  convert! ht.isTrail.even_countP_edges_iff x
+  convert ht.isTrail.even_countP_edges_iff x
   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
+  · rfl
   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/PNat/Factors.lean b/Mathlib/Data/PNat/Factors.lean
@@ -374,7 +374,6 @@ theorem count_factorMultiset (m : ℕ+) (p : Nat.Primes) (k : ℕ) :
   rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow,
     factorMultiset_ofPrime]
   congr! 2
-  · rfl
   apply Multiset.eq_replicate.mpr
   constructor
   · rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]
diff --git a/Mathlib/Data/Real/ConjExponents.lean b/Mathlib/Data/Real/ConjExponents.lean
@@ -152,7 +152,7 @@ theorem sub_one_pos : 0 < p - 1 := sub_pos.2 h.lt
 theorem sub_one_ne_zero : p - 1 ≠ 0 := h.sub_one_pos.ne'
 
 theorem conjugate_eq : q = p / (p - 1) := by
-  convert! inv_inv q ▸ congr($(h.symm.inv_sub_inv_eq_inv.symm)⁻¹) using 1
+  convert inv_inv q ▸ congr($(h.symm.inv_sub_inv_eq_inv.symm)⁻¹) using 1
   field [h.ne_zero]
 
 lemma conjExponent_eq : conjExponent p = q := h.conjugate_eq.symm
diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean
@@ -498,9 +498,9 @@ theorem range_mfderiv_coe_sphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : s
       (ℝ ∙ (↑(-v) : E))ᗮ.subtypeL (U.symm 0) := by
     convert! hasFDerivAt_stereoInvFunAux_comp_coe (-v : E)
     simp
-  convert! congr($((this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv).range)
+  convert congr($((this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv).range)
   symm
-  convert
+  convert!
     (U.symm : EuclideanSpace ℝ (Fin n) ≃ₗᵢ[ℝ] (ℝ ∙ (↑(-v) : E))ᗮ).range_comp
       (ℝ ∙ (↑(-v) : E))ᗮ.subtype using 1
   simp only [Submodule.range_subtype, coe_neg_sphere]
diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
@@ -444,7 +444,7 @@ theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) :
     iterate 3 rw [← Functor.map_comp_assoc]
     rw [NatTrans.naturality_assoc]
     erw [← (D.V (i, j)).presheaf.map_comp]
-    convert
+    convert!
       limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
         (Quiver.Hom.op (WalkingMultispan.Hom.fst (i, j)))
   · rw [Category.comp_id]
diff --git a/Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean b/Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean
@@ -129,7 +129,6 @@ instance actionGroupoidIsFree {G A : Type u} [Group G] [IsFreeGroup G] [MulActio
         intro e
         ext
         · convert! hE _ _ _
-          rfl
         · rfl
       apply Functor.hext
       · intro
diff --git a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
@@ -173,7 +173,7 @@ theorem MemLp.exists_hasCompactSupport_eLpNorm_sub_le
   rcases exists_continuous_eLpNorm_sub_le_of_closed hp s_closed isOpen_interior sk hsμ.ne c δpos.ne'
     with ⟨f, f_cont, I2, _f_bound, f_support, f_mem⟩
   have I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε := by
-    convert
+    convert!
       (hδ _ _
           (f_mem.aestronglyMeasurable.sub
             (aestronglyMeasurable_const.indicator s_closed.measurableSet))
@@ -270,7 +270,7 @@ theorem MemLp.exists_boundedContinuous_eLpNorm_sub_le [μ.WeaklyRegular] (hp : p
       δpos.ne' with
     ⟨f, f_cont, I2, f_bound, -, f_mem⟩
   have I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε := by
-    convert
+    convert!
       (hδ _ _
           (f_mem.aestronglyMeasurable.sub
             (aestronglyMeasurable_const.indicator s_closed.measurableSet))
diff --git a/Mathlib/MeasureTheory/Group/Prod.lean b/Mathlib/MeasureTheory/Group/Prod.lean
@@ -234,7 +234,7 @@ theorem measure_mul_lintegral_eq [IsMulLeftInvariant ν] (sm : MeasurableSet s)
     fun x => measurable_const.indicator (measurable_mul_const _ sm)
   have : ∀ x y, s.indicator (fun _ : G => (1 : ℝ≥0∞)) (y * x) =
       ((fun z => z * x) ⁻¹' s).indicator (fun b : G => 1) y := by
-    intro x y; symm; convert! indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2; ext1; rfl
+    intro x y; symm; convert! indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2
   simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator (measurable_mul_const _ sm),
     setLIntegral_one]
 
diff --git a/Mathlib/MeasureTheory/Measure/Dirac.lean b/Mathlib/MeasureTheory/Measure/Dirac.lean
@@ -162,9 +162,7 @@ lemma exists_sum_smul_dirac [Countable α] (μ : Measure α) :
       congr 1
       refine (measurableAtom_eq_of_mem ?_).symm
       convert! h_points_mem _
-      simp
     · convert! h_points_mem _
-      simp
   · simp only [ne_eq, mul_eq_zero, indicator_apply_eq_zero, Pi.one_apply, one_ne_zero, imp_false,
       Subtype.forall, Set.mem_range, Subtype.exists, Subtype.mk.injEq, forall_exists_index]
     refine fun y s hs hsy hyx ↦ .inr fun hyx' ↦ hyx ?_
diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean
@@ -624,7 +624,7 @@ theorem hausdorffMeasure_zero_singleton (x : X) : μH[0] ({x} : Set X) = 1 := by
         ⨅ (t : ℕ → Set X) (_ : {x} ⊆ ⋃ n, t n) (_ : ∀ n, ediam (t n) ≤ 1),
           ∑' n, ⨆ _ : (t n).Nonempty, ediam (t n) ^ (0 : ℝ) by
       apply le_trans this _
-      convert! le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one
+      convert le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one
       rfl
     simp only [ENNReal.rpow_zero, le_iInf_iff]
     intro t hst _
diff --git a/Mathlib/MeasureTheory/Measure/Support.lean b/Mathlib/MeasureTheory/Measure/Support.lean
@@ -130,7 +130,7 @@ lemma compl_support_eq_sUnion : μ.supportᶜ = ⋃₀ {t : Set X | IsOpen t ∧
     nhds_basis_opens x |>.notMem_measureSupport, fun t ↦ and_comm (b := x ∈ t)]
 
 lemma support_eq_sInter : μ.support = ⋂₀ {t : Set X | IsClosed t ∧ μ tᶜ = 0} := by
-  convert! congr($(compl_support_eq_sUnion (μ := μ))ᶜ)
+  convert congr($(compl_support_eq_sUnion (μ := μ))ᶜ)
   all_goals simp [Set.compl_sUnion, compl_involutive.image_eq_preimage_symm]
 
 section Lindelof
diff --git a/Mathlib/NumberTheory/LegendreSymbol/Basic.lean b/Mathlib/NumberTheory/LegendreSymbol/Basic.lean
@@ -128,7 +128,7 @@ theorem eq_pow (a : ℤ) : (legendreSym p a : ZMod p) = (a : ZMod p) ^ (p / 2) :
       generalize (a : ZMod 2) = b; fin_cases b
       · tauto
       · simp
-  · convert quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)
+  · convert! quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)
     exact (card p).symm
 
 /-- If `p ∤ a`, then `legendreSym p a` is `1` or `-1`. -/
diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean
@@ -152,7 +152,7 @@ theorem tendsto_normSq_coprime_pair :
       simp only [ofReal_im, ofReal_re, mul_im, zero_add, mul_zero]
   have hf' : IsClosedEmbedding f := f.isClosedEmbedding_of_injective hf
   have h₂ : Tendsto (fun p : Fin 2 → ℤ => ((↑) : ℤ → ℝ) ∘ p) cofinite (cocompact _) := by
-    convert Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite
+    convert! Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite
     · rw [coprodᵢ_cofinite]
     · rw [coprodᵢ_cocompact]
   exact tendsto_normSq_cocompact_atTop.comp (hf'.tendsto_cocompact.comp h₂)
@@ -217,7 +217,7 @@ theorem tendsto_lcRow0 {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) :
       LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin,
       val_planeConformalMatrix, neg_neg, mulVecLin_apply, mulVec, dotProduct, Fin.sum_univ_two,
       cons_val_one, mB, f₁]
-  · convert congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm using 1
+  · convert! congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm using 1
     simp only [Fin.zero_eta, Function.comp_apply, lcRow0Extend_apply, cons_val_zero,
       LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin,
       mulVecLin_apply, mulVec, dotProduct, det_fin_two, f₁]
@@ -259,7 +259,7 @@ theorem tendsto_abs_re_smul {p : Fin 2 → ℤ} (hp : IsCoprime (p 0) (p 1)) :
   let f := Homeomorph.mulRight₀ _ this
   let ff := Homeomorph.addRight
     (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1))).re
-  convert (f.trans ff).isClosedEmbedding.tendsto_cocompact.comp (tendsto_lcRow0 hp) with _ _ g
+  convert! (f.trans ff).isClosedEmbedding.tendsto_cocompact.comp (tendsto_lcRow0 hp) with _ _ g
   change
     ((g : SL(2, ℤ)) • z).re =
       lcRow0 p ↑(↑g : SL(2, ℝ)) / ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2) +
diff --git a/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean b/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
@@ -160,7 +160,7 @@ theorem Gamma1_mem (N : ℕ) (A : SL(2, ℤ)) : A ∈ Gamma1 N ↔
     rw [Gamma1_to_Gamma0_mem] at hx
     simp only [Subgroup.mem_top, true_and] at hxx
     rw [← hxx]
-    convert hx
+    convert! hx
   · intro ha
     simp_rw [Gamma1, Subgroup.mem_map]
     have hA : A ∈ Gamma0 N := by simp [ha.right.right, Gamma0_mem]
diff --git a/Mathlib/NumberTheory/ModularForms/Derivative.lean b/Mathlib/NumberTheory/ModularForms/Derivative.lean
@@ -164,7 +164,7 @@ If `F : ℍ → ℂ` is MDifferentiable, then `serreDerivative k F` is also MDif
 theorem serreDerivative_mdifferentiable {F : ℍ → ℂ} (k : ℂ) (hF : MDiff F) :
     MDiff (serreDerivative k F) := by
   refine (normalizedDerivOfComplex_mdifferentiable hF).sub ?_
-  convert
+  convert!
     (MDifferentiable.mul mdifferentiable_const (E2_mdifferentiable.mul hF) :
       MDiff (fun z ↦ (k * 12⁻¹) * (EisensteinSeries.E2 z * F z)))
   simp [Pi.mul_apply, mul_assoc, mul_left_comm, mul_comm]
diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean
diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
diff --git a/Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean b/Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean
diff --git a/Mathlib/NumberTheory/ModularForms/QExpansion.lean b/Mathlib/NumberTheory/ModularForms/QExpansion.lean
diff --git a/Mathlib/NumberTheory/Padics/Hensel.lean b/Mathlib/NumberTheory/Padics/Hensel.lean
diff --git a/Mathlib/NumberTheory/PrimeCounting.lean b/Mathlib/NumberTheory/PrimeCounting.lean
diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean
diff --git a/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean b/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
diff --git a/Mathlib/RingTheory/Smooth/IntegralClosure.lean b/Mathlib/RingTheory/Smooth/IntegralClosure.lean
diff --git a/Mathlib/RingTheory/SurjectiveOnStalks.lean b/Mathlib/RingTheory/SurjectiveOnStalks.lean
diff --git a/Mathlib/RingTheory/TensorProduct/Finite.lean b/Mathlib/RingTheory/TensorProduct/Finite.lean
diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean b/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
diff --git a/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean b/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
diff --git a/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
diff --git a/Mathlib/Topology/VectorBundle/ContinuousAlternatingMap.lean b/Mathlib/Topology/VectorBundle/ContinuousAlternatingMap.lean
