Formatting.

Vierkantor · Vierkantor · commit 7a985231fbba · 2026-05-13T18:20:03.000+02:00
diff --git a/Mathlib/Algebra/Group/Action/Basic.lean b/Mathlib/Algebra/Group/Action/Basic.lean
@@ -150,8 +150,7 @@ 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
diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean
@@ -539,8 +539,6 @@ theorem sub_one_div_inv_le_two (a2 : 2 ≤ a) : (1 - 1 / a)⁻¹ ≤ 2 := by
   rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]
   -- take inverses on both sides and use the assumption `2 ≤ a`.
   convert (one_div a).le.trans (inv_anti₀ zero_lt_two a2) using 1
-    -- show `1 - 1 / 2 = 1 / 2`.
-    
   -- show `1 - 1 / 2 = 1 / 2`.
   rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]
 
diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean
@@ -220,11 +220,11 @@ lemma Odd.sub_odd (ha : Odd a) (hb : Odd b) : Even (a - b) := by
 
 @[simp]
 lemma even_add_one : Even (a + 1) ↔ Odd a :=
-  ⟨(by convert x✝.sub_odd odd_one; rw [eq_sub_iff_add_eq]), (·.add_one)⟩
+  ⟨(by convert ·.sub_odd odd_one; rw [eq_sub_iff_add_eq]), (·.add_one)⟩
 
 @[simp]
 lemma even_sub_one : Even (a - 1) ↔ Odd a :=
-  ⟨(by convert x✝.add_odd odd_one; rw [sub_add_cancel]), (·.sub_odd odd_one)⟩
+  ⟨(by convert ·.add_odd odd_one; rw [sub_add_cancel]), (·.sub_odd odd_one)⟩
 
 @[simp]
 lemma even_add_two : Even (a + 2) ↔ Even a :=
@@ -236,11 +236,11 @@ lemma even_sub_two : Even (a - 2) ↔ Even a :=
 
 @[simp]
 lemma odd_add_one : Odd (a + 1) ↔ Even a :=
-  ⟨(by convert x✝.sub_odd odd_one; rw [eq_sub_iff_add_eq]), (·.add_one)⟩
+  ⟨(by convert ·.sub_odd odd_one; rw [eq_sub_iff_add_eq]), (·.add_one)⟩
 
 @[simp]
 lemma odd_sub_one : Odd (a - 1) ↔ Even a :=
-  ⟨(by convert x✝.add_odd odd_one; rw [sub_add_cancel]), (·.sub_odd odd_one)⟩
+  ⟨(by convert ·.add_odd odd_one; rw [sub_add_cancel]), (·.sub_odd odd_one)⟩
 
 @[simp]
 lemma odd_add_two : Odd (a + 2) ↔ Odd a := by
