chore: tidy various files (#11135)

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

@@ -100,8 +100,8 @@ lemma smul_fin3 (P : Fin 3 → R) (u : Rˣ) :
   rfl
 
 lemma smul_fin3_ext (P : Fin 3 → R) (u : Rˣ) :
-    (u • P) x = u ^ 2 * P x ∧ (u • P) y = u ^ 3 * P y ∧ (u • P) z = u * P z :=
-  ⟨rfl, rfl, rfl⟩
+    (u • P) x = u ^ 2 * P x ∧ (u • P) y = u ^ 3 * P y ∧ (u • P) z = u * P z := by
+  simp [smul_fin3]
 
 /-- The multiplicative action on a point representative. -/
 scoped instance instMulActionPoint : MulAction Rˣ <| Fin 3 → R where
@@ -297,7 +297,10 @@ lemma equiv_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nons
   have hPy : P y ≠ 0 := fun h => by simp [h] at hP; exact hPx <| pow_eq_zero hP.left.symm
   have hQy : Q y ≠ 0 := fun h => by simp [h] at hQ; exact hQx <| pow_eq_zero hQ.left.symm
   use Units.mk0 _ <| mul_ne_zero (div_ne_zero hPy hPx) (div_ne_zero hQx hQy)
-  simp [smul_fin3, mul_pow, div_pow]
+  simp? [smul_fin3, mul_pow, div_pow] says
+    simp only [Fin.isValue, Units.mk0_mul, smul_fin3, Units.val_mul, Units.val_mk0, mul_pow,
+      div_pow, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two,
+      Matrix.tail_cons, mul_zero]
   congr! 2
   · field_simp [hP.left, hQ.left]
     ring1

Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

@@ -97,11 +97,11 @@ lemma smul_fin3 {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) :
     u • P = ![u * P x, u * P y, u * P z] := by
   rw [fin3_def P]
   matrix_simp
-  rfl
+  simp only [Units.smul_def, smul_eq_mul]
 
 lemma smul_fin3_ext {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) :
-    (u • P) x = u * P x ∧ (u • P) y = u * P y ∧ (u • P) z = u * P z :=
-  ⟨rfl, rfl, rfl⟩
+    (u • P) x = u * P x ∧ (u • P) y = u * P y ∧ (u • P) z = u * P z := by
+  refine ⟨?_, ?_, ?_⟩ <;> simp only [Units.smul_def, Pi.smul_apply, smul_eq_mul]
 
 /-- The equivalence setoid for a point representative. -/
 scoped instance instSetoidPoint : Setoid <| Fin 3 → R :=
@@ -286,8 +286,15 @@ lemma equiv_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nons
     (hPz : P z = 0) (hQz : Q z = 0) : P ≈ Q := by
   rw [fin3_def P, hPz] at hP ⊢
   rw [fin3_def Q, hQz] at hQ ⊢
-  simp [nonsingular_iff, equation_iff] at hP hQ
-  simp [pow_eq_zero hP.left.symm, pow_eq_zero hQ.left.symm] at *
+  simp? [nonsingular_iff, equation_iff] at hP hQ says
+    simp only [Fin.isValue, nonsingular_iff, equation_iff, Matrix.cons_val_one, Matrix.head_cons,
+      Matrix.cons_val_two, Matrix.tail_cons, mul_zero, Matrix.cons_val_zero, add_zero, ne_eq,
+      OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_eq_mul, pow_eq_zero_iff, sub_self,
+      not_true_eq_false, false_or] at hP hQ
+  simp? [pow_eq_zero hP.left.symm, pow_eq_zero hQ.left.symm] at * says
+    simp only [Fin.isValue, pow_eq_zero hP.left.symm, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+      zero_pow, or_true, not_true_eq_false, mul_zero, zero_mul, add_zero, pow_eq_zero_iff, false_or,
+      true_and, pow_eq_zero hQ.left.symm] at *
   exact ⟨Units.mk0 (P y / Q y) <| div_ne_zero hP hQ, by simp [div_mul_cancel _ hQ]⟩
 
 lemma equiv_zero_of_Z_eq_zero {P : Fin 3 → F} (h : W.Nonsingular P) (hPz : P z = 0) :

Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean

@@ -1468,7 +1468,7 @@ variable (G : C ⥤ D)
 
 /-- The comparison morphism for the pullback of `f,g`.
 This is an isomorphism iff `G` preserves the pullback of `f,g`; see
-`CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean`
+`Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean`
 -/
 def pullbackComparison (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] :
     G.obj (pullback f g) ⟶ pullback (G.map f) (G.map g) :=
@@ -1500,7 +1500,7 @@ theorem map_lift_pullbackComparison (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g
 
 /-- The comparison morphism for the pushout of `f,g`.
 This is an isomorphism iff `G` preserves the pushout of `f,g`; see
-`CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean`
+`Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean`
 -/
 def pushoutComparison (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] [HasPushout (G.map f) (G.map g)] :
     pushout (G.map f) (G.map g) ⟶ G.obj (pushout f g) :=
@@ -2398,8 +2398,8 @@ def pullbackAssocSymmIsPullback [HasPullback f₁ (g₃ ≫ f₂)] :
         (show l₁' ≫ g₂ ≫ f₃ = (l₂' ≫ g₄) ≫ f₄ by
           rw [pullback.lift_snd_assoc, Category.assoc, Category.assoc, pullback.condition])) := by
   apply bigSquareIsPullback
