chore: tidy various files (#9903)

Author: Ruben-VandeVelde

Mathlib/Algebra/AddTorsor.lean

@@ -287,7 +287,7 @@ instance instAddTorsor : AddTorsor (G × G') (P × P') where
   zero_vadd _ := Prod.ext (zero_vadd _ _) (zero_vadd _ _)
   add_vadd _ _ _ := Prod.ext (add_vadd _ _ _) (add_vadd _ _ _)
   vsub p₁ p₂ := (p₁.1 -ᵥ p₂.1, p₁.2 -ᵥ p₂.2)
-  nonempty := Prod.Nonempty
+  nonempty := Prod.instNonempty
   vsub_vadd' _ _ := Prod.ext (vsub_vadd _ _) (vsub_vadd _ _)
   vadd_vsub' _ _ := Prod.ext (vadd_vsub _ _) (vadd_vsub _ _)
 

Mathlib/Algebra/CharP/Basic.lean

@@ -445,21 +445,21 @@ theorem sum_pow_char {ι : Type*} (s : Finset ι) (f : ι → R) :
 variable (n : ℕ)
 
 theorem list_sum_pow_char_pow (l : List R) : l.sum ^ p ^ n = (l.map (· ^ p ^ n : R → R)).sum := by
-  induction n
-  case zero => simp_rw [pow_zero, pow_one, List.map_id']
-  case succ n ih => simp_rw [pow_succ', pow_mul, ih, list_sum_pow_char, List.map_map]; rfl
+  induction n with
+  | zero => simp_rw [pow_zero, pow_one, List.map_id']
+  | succ n ih => simp_rw [pow_succ', pow_mul, ih, list_sum_pow_char, List.map_map]; rfl
 
 theorem multiset_sum_pow_char_pow (s : Multiset R) :
     s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum := by
-  induction n
-  case zero => simp_rw [pow_zero, pow_one, Multiset.map_id']
-  case succ n ih => simp_rw [pow_succ', pow_mul, ih, multiset_sum_pow_char, Multiset.map_map]; rfl
+  induction n with
+  | zero => simp_rw [pow_zero, pow_one, Multiset.map_id']
+  | succ n ih => simp_rw [pow_succ', pow_mul, ih, multiset_sum_pow_char, Multiset.map_map]; rfl
 
 theorem sum_pow_char_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
     (∑ i in s, f i) ^ p ^ n = ∑ i in s, f i ^ p ^ n := by
-  induction n
-  case zero => simp_rw [pow_zero, pow_one]
-  case succ n ih => simp_rw [pow_succ', pow_mul, ih, sum_pow_char]
+  induction n with
+  | zero => simp_rw [pow_zero, pow_one]
+  | succ n ih => simp_rw [pow_succ', pow_mul, ih, sum_pow_char]
 
 end CommSemiring
 

Mathlib/Algebra/CharP/ExpChar.lean

@@ -253,37 +253,37 @@ variable {R}
 variable [CommSemiring R] (q : ℕ) [hR : ExpChar R q] (n : ℕ)
 
 theorem list_sum_pow_expChar (l : List R) : l.sum ^ q = (l.map (· ^ q : R → R)).sum := by
-  cases hR
-  case zero => simp_rw [pow_one, List.map_id']
-  case prime hprime _ => haveI := Fact.mk hprime; exact list_sum_pow_char q l
+  cases hR with
+  | zero => simp_rw [pow_one, List.map_id']
+  | prime hprime => haveI := Fact.mk hprime; exact list_sum_pow_char q l
 
 theorem multiset_sum_pow_expChar (s : Multiset R) : s.sum ^ q = (s.map (· ^ q : R → R)).sum := by
-  cases hR
-  case zero => simp_rw [pow_one, Multiset.map_id']
-  case prime hprime _ => haveI := Fact.mk hprime; exact multiset_sum_pow_char q s
+  cases hR with
+  | zero => simp_rw [pow_one, Multiset.map_id']
+  | prime hprime => haveI := Fact.mk hprime; exact multiset_sum_pow_char q s
 
 theorem sum_pow_expChar {ι : Type*} (s : Finset ι) (f : ι → R) :
     (∑ i in s, f i) ^ q = ∑ i in s, f i ^ q := by
-  cases hR
-  case zero => simp_rw [pow_one]
-  case prime hprime _ => haveI := Fact.mk hprime; exact sum_pow_char q s f
+  cases hR with
+  | zero => simp_rw [pow_one]
+  | prime hprime => haveI := Fact.mk hprime; exact sum_pow_char q s f
 
 theorem list_sum_pow_expChar_pow (l : List R) :
     l.sum ^ q ^ n = (l.map (· ^ q ^ n : R → R)).sum := by
-  cases hR
-  case zero => simp_rw [one_pow, pow_one, List.map_id']
-  case prime hprime _ => haveI := Fact.mk hprime; exact list_sum_pow_char_pow q n l
+  cases hR with
+  | zero => simp_rw [one_pow, pow_one, List.map_id']
+  | prime hprime => haveI := Fact.mk hprime; exact list_sum_pow_char_pow q n l
 
 theorem multiset_sum_pow_expChar_pow (s : Multiset R) :
     s.sum ^ q ^ n = (s.map (· ^ q ^ n : R → R)).sum := by
-  cases hR
-  case zero => simp_rw [one_pow, pow_one, Multiset.map_id']
-  case prime hprime _ => haveI := Fact.mk hprime; exact multiset_sum_pow_char_pow q n s
+  cases hR with
+  | zero => simp_rw [one_pow, pow_one, Multiset.map_id']
+  | prime hprime => haveI := Fact.mk hprime; exact multiset_sum_pow_char_pow q n s
 
 theorem sum_pow_expChar_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
     (∑ i in s, f i) ^ q ^ n = ∑ i in s, f i ^ q ^ n := by
-  cases hR
-  case zero => simp_rw [one_pow, pow_one]
-  case prime hprime _ => haveI := Fact.mk hprime; exact sum_pow_char_pow q n s f
+  cases hR with
+  | zero => simp_rw [one_pow, pow_one]
+  | prime hprime => haveI := Fact.mk hprime; exact sum_pow_char_pow q n s f
 
 end BigOperators

Mathlib/Analysis/Fourier/AddCircle.lean

@@ -219,7 +219,7 @@ theorem fourier_norm [Fact (0 < T)] (n : ℤ) : ‖@fourier T n‖ = 1 := by
   rw [ContinuousMap.norm_eq_iSup_norm]
   have : ∀ x : AddCircle T, ‖fourier n x‖ = 1 := fun x => abs_coe_circle _
   simp_rw [this]
-  exact @ciSup_const _ _ _ Zero.nonempty _
+  exact @ciSup_const _ _ _ Zero.instNonempty _
 #align fourier_norm fourier_norm
 
 /-- For `n ≠ 0`, a translation by `T / 2 / n` negates the function `fourier n`. -/

Mathlib/Analysis/NormedSpace/PiLp.lean

@@ -86,6 +86,40 @@ protected theorem PiLp.ext {p : ℝ≥0∞} {ι : Type*} {α : ι → Type*} {x
 namespace PiLp
 
 variable (p : ℝ≥0∞) (𝕜 : Type*) {ι : Type*} (α : ι → Type*) (β : ι → Type*)
+section
+/- Register simplification lemmas for the applications of `PiLp` elements, as the usual lemmas
+for Pi types will not trigger. -/
+variable {𝕜 p α}
+variable [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
+variable [∀ i, Module 𝕜 (β i)] [∀ i, BoundedSMul 𝕜 (β i)] (c : 𝕜)
+
+variable (x y : PiLp p β) (i : ι)
+
+@[simp]
+theorem zero_apply : (0 : PiLp p β) i = 0 :=
+  rfl
+#align pi_Lp.zero_apply PiLp.zero_apply
+
+@[simp]
+theorem add_apply : (x + y) i = x i + y i :=
+  rfl
+#align pi_Lp.add_apply PiLp.add_apply
+
+@[simp]
+theorem sub_apply : (x - y) i = x i - y i :=
+  rfl
+#align pi_Lp.sub_apply PiLp.sub_apply
+
+@[simp]
+theorem smul_apply : (c • x) i = c • x i :=
+  rfl
+#align pi_Lp.smul_apply PiLp.smul_apply
+
+@[simp]
+theorem neg_apply : (-x) i = -x i :=
+  rfl
+#align pi_Lp.neg_apply PiLp.neg_apply
+end
 
 /-! Note that the unapplied versions of these lemmas are deliberately omitted, as they break
 the use of the type synonym. -/
@@ -223,11 +257,11 @@ separate from `PiLp.seminormedAddCommGroup` since the latter requires the type c
 
 Registering this separately allows for a future norm-like structure on `PiLp p β` for `p < 1`
 satisfying a relaxed triangle inequality. These are called *quasi-norms*. -/
-instance hasNorm : Norm (PiLp p β) where
+instance instNorm : Norm (PiLp p β) where
   norm f :=
     if p = 0 then {i | ‖f i‖ ≠ 0}.toFinite.toFinset.card
     else if p = ∞ then ⨆ i, ‖f i‖ else (∑ i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal)
-#align pi_Lp.has_norm PiLp.hasNorm
+#align pi_Lp.has_norm PiLp.instNorm
 
 variable {p β}
 
@@ -299,7 +333,6 @@ def pseudoEmetricAux : PseudoEMetricSpace (PiLp p β) where
             (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal) +
               (∑ i, edist (g i) (h i) ^ p.toReal) ^ (1 / p.toReal) :=
           ENNReal.Lp_add_le _ _ _ hp
-
 #align pi_Lp.pseudo_emetric_aux PiLp.pseudoEmetricAux
 
 attribute [local instance] PiLp.pseudoEmetricAux
@@ -528,17 +561,13 @@ instance seminormedAddCommGroup [∀ i, SeminormedAddCommGroup (β i)] :
   { Pi.addCommGroup with
     dist_eq := fun x y => by
       rcases p.dichotomy with (rfl | h)
-      · simp only [dist_eq_iSup, norm_eq_ciSup, dist_eq_norm]
-        -- Porting note: added
-        congr
+      · simp only [dist_eq_iSup, norm_eq_ciSup, dist_eq_norm, sub_apply]
       · have : p ≠ ∞ := by
           intro hp
           rw [hp, ENNReal.top_toReal] at h
           linarith
         simp only [dist_eq_sum (zero_lt_one.trans_le h), norm_eq_sum (zero_lt_one.trans_le h),
-          dist_eq_norm]
-        -- Porting note: added
-        congr }
+          dist_eq_norm, sub_apply] }
 #align pi_Lp.seminormed_add_comm_group PiLp.seminormedAddCommGroup
 
 /-- normed group instance on the product of finitely many normed groups, using the `L^p` norm. -/
@@ -610,8 +639,7 @@ theorem norm_sq_eq_of_L2 (β : ι → Type*) [∀ i, SeminormedAddCommGroup (β
 
 theorem dist_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x y : PiLp 2 β) :
     dist x y = (∑ i, dist (x i) (y i) ^ 2).sqrt := by
-  simp_rw [dist_eq_norm, norm_eq_of_L2]
-  rfl
+  simp_rw [dist_eq_norm, norm_eq_of_L2, sub_apply]
 #align pi_Lp.dist_eq_of_L2 PiLp.dist_eq_of_L2
 
 theorem nndist_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x y : PiLp 2 β) :
@@ -626,7 +654,7 @@ theorem edist_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)
     edist x y = (∑ i, edist (x i) (y i) ^ 2) ^ (1 / 2 : ℝ) := by simp [PiLp.edist_eq_sum]
 #align pi_Lp.edist_eq_of_L2 PiLp.edist_eq_of_L2
 
-instance instboundedSMul [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
+instance instBoundedSMul [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
     [∀ i, Module 𝕜 (β i)] [∀ i, BoundedSMul 𝕜 (β i)] :
     BoundedSMul 𝕜 (PiLp p β) :=
   .of_nnnorm_smul_le fun c f => by
@@ -637,8 +665,6 @@ instance instboundedSMul [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (
       have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
       rw [nnnorm_eq_sum hpt, nnnorm_eq_sum hpt, NNReal.rpow_one_div_le_iff hp0, NNReal.mul_rpow,
         ← NNReal.rpow_mul, div_mul_cancel 1 hp0.ne', NNReal.rpow_one, Finset.mul_sum]
-      -- Porting note: added to replace Pi.smul_apply
-      have smul_apply : ∀ i : ι, (c • f) i = c • (f i) := fun i => rfl
       simp_rw [← NNReal.mul_rpow, smul_apply]
       exact Finset.sum_le_sum fun i _ => NNReal.rpow_le_rpow (nnnorm_smul_le _ _) hp0.le
 
@@ -648,39 +674,10 @@ instance normedSpace [NormedField 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
   norm_smul_le := norm_smul_le
 #align pi_Lp.normed_space PiLp.normedSpace
 
-/- Register simplification lemmas for the applications of `PiLp` elements, as the usual lemmas
-for Pi types will not trigger. -/
 variable {𝕜 p α}
 variable [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
 variable [∀ i, Module 𝕜 (β i)] [∀ i, BoundedSMul 𝕜 (β i)] (c : 𝕜)
 
-variable (x y : PiLp p β) (x' y' : ∀ i, β i) (i : ι)
-
-@[simp]
-theorem zero_apply : (0 : PiLp p β) i = 0 :=
-  rfl
-#align pi_Lp.zero_apply PiLp.zero_apply
-
-@[simp]
-theorem add_apply : (x + y) i = x i + y i :=
-  rfl
-#align pi_Lp.add_apply PiLp.add_apply
-
-@[simp]
-theorem sub_apply : (x - y) i = x i - y i :=
-  rfl
-#align pi_Lp.sub_apply PiLp.sub_apply
-
-@[simp]
-theorem smul_apply : (c • x) i = c • x i :=
-  rfl
-#align pi_Lp.smul_apply PiLp.smul_apply
-
-@[simp]
-theorem neg_apply : (-x) i = -x i :=
-  rfl
-#align pi_Lp.neg_apply PiLp.neg_apply
-
 /-- The canonical map `WithLp.equiv` between `PiLp ∞ β` and `Π i, β i` as a linear isometric
 equivalence. -/
 def equivₗᵢ : PiLp ∞ β ≃ₗᵢ[𝕜] ∀ i, β i :=
@@ -703,8 +700,6 @@ def _root_.LinearIsometryEquiv.piLpCongrLeft (e : ι ≃ ι') :
     (PiLp p fun _ : ι => E) ≃ₗᵢ[𝕜] PiLp p fun _ : ι' => E where
   toLinearEquiv := LinearEquiv.piCongrLeft' 𝕜 (fun _ : ι => E) e
   norm_map' x' := by
-  -- Porting note: this avoids spurious `x` and `y` arguments
-    clear x y
     rcases p.dichotomy with (rfl | h)
     · simp_rw [norm_eq_ciSup]
       exact e.symm.iSup_congr fun _ => rfl
@@ -754,7 +749,6 @@ variable [DecidableEq ι]
 @[simp]
 theorem nnnorm_equiv_symm_single [hp : Fact (1 ≤ p)] (i : ι) (b : β i) :
     ‖(WithLp.equiv p (∀ i, β i)).symm (Pi.single i b)‖₊ = ‖b‖₊ := by
-  clear x y -- Porting note: added
   haveI : Nonempty ι := ⟨i⟩
   induction p using ENNReal.recTopCoe generalizing hp with
   | top =>
@@ -834,7 +828,6 @@ for `p ≠ ∞`. -/
 theorem nnnorm_equiv_symm_const' {β} [SeminormedAddCommGroup β] [Nonempty ι] (b : β) :
     ‖(WithLp.equiv p (ι → β)).symm (Function.const _ b)‖₊ =
       (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖b‖₊ := by
-  clear x y -- Porting note: added to avoid spurious arguments
   rcases em <| p = ∞ with (rfl | hp)
   · simp only [WithLp.equiv_symm_pi_apply, ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero,
       one_mul, nnnorm_eq_ciSup, Function.const_apply, ciSup_const]

Mathlib/Analysis/SpecialFunctions/Gaussian.lean

@@ -665,8 +665,8 @@ theorem isLittleO_exp_neg_mul_sq_cocompact {a : ℂ} (ha : 0 < a.re) (s : ℝ) :
 /-- Jacobi's theta-function transformation formula for the sum of `exp -Q(x)`, where `Q` is a
 negative definite quadratic form. -/
 theorem Complex.tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) :
-    (∑' n : ℤ, cexp (-π * a * n ^ 2 + 2 * π * b * n)) = 1 / a ^ (1 / 2 : ℂ) *
-    ∑' n : ℤ, cexp (-π / a * (n + I * b) ^ 2) := by
+    (∑' n : ℤ, cexp (-π * a * n ^ 2 + 2 * π * b * n)) =
+      1 / a ^ (1 / 2 : ℂ) * ∑' n : ℤ, cexp (-π / a * (n + I * b) ^ 2) := by
   let f : ℝ → ℂ := fun x ↦ cexp (-π * a * x ^ 2 + 2 * π * b * x)
   have hCf : Continuous f
   · refine Complex.continuous_exp.comp (Continuous.add ?_ ?_)
@@ -691,8 +691,7 @@ theorem Complex.tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) :
       -↑π / a * x ^ 2 + (-2 * π * I * b) / a * x + π * b ^ 2 / a
     · intro x; ring_nf; rw [I_sq]; ring
     simp_rw [this]
-    conv => enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _),
-      mul_comm]
+    conv => enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]
     refine ((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact
       (?_) (-2 * ↑π * I * b / a) (-2)).isBigO.const_mul_left _).const_mul_left _
     rwa [neg_div, neg_re, neg_lt_zero]
@@ -704,8 +703,7 @@ theorem Complex.tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) :
 theorem Complex.tsum_exp_neg_mul_int_sq {a : ℂ} (ha : 0 < a.re) :
     (∑' n : ℤ, cexp (-π * a * (n : ℂ) ^ 2)) =
       1 / a ^ (1 / 2 : ℂ) * ∑' n : ℤ, cexp (-π / a * (n : ℂ) ^ 2) := by
-  simpa only [mul_zero, zero_mul, add_zero] using
-    Complex.tsum_exp_neg_quadratic ha 0
+  simpa only [mul_zero, zero_mul, add_zero] using Complex.tsum_exp_neg_quadratic ha 0
 #align complex.tsum_exp_neg_mul_int_sq Complex.tsum_exp_neg_mul_int_sq
 
 theorem Real.tsum_exp_neg_mul_int_sq {a : ℝ} (ha : 0 < a) :

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -344,11 +344,11 @@ theorem coe_comp (f' : G' →g G'') (f : G →g G') : ⇑(f'.comp f) = f' ∘ f
 #align simple_graph.hom.coe_comp SimpleGraph.Hom.coe_comp
 
 /-- The graph homomorphism from a smaller graph to a bigger one. -/
-def ofLe (h : G₁ ≤ G₂) : G₁ →g G₂ := ⟨id, @h⟩
-#align simple_graph.hom.of_le SimpleGraph.Hom.ofLe
+def ofLE (h : G₁ ≤ G₂) : G₁ →g G₂ := ⟨id, @h⟩
+#align simple_graph.hom.of_le SimpleGraph.Hom.ofLE
 
-@[simp, norm_cast] lemma coe_ofLe (h : G₁ ≤ G₂) : ⇑(ofLe h) = id := rfl
-#align simple_graph.hom.coe_of_le SimpleGraph.Hom.coe_ofLe
+@[simp, norm_cast] lemma coe_ofLE (h : G₁ ≤ G₂) : ⇑(ofLE h) = id := rfl
+#align simple_graph.hom.coe_of_le SimpleGraph.Hom.coe_ofLE
 
 end Hom
 

Mathlib/Data/Fintype/Prod.lean

@@ -87,7 +87,7 @@ instance Pi.infinite_of_left {ι : Sort*} {π : ι → Sort _} [∀ i, Nontrivia
 /-- If at least one `π i` is infinite and the rest nonempty, the pi type of all `π` is infinite. -/
 theorem Pi.infinite_of_exists_right {ι : Type*} {π : ι → Type*} (i : ι) [Infinite <| π i]
     [∀ i, Nonempty <| π i] : Infinite (∀ i : ι, π i) :=
-  let ⟨m⟩ := @Pi.Nonempty ι π _
+  let ⟨m⟩ := @Pi.instNonempty ι π _
   Infinite.of_injective _ (update_injective m i)
 #align pi.infinite_of_exists_right Pi.infinite_of_exists_right
 

Mathlib/GroupTheory/MonoidLocalization.lean

@@ -2006,16 +2006,12 @@ variable {α : Type*} [CancelCommMonoid α] {s : Submonoid α} {a₁ b₁ : α}
 
 @[to_additive]
 theorem mk_left_injective (b : s) : Injective fun a => mk a b := fun c d h => by
-  -- porting note: times out unless we add this `have`. Even `infer_instance` times out here.
-  have : Nonempty s := One.nonempty
   simpa [-mk_eq_monoidOf_mk', mk_eq_mk_iff, r_iff_exists] using h
 #align localization.mk_left_injective Localization.mk_left_injective
 #align add_localization.mk_left_injective AddLocalization.mk_left_injective
 
 @[to_additive]
 theorem mk_eq_mk_iff' : mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = a₂ * b₁ := by
-  -- porting note: times out unless we add this `have`. Even `inferInstance` times out here.
-  have : Nonempty s := One.nonempty
   simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]
 #align localization.mk_eq_mk_iff' Localization.mk_eq_mk_iff'
 #align add_localization.mk_eq_mk_iff' AddLocalization.mk_eq_mk_iff'

Mathlib/GroupTheory/Nilpotent.lean

@@ -865,7 +865,7 @@ theorem IsPGroup.isNilpotent [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h :
       have hcq : Fintype.card (G ⧸ center G) < Fintype.card G := by
         rw [card_eq_card_quotient_mul_card_subgroup (center G)]
         apply lt_mul_of_one_lt_right
-        exact Fintype.card_pos_iff.mpr One.nonempty
+        exact Fintype.card_pos_iff.mpr One.instNonempty
         exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
       have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
       exact of_quotient_center_nilpotent hnq