diff --git a/Mathlib/Analysis/Fourier/Convolution.lean b/Mathlib/Analysis/Fourier/Convolution.lean
@@ -88,8 +88,7 @@ theorem fourier_bilin_convolution_eq_integral (B : F₁ →L[𝕜] F₂ →L[
     congr
     ext y
     -- Linear change of variables
-    convert! integral_sub_right_eq_self _ y (μ := volume)
-    congr
+    convert integral_sub_right_eq_self _ y (μ := volume)
     simp
 
 variable [CompleteSpace F₁] [CompleteSpace F₂] [CompleteSpace F₃]
diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean
@@ -204,8 +204,10 @@ theorem summable_condensed_iff {f : ℕ → ℝ≥0} (hf : ∀ ⦃m n⦄, 0 < m
   have h_succ_diff : SuccDiffBounded 2 (2 ^ ·) := by
     intro n
     simp [pow_succ, mul_two, two_mul]
-  convert! summable_schlomilch_iff hf (pow_pos zero_lt_two) (pow_right_strictMono₀ _root_.one_lt_two)
-    two_ne_zero h_succ_diff
+  convert! summable_schlomilch_iff hf (pow_pos zero_lt_two)
+    (pow_right_strictMono₀ _root_.one_lt_two)
+    two_ne_zero
+    h_succ_diff
   simp [pow_succ, mul_two]
 
 end NNReal
diff --git a/Mathlib/Analysis/SpecialFunctions/Arsinh.lean b/Mathlib/Analysis/SpecialFunctions/Arsinh.lean
@@ -158,7 +158,8 @@ theorem arsinh_neg_iff : arsinh x < 0 ↔ x < 0 :=
   lt_iff_lt_of_le_iff_le arsinh_nonneg_iff
 
 theorem hasStrictDerivAt_arsinh (x : ℝ) : HasStrictDerivAt arsinh (√(1 + x ^ 2))⁻¹ x := by
-  convert! sinhHomeomorph.toOpenPartialHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne'
+  convert! sinhHomeomorph.toOpenPartialHomeomorph.hasStrictDerivAt_symm (mem_univ x)
+    (cosh_pos _).ne'
     (hasStrictDerivAt_sinh _) using 2
   exact (cosh_arsinh _).symm
 
diff --git a/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean b/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
@@ -285,7 +285,8 @@ theorem lintegral_comp_pi_polarCoord_symm (f : (ι → ℝ × ℝ) → ℝ≥0
     ∫⁻ p in (Set.univ.pi fun _ : ι ↦ polarCoord.target),
       (∏ i, .ofReal (p i).1) * f (fun i ↦ polarCoord.symm (p i)) = ∫⁻ p, f p := by
   rw [← setLIntegral_univ f, ← setLIntegral_congr pi_polarCoord_symm_target_ae_eq_univ]
-  convert! (lintegral_image_eq_lintegral_abs_det_fderiv_mul volume measurableSet_pi_polarCoord_target
+  convert! (lintegral_image_eq_lintegral_abs_det_fderiv_mul volume
+    measurableSet_pi_polarCoord_target
     (fun p _ ↦ (hasFDerivAt_pi_polarCoord_symm p).hasFDerivWithinAt)
       injOn_pi_polarCoord_symm f).symm using 1
   refine setLIntegral_congr_fun measurableSet_pi_polarCoord_target (fun x hx ↦ ?_)
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
@@ -147,8 +147,9 @@ abbrev pushoutInl (F : WalkingParallelPair ⥤ C) :
 set_option backward.isDefEq.respectTransparency false in
 theorem pushoutInl_eq_pushout_inr (F : WalkingParallelPair ⥤ C) :
     pushoutInl F = pushout.inr _ _ := by
-  convert
-    (whisker_eq Limits.coprod.inl pushout.condition : (_ : F.obj _ ⟶ constructCoequalizer _) = _) <;> simp
+  convert (whisker_eq Limits.coprod.inl pushout.condition :
+      (_ : F.obj _ ⟶ constructCoequalizer _) = _) <;>
+    simp
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Define the equalizing cocone -/
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean
@@ -97,7 +97,7 @@ namespace CommMonTypeEquivalenceCommMon
 
 instance commMonCommMonoid (A : Type u) [MonObj A] [IsCommMonObj A] : CommMonoid A :=
   { MonTypeEquivalenceMon.monMonoid A with
-    mul_comm := fun x y => by convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x) }
+    mul_comm x y := by convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x) }
 
 /-- Converting a commutative monoid object in `Type` to a bundled commutative monoid.
 -/
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean
@@ -29,7 +29,7 @@ namespace CommGrpTypeEquivalenceCommGrp
 
 instance commGrpCommGroup (A : Type u) [GrpObj A] [IsCommMonObj A] : CommGroup A :=
   { GrpTypeEquivalenceGrp.grpGroup A with
-    mul_comm := fun x y => by convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x) }
+    mul_comm x y := by convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x) }
 
 /-- Converting a commutative group object in `Type u` into a group. -/
 noncomputable def functor : CommGrp (Type u) ⥤ CommGrpCat.{u} where
diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
@@ -347,7 +347,8 @@ lemma IsEquipartition.card_biUnion_offDiag_le (hε : 0 < ε) (hP : P.IsEquiparti
   refine (mul_le_mul_of_nonneg_left this <| by positivity).trans ?_
   suffices 1 ≤ ε / 4 * #P.parts by
     rw [mul_left_comm, ← sq]
-    convert mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1 <;> ring
+    convert mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜))
+      using 1 <;> ring
   rwa [← div_le_iff₀', one_div_div]
   positivity
 
diff --git a/Mathlib/Data/Nat/Digits/Lemmas.lean b/Mathlib/Data/Nat/Digits/Lemmas.lean
@@ -200,8 +200,8 @@ theorem sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) :
   obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
   · rcases eq_or_ne n 0 with rfl | hn
     · simp