-  exact pullbackIsPullback f₃ f₄
-  apply pullbackPullbackRightIsPullback
+  · exact pullbackIsPullback f₃ f₄
+  · apply pullbackPullbackRightIsPullback
 #align category_theory.limits.pullback_assoc_symm_is_pullback CategoryTheory.Limits.pullbackAssocSymmIsPullback
 
 theorem hasPullback_assoc_symm [HasPullback f₁ (g₃ ≫ f₂)] : HasPullback (g₂ ≫ f₃) f₄ :=
@@ -2424,10 +2424,10 @@ theorem pullbackAssoc_inv_fst_fst [HasPullback ((pullback.snd : Z₁ ⟶ X₂) 
     [HasPullback f₁ ((pullback.fst : Z₂ ⟶ X₂) ≫ f₂)] :
     (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst ≫ pullback.fst = pullback.fst := by
   trans l₁' ≫ pullback.fst
-  rw [← Category.assoc]
-  congr 1
-  exact IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.left
-  exact pullback.lift_fst _ _ _
+  · rw [← Category.assoc]
+    congr 1
+    exact IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.left
+  · exact pullback.lift_fst _ _ _
 #align category_theory.limits.pullback_assoc_inv_fst_fst CategoryTheory.Limits.pullbackAssoc_inv_fst_fst
 
 @[reassoc (attr := simp)]
@@ -2442,21 +2442,21 @@ theorem pullbackAssoc_hom_snd_fst [HasPullback ((pullback.snd : Z₁ ⟶ X₂) 
     [HasPullback f₁ ((pullback.fst : Z₂ ⟶ X₂) ≫ f₂)] : (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫
     pullback.snd ≫ pullback.fst = pullback.fst ≫ pullback.snd := by
   trans l₂ ≫ pullback.fst
-  rw [← Category.assoc]
-  congr 1
-  exact IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right
-  exact pullback.lift_fst _ _ _
+  · rw [← Category.assoc]
+    congr 1
+    exact IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right
+  · exact pullback.lift_fst _ _ _
 #align category_theory.limits.pullback_assoc_hom_snd_fst CategoryTheory.Limits.pullbackAssoc_hom_snd_fst
 
 @[reassoc (attr := simp)]
 theorem pullbackAssoc_hom_snd_snd [HasPullback ((pullback.snd : Z₁ ⟶ X₂) ≫ f₃) f₄]
     [HasPullback f₁ ((pullback.fst : Z₂ ⟶ X₂) ≫ f₂)] :
     (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd ≫ pullback.snd = pullback.snd := by
   trans l₂ ≫ pullback.snd
-  rw [← Category.assoc]
-  congr 1
-  exact IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right
-  exact pullback.lift_snd _ _ _
+  · rw [← Category.assoc]
+    congr 1
+    exact IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right
+  · exact pullback.lift_snd _ _ _
 #align category_theory.limits.pullback_assoc_hom_snd_snd CategoryTheory.Limits.pullbackAssoc_hom_snd_snd
 
 @[reassoc (attr := simp)]

Mathlib/Data/Complex/Basic.lean

@@ -959,15 +959,12 @@ instance charZero : CharZero ℂ :=
 
 /-- A complex number `z` plus its conjugate `conj z` is `2` times its real part. -/
 theorem re_eq_add_conj (z : ℂ) : (z.re : ℂ) = (z + conj z) / 2 := by
-  have : (↑(↑2 : ℝ) : ℂ) = (2 : ℂ) := rfl
-  simp only [add_conj, ofReal_mul, ofReal_one, ofReal_bit0, this,
-    mul_div_cancel_left (z.re : ℂ) two_ne_zero]
+  simp only [add_conj, ofReal_mul, ofReal_ofNat, mul_div_cancel_left (z.re : ℂ) two_ne_zero]
 #align complex.re_eq_add_conj Complex.re_eq_add_conj
 
 /-- A complex number `z` minus its conjugate `conj z` is `2i` times its imaginary part. -/
 theorem im_eq_sub_conj (z : ℂ) : (z.im : ℂ) = (z - conj z) / (2 * I) := by
-  have : (↑2 : ℝ ) * I = 2 * I := rfl
-  simp only [sub_conj, ofReal_mul, ofReal_one, ofReal_bit0, mul_right_comm, this,
+  simp only [sub_conj, ofReal_mul, ofReal_ofNat, mul_right_comm,
     mul_div_cancel_left _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)]
 #align complex.im_eq_sub_conj Complex.im_eq_sub_conj
 

Mathlib/Data/Nat/ModEq.lean

@@ -385,7 +385,7 @@ theorem chineseRemainder_lt_mul (co : n.Coprime m) (a b : ℕ) (hn : n ≠ 0) (h
 #align nat.chinese_remainder_lt_mul Nat.chineseRemainder_lt_mul
 
 theorem mod_lcm (hn : a ≡ b [MOD n]) (hm : a ≡ b [MOD m]) : a ≡ b [MOD lcm n m] :=
-  (Nat.modEq_iff_dvd).mpr <| Int.lcm_dvd (Nat.modEq_iff_dvd.mp hn) (Nat.modEq_iff_dvd.mp hm)
+  Nat.modEq_iff_dvd.mpr <| Int.lcm_dvd (Nat.modEq_iff_dvd.mp hn) (Nat.modEq_iff_dvd.mp hm)
 
 theorem chineseRemainder_modEq_unique (co : n.Coprime m) {a b z}
     (hzan : z ≡ a [MOD n]) (hzbm : z ≡ b [MOD m]) : z ≡ chineseRemainder co a b [MOD n*m] := by
@@ -399,8 +399,8 @@ theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℕ} (hmn : m.Coprime n) :
     rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd, ← Int.dvd_natAbs,
       Int.coe_nat_dvd] at h
     rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd]
-    exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2, fun h =>
-    ⟨h.of_mul_right _, h.of_mul_left _⟩⟩
+    exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2,
+   fun h => ⟨h.of_mul_right _, h.of_mul_left _⟩⟩
 #align nat.modeq_and_modeq_iff_modeq_mul Nat.modEq_and_modEq_iff_modEq_mul
 
 theorem coprime_of_mul_modEq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : a.Coprime n := by

Mathlib/GroupTheory/SchurZassenhaus.lean

@@ -15,10 +15,10 @@ In this file we prove the Schur-Zassenhaus theorem.
 
 ## Main results
 
-- `exists_right_complement'_of_coprime` : The **Schur-Zassenhaus** theorem:
+- `exists_right_complement'_of_coprime`: The **Schur-Zassenhaus** theorem:
   If `H : Subgroup G` is normal and has order coprime to its index,
   then there exists a subgroup `K` which is a (right) complement of `H`.
-- `exists_left_complement'_of_coprime` : The **Schur-Zassenhaus** theorem:
+- `exists_left_complement'_of_coprime`: The **Schur-Zassenhaus** theorem:
   If `H : Subgroup G` is normal and has order coprime to its index,
   then there exists a subgroup `K` which is a (left) complement of `H`.
 -/

Mathlib/Init/Logic.lean

@@ -469,7 +469,7 @@ lemma Equivalence.reflexive {r : β → β → Prop} (h : Equivalence r) : Refle
 
 lemma Equivalence.symmetric {r : β → β → Prop} (h : Equivalence r) : Symmetric r := fun _ _ ↦ h.symm
 
-lemma Equivalence.transitive {r : β → β → Prop}(h : Equivalence r) : Transitive r :=
+lemma Equivalence.transitive {r : β → β → Prop} (h : Equivalence r) : Transitive r :=
   fun _ _ _ ↦ h.trans
 
 /-- A relation is total if for all `x` and `y`, either `x ≺ y` or `y ≺ x`. -/

Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

@@ -145,9 +145,11 @@ def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] :
     (LinearMap.fst _ _ _ - LinearMap.snd _ _ _)
   map_app' x := by
     dsimp only [associated, associatedHom]
-    dsimp
-    -- Porting note: added `()` around `Submonoid.smul_def`
-    simp [polar_comm _ x.1 x.2, ← sub_add, mul_sub, sub_mul, smul_sub, (Submonoid.smul_def), ←
+    dsimp only [LinearMap.smul_apply, LinearMap.coe_mk, AddHom.coe_mk, AddHom.toFun_eq_coe,
+      LinearMap.coe_toAddHom, LinearMap.prod_apply, Pi.prod, LinearMap.add_apply,
+      LinearMap.coe_comp, Function.comp_apply, LinearMap.fst_apply, LinearMap.snd_apply,
+      LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, prod_apply, neg_apply]
+    simp [polar_comm _ x.1 x.2, ← sub_add, mul_sub, sub_mul, smul_sub, Submonoid.smul_def, ←
       sub_eq_add_neg (Q x.1) (Q x.2)]
 #align quadratic_form.to_dual_prod QuadraticForm.toDualProdₓ
 

Mathlib/Logic/Godel/GodelBetaFunction.lean

@@ -43,21 +43,16 @@ Gödel, beta function
 namespace Nat
 
 lemma coprime_mul_succ {n m a} (h : n ≤ m) (ha : m - n ∣ a) : Coprime (n * a + 1) (m * a + 1) :=
-  Nat.coprime_of_dvd (by
-    intro p pp hn hm
+  Nat.coprime_of_dvd fun p pp hn hm => by
     have : p ∣ (m - n) * a := by
       simpa [Nat.succ_sub_succ, ← Nat.mul_sub_right_distrib] using
         Nat.dvd_sub (Nat.succ_le_succ $ Nat.mul_le_mul_right a h) hm hn
     have : p ∣ a := by
       rcases (Nat.Prime.dvd_mul pp).mp this with (hp | hp)
       · exact Nat.dvd_trans hp ha
       · exact hp
-    have : p = 1 := by
-      simpa[Nat.add_sub_cancel_left] using Nat.dvd_sub (le_add_right _ _) hn
-        (Dvd.dvd.mul_left this n)
-    simp[this] at pp
-    apply Nat.not_prime_one at pp
-    exact pp)
+    apply pp.ne_one
+    simpa [Nat.add_sub_cancel_left] using Nat.dvd_sub (le_add_right _ _) hn (this.mul_left n)
 
 variable {m : ℕ}
 
@@ -77,12 +72,13 @@ private lemma pairwise_coprime_coprimes (a : Fin m → ℕ) : Pairwise (Coprime
   intro i j hij
   wlog ltij : i < j
   · exact (this a hij.symm (lt_of_le_of_ne (Fin.not_lt.mp ltij) hij.symm)).symm
-  suffices  Coprime ((i + 1) * (supOfSeq a)! + 1) ((j + 1) * (supOfSeq a)! + 1) by exact this
+  unfold Function.onFun coprimes
   have hja : j < supOfSeq a := lt_of_lt_of_le j.prop (le_step (le_max_left _ _))
   exact coprime_mul_succ
     (Nat.succ_le_succ $ le_of_lt ltij)
-    (Nat.dvd_factorial (by simp[Nat.succ_sub_succ, ltij]) (by
-      simpa only [Nat.succ_sub_succ] using le_of_lt (lt_of_le_of_lt (sub_le j i) hja)))
+    (Nat.dvd_factorial
+      (by simp [Nat.succ_sub_succ, ltij])
+      (by simpa only [Nat.succ_sub_succ] using le_of_lt (lt_of_le_of_lt (sub_le j i) hja)))
 
 /-- Gödel's Beta Function. This is similar to `(Encodable.decodeList).get i`, but it is easier to
 prove that it is arithmetically definable. -/
@@ -92,13 +88,12 @@ def beta (n i : ℕ) : ℕ := n.unpair.1 % ((i + 1) * n.unpair.2 + 1)
 to prove that it is arithmetically definable. -/
 def unbeta (l : List ℕ) : ℕ :=
   (chineseRemainderOfFinset l.get (coprimes l.get) Finset.univ
-    (by simp[coprimes])
+    (by simp [coprimes])
     (by simpa using Set.pairwise_univ.mpr (pairwise_coprime_coprimes _)) : ℕ).pair
   (supOfSeq l.get)!
 
 /-- **Gödel's Beta Function Lemma** -/
-lemma beta_unbeta_coe (l : List ℕ) (i : Fin l.length) :
-    beta (unbeta l) i = l.get i := by
+lemma beta_unbeta_coe (l : List ℕ) (i : Fin l.length) : beta (unbeta l) i = l.get i := by
   simpa [beta, unbeta, coprimes] using mod_eq_of_modEq
     ((chineseRemainderOfFinset l.get (coprimes l.get) Finset.univ
       (by simp [coprimes])

Mathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -1102,7 +1102,7 @@ theorem lintegral_iInf_directed_of_measurable {mα : MeasurableSpace α} [Counta
     _ = ⨅ n, ∫⁻ a, (f ∘ h_directed.sequence f) n a ∂μ := by
       rw [lintegral_iInf ?_ h_directed.sequence_anti]
       · exact hf_int _
-      · exact (fun n => hf _)
+      · exact fun n => hf _
     _ = ⨅ b, ∫⁻ a, f b a ∂μ := by
       refine' le_antisymm (le_iInf fun b => _) (le_iInf fun n => _)
       · exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

@@ -560,7 +560,7 @@ instance : NoAtoms (volume : Measure (E K)) := by
 
 /-- The fudge factor that appears in the formula for the volume of `convexBodyLT`. -/
 noncomputable abbrev convexBodyLTFactor : ℝ≥0 :=
-  (2:ℝ≥0) ^ NrRealPlaces K * NNReal.pi ^ NrComplexPlaces K
+  (2 : ℝ≥0) ^ NrRealPlaces K * NNReal.pi ^ NrComplexPlaces K
 
 theorem convexBodyLTFactor_ne_zero : convexBodyLTFactor K ≠ 0 :=
   mul_ne_zero (pow_ne_zero _ two_ne_zero) (pow_ne_zero _ pi_ne_zero)
@@ -633,7 +633,7 @@ abbrev convexBodyLT' : Set (E K) :=
     if w = w₀ then {x | |x.re| < 1 ∧ |x.im| < (f w : ℝ) ^ 2} else ball 0 (f w)))
 
 theorem convexBodyLT'_mem {x : K} :
-    mixedEmbedding K x ∈ (convexBodyLT' K f w₀) ↔
+    mixedEmbedding K x ∈ convexBodyLT' K f w₀ ↔
       (∀ w : InfinitePlace K, w ≠ w₀ → w x < f w) ∧
       |(w₀.val.embedding x).re| < 1 ∧ |(w₀.val.embedding x).im| < (f w₀: ℝ) ^ 2 := by
   simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ,
@@ -651,8 +651,8 @@ theorem convexBodyLT'_mem {x : K} :
     · rw [if_neg (by exact Subtype.ne_of_val_ne h_ne)]
       exact h₁ w h_ne
 
-theorem convexBodyLT'_neg_mem (x : E K) (hx : x ∈ (convexBodyLT' K f w₀)) :
-    -x ∈ (convexBodyLT' K f w₀) := by
+theorem convexBodyLT'_neg_mem (x : E K) (hx : x ∈ convexBodyLT' K f w₀) :
+    -x ∈ convexBodyLT' K f w₀ := by
   simp [Set.mem_prod, Prod.fst_neg, Set.mem_pi, Set.mem_univ, Pi.neg_apply,
     mem_ball_zero_iff, norm_neg, Real.norm_eq_abs, forall_true_left, Subtype.forall,
     Prod.snd_neg, Complex.norm_eq_abs] at hx ⊢
@@ -675,7 +675,7 @@ variable [NumberField K]
 
 /-- The fudge factor that appears in the formula for the volume of `convexBodyLT'`. -/
 noncomputable abbrev convexBodyLT'Factor : ℝ≥0 :=
-  (2:ℝ≥0) ^ (NrRealPlaces K + 2) * NNReal.pi ^ (NrComplexPlaces K - 1)
+  (2 : ℝ≥0) ^ (NrRealPlaces K + 2) * NNReal.pi ^ (NrComplexPlaces K - 1)
 
 theorem convexBodyLT'Factor_ne_zero : convexBodyLT'Factor K ≠ 0 :=
   mul_ne_zero (pow_ne_zero _ two_ne_zero) (pow_ne_zero _ pi_ne_zero)
@@ -685,7 +685,7 @@ theorem one_le_convexBodyLT'Factor : 1 ≤ convexBodyLT'Factor K :=
     (one_le_pow_of_one_le (le_trans one_le_two Real.two_le_pi) _)
 
 theorem convexBodyLT'_volume :
-    volume (convexBodyLT' K f w₀) = (convexBodyLT'Factor K) * ∏ w, (f w) ^ (mult w) := by
+    volume (convexBodyLT' K f w₀) = convexBodyLT'Factor K * ∏ w, (f w) ^ (mult w) := by
   have vol_box : ∀ B : ℝ≥0, volume {x : ℂ | |x.re| < 1 ∧ |x.im| < B^2} = 4*B^2 := by
     intro B
     rw [← (Complex.volume_preserving_equiv_real_prod.symm).measure_preimage]
@@ -709,20 +709,20 @@ theorem convexBodyLT'_volume :
       · refine Finset.prod_congr rfl (fun w' hw' ↦ ?_)
         rw [if_neg (Finset.ne_of_mem_erase hw'), Complex.volume_ball]
       · simpa only [ite_true] using vol_box (f w₀)
-    _ = ((2:ℝ≥0) ^ NrRealPlaces K *
+    _ = ((2 : ℝ≥0) ^ NrRealPlaces K *
           (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))) *
             ((∏ x in Finset.univ.erase  w₀, ENNReal.ofReal (f x.val) ^ 2) *
               ↑pi ^ (NrComplexPlaces K - 1) * (4 * (f w₀) ^ 2)) := by
       simp_rw [ofReal_mul (by norm_num : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
         Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, ofReal_ofNat,
         ofReal_coe_nnreal, coe_ofNat]
-    _ = (convexBodyLT'Factor K) * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))
+    _ = convexBodyLT'Factor K * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))
         * (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2) := by
-      rw [show (4:ℝ≥0∞) = (2:ℝ≥0) ^ 2 by norm_num, convexBodyLT'Factor, pow_add,
+      rw [show (4 : ℝ≥0∞) = (2 : ℝ≥0) ^ 2 by norm_num, convexBodyLT'Factor, pow_add,
         ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀), ofReal_coe_nnreal]
       simp_rw [coe_mul, ENNReal.coe_pow]
       ring
-    _ = (convexBodyLT'Factor K) * ∏ w, (f w) ^ (mult w) := by
+    _ = convexBodyLT'Factor K * ∏ w, (f w) ^ (mult w) := by
       simp_rw [mult, pow_ite, pow_one, Finset.prod_ite, ofReal_coe_nnreal, not_isReal_iff_isComplex,
         coe_mul, coe_finset_prod, ENNReal.coe_pow, mul_assoc]
       congr 3
@@ -863,7 +863,7 @@ theorem convexBodySum_compact : IsCompact (convexBodySum K B) := by
 
 /-- The fudge factor that appears in the formula for the volume of `convexBodyLt`. -/
 noncomputable abbrev convexBodySumFactor : ℝ≥0 :=
-  (2:ℝ≥0) ^ NrRealPlaces K * (NNReal.pi / 2) ^ NrComplexPlaces K / (finrank ℚ K).factorial
+  (2 : ℝ≥0) ^ NrRealPlaces K * (NNReal.pi / 2) ^ NrComplexPlaces K / (finrank ℚ K).factorial
 
 theorem convexBodySumFactor_ne_zero : convexBodySumFactor K ≠ 0 := by
   refine div_ne_zero ?_ <| Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
@@ -1038,7 +1038,7 @@ theorem exists_primitive_element_lt_of_isComplex {w₀ : InfinitePlace K} (hw₀
     {B : ℝ≥0} (hB : minkowskiBound K ↑1 < convexBodyLT'Factor K * B) :
     ∃ a ∈ 𝓞 K, ℚ⟮(a:K)⟯ = ⊤ ∧ (∀ w : InfinitePlace K, w a < Real.sqrt (1 + B ^ 2)) := by
   have : minkowskiBound K ↑1 <
-      volume (convexBodyLT' K (fun w ↦ if w = w₀ then (NNReal.sqrt B) else 1) ⟨w₀, hw₀⟩) := by
+      volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩) := by
     rw [convexBodyLT'_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
     simp_rw [ite_pow, one_pow]
     rw [Finset.prod_ite_eq']