chore: tidy various files (#1693)

Author: Ruben-VandeVelde

Mathlib/Algebra/BigOperators/Ring.lean

@@ -38,8 +38,7 @@ variable [CommMonoid β]
 open Classical
 
 theorem prod_pow_eq_pow_sum {x : β} {f : α → ℕ} :
-    ∀ {s : Finset α}, (∏ i in s, x ^ f i) = x ^ ∑ x in s, f x :=
-  by
+    ∀ {s : Finset α}, (∏ i in s, x ^ f i) = x ^ ∑ x in s, f x := by
   apply Finset.induction
   · simp
   · intro a s has H
@@ -61,8 +60,8 @@ theorem mul_sum : (b * ∑ x in s, f x) = ∑ x in s, b * f x :=
 #align finset.mul_sum Finset.mul_sum
 
 theorem sum_mul_sum {ι₁ : Type _} {ι₂ : Type _} (s₁ : Finset ι₁) (s₂ : Finset ι₂) (f₁ : ι₁ → β)
-    (f₂ : ι₂ → β) : ((∑ x₁ in s₁, f₁ x₁) * ∑ x₂ in s₂, f₂ x₂) = ∑ p in s₁ ×ᶠ s₂, f₁ p.1 * f₂ p.2 :=
-  by
+    (f₂ : ι₂ → β) :
+    ((∑ x₁ in s₁, f₁ x₁) * ∑ x₂ in s₂, f₂ x₂) = ∑ p in s₁ ×ᶠ s₂, f₁ p.1 * f₂ p.2 := by
   rw [sum_product, sum_mul, sum_congr rfl]
   intros
   rw [mul_sum]
@@ -96,13 +95,12 @@ variable [CommSemiring β]
   `Finset.prod_univ_sum` is an alternative statement when the product is over `univ`. -/
 theorem prod_sum {δ : α → Type _} [DecidableEq α] [∀ a, DecidableEq (δ a)] {s : Finset α}
     {t : ∀ a, Finset (δ a)} {f : ∀ a, δ a → β} :
-    (∏ a in s, ∑ b in t a, f a b) = ∑ p in s.pi t, ∏ x in s.attach, f x.1 (p x.1 x.2) :=
-  by
+    (∏ a in s, ∑ b in t a, f a b) = ∑ p in s.pi t, ∏ x in s.attach, f x.1 (p x.1 x.2) := by
   induction' s using Finset.induction with a s ha ih
   · rw [pi_empty, sum_singleton]
     rfl
-  · have h₁ : ∀ x ∈ t a,∀ y ∈ t a,
-      x ≠ y → Disjoint (image (pi.cons s a x) (pi s t)) (image (pi.cons s a y) (pi s t)) := by
+  · have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
+      Disjoint (image (pi.cons s a x) (pi s t)) (image (pi.cons s a y) (pi s t)) := by
       intro x _ y _ h
       simp only [disjoint_iff_ne, mem_image]
       rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
@@ -166,8 +164,7 @@ theorem prod_add_ordered {ι R : Type _} [CommSemiring R] [LinearOrder ι] (s :
     ∏ i in s, (f i + g i) =
       (∏ i in s, f i) +
         ∑ i in s,
-          g i * (∏ j in s.filter (· < i), (f j + g j)) * ∏ j in s.filter fun j => i < j, f j :=
-  by
+          g i * (∏ j in s.filter (· < i), (f j + g j)) * ∏ j in s.filter fun j => i < j, f j := by
   refine' Finset.induction_on_max s (by simp) _
   clear s
   intro a s ha ihs
@@ -191,8 +188,7 @@ theorem prod_sub_ordered {ι R : Type _} [CommRing R] [LinearOrder ι] (s : Fins
     ∏ i in s, (f i - g i) =
       (∏ i in s, f i) -
         ∑ i in s,
-          g i * (∏ j in s.filter (· < i), (f j - g j)) * ∏ j in s.filter fun j => i < j, f j :=
-  by
+          g i * (∏ j in s.filter (· < i), (f j - g j)) * ∏ j in s.filter fun j => i < j, f j := by
   simp only [sub_eq_add_neg]
   convert prod_add_ordered s f fun i => -g i
   simp
@@ -201,17 +197,15 @@ theorem prod_sub_ordered {ι R : Type _} [CommRing R] [LinearOrder ι] (s : Fins
 /-- `∏ i, (1 - f i) = 1 - ∑ i, f i * (∏ j < i, 1 - f j)`. This formula is useful in construction of
 a partition of unity from a collection of “bump” functions.  -/
 theorem prod_one_sub_ordered {ι R : Type _} [CommRing R] [LinearOrder ι] (s : Finset ι)
-    (f : ι → R) : ∏ i in s, (1 - f i) = 1 - ∑ i in s, f i * ∏ j in s.filter (· < i), (1 - f j) :=
-  by
+    (f : ι → R) : ∏ i in s, (1 - f i) = 1 - ∑ i in s, f i * ∏ j in s.filter (· < i), (1 - f j) := by
   rw [prod_sub_ordered]
   simp
 #align finset.prod_one_sub_ordered Finset.prod_one_sub_ordered
 
 /-- Summing `a^s.card * b^(n-s.card)` over all finite subsets `s` of a `Finset`
 gives `(a + b)^s.card`.-/
 theorem sum_pow_mul_eq_add_pow {α R : Type _} [CommSemiring R] (a b : R) (s : Finset α) :
-    (∑ t in s.powerset, a ^ t.card * b ^ (s.card - t.card)) = (a + b) ^ s.card :=
-  by
+    (∑ t in s.powerset, a ^ t.card * b ^ (s.card - t.card)) = (a + b) ^ s.card := by
   rw [← prod_const, prod_add]
   refine' Finset.sum_congr rfl fun t ht => _
   rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]
@@ -222,9 +216,9 @@ theorem dvd_sum {b : β} {s : Finset α} {f : α → β} (h : ∀ x ∈ s, b ∣
 #align finset.dvd_sum Finset.dvd_sum
 
 @[norm_cast]
-theorem prod_nat_cast (s : Finset α) (f : α → ℕ) : ↑(∏ x in s, f x : ℕ) = ∏ x in s, (f x : β) :=
+theorem prod_natCast (s : Finset α) (f : α → ℕ) : ↑(∏ x in s, f x : ℕ) = ∏ x in s, (f x : β) :=
   (Nat.castRingHom β).map_prod f s
-#align finset.prod_nat_cast Finset.prod_nat_cast
+#align finset.prod_nat_cast Finset.prod_natCast
 
 end CommSemiring
 
@@ -235,7 +229,7 @@ variable {R : Type _} [CommRing R]
 theorem prod_range_cast_nat_sub (n k : ℕ) :
     ∏ i in range k, (n - i : R) = (∏ i in range k, (n - i) : ℕ) :=
   by
-  rw [prod_nat_cast]
+  rw [prod_natCast]
   cases' le_or_lt k n with hkn hnk
   · exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm
   · rw [← mem_range] at hnk
@@ -252,8 +246,7 @@ of `s`, and over all subsets of `s` to which one adds `x`. -/
 theorem prod_powerset_insert [DecidableEq α] [CommMonoid β] {s : Finset α} {x : α} (h : x ∉ s)
     (f : Finset α → β) :
     (∏ a in (insert x s).powerset, f a) =
-      (∏ a in s.powerset, f a) * ∏ t in s.powerset, f (insert x t) :=
-  by
+      (∏ a in s.powerset, f a) * ∏ t in s.powerset, f (insert x t) := by
   rw [powerset_insert, Finset.prod_union, Finset.prod_image]
   · intro t₁ h₁ t₂ h₂ heq
     rw [← Finset.erase_insert (not_mem_of_mem_powerset_of_not_mem h₁ h), ←
@@ -279,8 +272,8 @@ theorem sum_range_succ_mul_sum_range_succ [NonUnitalNonAssocSemiring β] (n k :
     ((∑ i in range (n + 1), f i) * ∑ i in range (k + 1), g i) =
       (((∑ i in range n, f i) * ∑ i in range k, g i) + f n * ∑ i in range k, g i) +
           (∑ i in range n, f i) * g k +
-        f n * g k :=
-  by simp only [add_mul, mul_add, add_assoc, sum_range_succ]
+        f n * g k := by
+  simp only [add_mul, mul_add, add_assoc, sum_range_succ]
 #align finset.sum_range_succ_mul_sum_range_succ Finset.sum_range_succ_mul_sum_range_succ
 
 end Finset

Mathlib/Algebra/Order/Monoid/Lemmas.lean

@@ -1277,47 +1277,47 @@ theorem StrictAntiOn.mul' [CovariantClass α α (· * ·) (· < ·)]
 #align strict_anti_on.add StrictAntiOn.add
 
 /-- The product of a monotone function and a strictly monotone function is strictly monotone. -/
-@[to_additive add_strict_mono "The sum of a monotone function and a strictly monotone function is
+@[to_additive add_strictMono "The sum of a monotone function and a strictly monotone function is
 strictly monotone."]
-theorem Monotone.mul_strict_mono' [CovariantClass α α (· * ·) (· < ·)]
+theorem Monotone.mul_strictMono' [CovariantClass α α (· * ·) (· < ·)]
     [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {f g : β → α} (hf : Monotone f)
     (hg : StrictMono g) :
     StrictMono fun x => f x * g x :=
   fun _ _ h => mul_lt_mul_of_le_of_lt (hf h.le) (hg h)
-#align monotone.mul_strict_mono' Monotone.mul_strict_mono'
-#align monotone.add_strict_mono Monotone.add_strict_mono
+#align monotone.mul_strict_mono' Monotone.mul_strictMono'
+#align monotone.add_strict_mono Monotone.add_strictMono
 
 /-- The product of a monotone function and a strictly monotone function is strictly monotone. -/
-@[to_additive add_strict_mono "The sum of a monotone function and a strictly monotone function is
+@[to_additive add_strictMono "The sum of a monotone function and a strictly monotone function is
 strictly monotone."]
-theorem MonotoneOn.mul_strict_mono' [CovariantClass α α (· * ·) (· < ·)]
+theorem MonotoneOn.mul_strictMono' [CovariantClass α α (· * ·) (· < ·)]
     [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {f g : β → α} (hf : MonotoneOn f s)
     (hg : StrictMonoOn g s) : StrictMonoOn (fun x => f x * g x) s :=
   fun _ hx _ hy h => mul_lt_mul_of_le_of_lt (hf hx hy h.le) (hg hx hy h)
-#align monotone_on.mul_strict_mono' MonotoneOn.mul_strict_mono'
-#align monotone_on.add_strict_mono MonotoneOn.add_strict_mono
+#align monotone_on.mul_strict_mono' MonotoneOn.mul_strictMono'
+#align monotone_on.add_strict_mono MonotoneOn.add_strictMono
 
 /-- The product of a antitone function and a strictly antitone function is strictly antitone. -/
-@[to_additive add_strict_anti "The sum of a antitone function and a strictly antitone function is
+@[to_additive add_strictAnti "The sum of a antitone function and a strictly antitone function is
 strictly antitone."]
-theorem Antitone.mul_strict_anti' [CovariantClass α α (· * ·) (· < ·)]
+theorem Antitone.mul_strictAnti' [CovariantClass α α (· * ·) (· < ·)]
     [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {f g : β → α} (hf : Antitone f)
     (hg : StrictAnti g) :
     StrictAnti fun x => f x * g x :=
   fun _ _ h => mul_lt_mul_of_le_of_lt (hf h.le) (hg h)
-#align antitone.mul_strict_anti' Antitone.mul_strict_anti'
-#align antitone.add_strict_anti Antitone.add_strict_anti
+#align antitone.mul_strict_anti' Antitone.mul_strictAnti'
+#align antitone.add_strict_anti Antitone.add_strictAnti
 
 /-- The product of a antitone function and a strictly antitone function is strictly antitone. -/
-@[to_additive add_strict_anti "The sum of a antitone function and a strictly antitone function is
+@[to_additive add_strictAnti "The sum of a antitone function and a strictly antitone function is
 strictly antitone."]
-theorem AntitoneOn.mul_strict_anti' [CovariantClass α α (· * ·) (· < ·)]
+theorem AntitoneOn.mul_strictAnti' [CovariantClass α α (· * ·) (· < ·)]
     [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {f g : β → α} (hf : AntitoneOn f s)
     (hg : StrictAntiOn g s) :
     StrictAntiOn (fun x => f x * g x) s :=
   fun _ hx _ hy h => mul_lt_mul_of_le_of_lt (hf hx hy h.le) (hg hx hy h)
-#align antitone_on.mul_strict_anti' AntitoneOn.mul_strict_anti'
-#align antitone_on.add_strict_anti AntitoneOn.add_strict_anti
+#align antitone_on.mul_strict_anti' AntitoneOn.mul_strictAnti'
+#align antitone_on.add_strict_anti AntitoneOn.add_strictAnti
 
 variable [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· < ·)]
 
@@ -1490,9 +1490,9 @@ theorem bit0_mono [CovariantClass α α (· + ·) (· ≤ ·)] [CovariantClass 
 #align bit0_mono bit0_mono
 
 @[deprecated]
-theorem bit0_strict_mono [CovariantClass α α (· + ·) (· < ·)]
+theorem bit0_strictMono [CovariantClass α α (· + ·) (· < ·)]
     [CovariantClass α α (swap (· + ·)) (· < ·)] :
     StrictMono (bit0 : α → α) := fun _ _ h => add_lt_add h h
-#align bit0_strict_mono bit0_strict_mono
+#align bit0_strict_mono bit0_strictMono
 
 end Bit

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -154,11 +154,11 @@ def consCases {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fi
 #align fin.cons_cases Fin.consCases
 
 @[simp]
-theorem cons_cases_cons {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x))
+theorem consCases_cons {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x))
     (x₀ : α 0) (x : ∀ i : Fin n, α i.succ) : @consCases _ _ _ h (cons x₀ x) = h x₀ x := by
   rw [consCases, cast_eq]
   congr
-#align fin.cons_cases_cons Fin.cons_cases_cons
+#align fin.cons_cases_cons Fin.consCases_cons
 
 /-- Recurse on an tuple by splitting into `Fin.elim0` and `Fin.cons`. -/
 @[elab_as_elim]
@@ -289,7 +289,7 @@ theorem range_cons {α : Type _} {n : ℕ} (x : α) (b : Fin n → α) :
 section Append
 
 /-- Append a tuple of length `m` to a tuple of length `n` to get a tuple of length `m + n`.
-This is a non-dependent version of `fin.add_cases`. -/
+This is a non-dependent version of `Fin.add_cases`. -/
 def append {α : Type _} (a : Fin m → α) (b : Fin n → α) : Fin (m + n) → α :=
   @Fin.addCases _ _ (fun _ => α) a b
 #align fin.append Fin.append
@@ -935,7 +935,7 @@ theorem sigma_eq_of_eq_comp_cast {α : Type _} :
     simpa using h
 #align fin.sigma_eq_of_eq_comp_cast Fin.sigma_eq_of_eq_comp_cast
 
-/-- `fin.sigma_eq_of_eq_comp_cast` as an `iff`. -/
+/-- `Fin.sigma_eq_of_eq_comp_cast` as an `iff`. -/
 theorem sigma_eq_iff_eq_comp_cast {α : Type _} {a b : Σii, Fin ii → α} :
     a = b ↔ ∃ h : a.fst = b.fst, a.snd = b.snd ∘ Fin.cast h :=
   ⟨fun h ↦ h ▸ ⟨rfl, funext <| Fin.rec fun _ _ ↦ rfl⟩, fun ⟨_, h'⟩ ↦