-    · convert! sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
-          (fun l a ↦ digits_lt_base h a)
+    · convert! sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn)
+        fun l a ↦ digits_lt_base h a
       · refine (length_digits p n h hn).symm
       all_goals exact (ofDigits_digits p n).symm
   · simp
diff --git a/Mathlib/FieldTheory/Galois/NormalBasis.lean b/Mathlib/FieldTheory/Galois/NormalBasis.lean
@@ -44,9 +44,10 @@ theorem exists_linearIndependent_algEquiv_apply_of_finite [Finite L] :
     .ofBijective _ <| bijective_frobeniusAlgEquivOfAlgebraic_pow K L)]
   /- Therefore, `{Frⁱ | 0 ≤ i < [L : K]}` is linearly independent, which implies that
     `{Frⁱ(x) | 0 ≤ i < [L : K]}` is also linearly independent. -/
-  convert! (AdjoinRoot.powerBasis (X_pow_sub_C_ne_zero Module.finrank_pos 1)).basis.linearIndependent
-    |>.map' ((AEval'.of _).symm.toLinearMap ∘ₗ (liftQ _ _ hx.le).restrictScalars K) <| by
-    exact congr($(ker_liftQ_eq_bot' _ _ hx).restrictScalars K)
+  convert!
+    (AdjoinRoot.powerBasis (X_pow_sub_C_ne_zero Module.finrank_pos 1)).basis.linearIndependent
+      |>.map' ((AEval'.of _).symm.toLinearMap ∘ₗ (liftQ _ _ hx.le).restrictScalars K) <| by
+      exact congr($(ker_liftQ_eq_bot' _ _ hx).restrictScalars K)
   ext i
   simp_rw [Equiv.coe_trans, Function.comp_apply, finCongr_apply, Equiv.ofBijective_apply,
     AlgEquiv.coe_pow, AdjoinRoot.powerBasis, AdjoinRoot.powerBasisAux, Basis.coe_mk,
diff --git a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean
@@ -94,8 +94,8 @@ lemma root_add_root_mem_of_mem_of_mem (hk : α k + α i - α j ∈ Φ)
   rw [← neg_mem_range_root_iff]
   convert
     b.root_sub_root_mem_of_mem_of_mem j i (-k) hij.symm hj hi hk (by contrapose hkj; aesop)
-      (by convert! P.neg_mem_range_root_iff.mpr hk' using 1; simp [neg_add_eq_sub]) using
-    1
+      (by convert P.neg_mem_range_root_iff.mpr hk' using 1; simp [neg_add_eq_sub])
+    using 1
   simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self]
   module
 
diff --git a/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean b/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean
@@ -215,11 +215,7 @@ lemma tendstoInDistribution_of_tendstoInMeasure_sub {X : ι → Ω'' → E}
         · exact fun x hx ↦ hF_lip.norm_sub_le_of_le hx.le
       · refine setIntegral_mono h_int_sub.integrableOn integrableOn_const fun a ↦ ?_
         rw [← dist_eq_norm]
-        convert
-          hF_bounded _
-            _
-              -- The goal is now a simple computation
-              
+        convert hF_bounded _ _
     -- The goal is now a simple computation
     _ = L * (ε / 2) * μ''.real {x | ‖Y n x - X n x‖ < ε / 2}
         + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} := by
diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Set.lean b/Mathlib/MeasureTheory/Integral/Bochner/Set.lean
@@ -1028,7 +1028,8 @@ variable [MeasurableSpace X] [PseudoEMetricSpace X]
 
 theorem measure_le_lintegral_thickenedIndicatorAux (μ : Measure X) {E : Set X}
     (E_mble : MeasurableSet E) (δ : ℝ) : μ E ≤ ∫⁻ x, (thickenedIndicatorAux δ E x : ℝ≥0∞) ∂μ := by
-  convert_to! lintegral μ (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ lintegral μ (thickenedIndicatorAux δ E)
+  convert_to!
+    lintegral μ (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ lintegral μ (thickenedIndicatorAux δ E)
   · rw [lintegral_indicator E_mble]
     simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]
   · apply lintegral_mono
diff --git a/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean b/Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean
@@ -62,7 +62,8 @@ theorem exists_partition {ι : Type*} [Finite ι] {ε : ℝ} (hε : 0 < ε) {b :
   rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
   obtain ⟨t, ht⟩ := h.exists_partition' n hε hb (A ∘ e.symm)
   refine ⟨t ∘ e, fun i₀ i₁ h ↦ ?_⟩
-  convert (config := { transparency := .default }) ht (e i₀) (e i₁) h <;> simp only [e.symm_apply_apply]
+  convert (config := { transparency := .default }) ht (e i₀) (e i₁) h <;>
+    simp only [e.symm_apply_apply]
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Any large enough family of vectors in `R^n` has a pair of elements
diff --git a/Mathlib/Order/RelSeries.lean b/Mathlib/Order/RelSeries.lean
@@ -296,7 +296,7 @@ def append (p q : RelSeries r) (connect : p.last ~[r] q.head) : RelSeries r wher
   step i := by
     obtain hi | rfl | hi :=
       lt_trichotomy i (Fin.castLE (by lia) (Fin.last _ : Fin (p.length + 1)))
-    · convert p.step ⟨i.1, hi⟩ <;> convert! Fin.append_left p q _ <;> rfl
+    · convert p.step ⟨i.1, hi⟩ <;> convert! Fin.append_left p q _
     · convert connect
       · convert! Fin.append_left p q _
       · convert! Fin.append_right p q _; rfl
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)
+  with_reducible 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/Localization/Integral.lean b/Mathlib/RingTheory/Localization/Integral.lean
@@ -449,7 +449,9 @@ protected lemma IsLocalization.integralClosure
       (integralClosure Rf Sf) := by
   refine ⟨⟨?_, ?_, ?_⟩⟩
   · rintro ⟨_, f, hf, rfl⟩
-    convert! (IsLocalization.map_units (S := Rf) ⟨f, hf⟩).map (algebraMap Rf (integralClosure Rf Sf))
+    convert!
+      (IsLocalization.map_units (S := Rf) ⟨f, hf⟩).map
+        (algebraMap Rf (integralClosure Rf Sf))
     simp [← IsScalarTower.algebraMap_apply]
   · rintro ⟨s, hs⟩
     obtain ⟨⟨x, _, m₁, hm₁, rfl⟩, e⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid S M) s
diff --git a/Mathlib/Topology/ContinuousMap/Periodic.lean b/Mathlib/Topology/ContinuousMap/Periodic.lean
@@ -33,8 +33,6 @@ theorem periodic_tsum_comp_add_zsmul [AddCommGroup X] [ContinuousAdd X] [AddComm
   intro x
   by_cases h : Summable fun n : ℤ => f.comp (ContinuousMap.addRight (n • p))
   · convert congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _) using 1
-    -- This `have` unfolds the function composition in `Equiv.summable_iff`.
-    
     -- This `have` unfolds the function composition in `Equiv.summable_iff`.
     have : Summable fun (c : ℤ) => f.comp (ContinuousMap.addRight (Equiv.addRight 1 c • p)) :=
       (Equiv.addRight (1 : ℤ)).summable_iff.mpr h
diff --git a/Mathlib/Topology/Sheaves/Stalks.lean b/Mathlib/Topology/Sheaves/Stalks.lean
@@ -216,7 +216,8 @@ theorem comp (ℱ : X.Presheaf C) (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
 theorem stalkPushforward_iso_of_isInducing {f : X ⟶ Y} (hf : IsInducing f)
     (F : X.Presheaf C) (x : X) : IsIso (F.stalkPushforward _ f x) := by
   haveI := Functor.initial_of_adjunction (hf.adjunctionNhds x)
-  convert! (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).isIso_hom
+  convert!
+    (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).isIso_hom
   refine stalk_hom_ext _ fun U hU ↦ (stalkPushforward_germ _ f F _ x hU).trans ?_
   symm
   exact colimit.ι_pre ((OpenNhds.inclusion x).op ⋙ F) (OpenNhds.map f x).op _
