chore(Data/Nat/Choose/Sum): clean up (#15935)

Author: Parcly-Taxel

Mathlib/Data/Nat/Choose/Sum.lean

@@ -17,13 +17,9 @@ import Mathlib.Tactic.Ring
 This file includes variants of the binomial theorem and other results on sums of binomial
 coefficients. Theorems whose proofs depend on such sums may also go in this file for import
 reasons.
-
 -/
 
-
-open Nat
-
-open Finset
+open Nat Finset
 
 variable {R : Type*}
 
@@ -33,114 +29,116 @@ variable [Semiring R] {x y : R}
 
 /-- A version of the **binomial theorem** for commuting elements in noncommutative semirings. -/
 theorem add_pow (h : Commute x y) (n : ℕ) :
-    (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * choose n m := by
-  let t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * choose n m
+    (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * n.choose m := by
+  let t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * n.choose m
   change (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
   have h_first : ∀ n, t n 0 = y ^ n := fun n ↦ by
-    simp only [t, choose_zero_right, _root_.pow_zero, Nat.cast_one, mul_one, one_mul, tsub_zero]
+    simp only [t, choose_zero_right, pow_zero, cast_one, mul_one, one_mul, tsub_zero]
   have h_last : ∀ n, t n n.succ = 0 := fun n ↦ by
     simp only [t, choose_succ_self, cast_zero, mul_zero]
   have h_middle :
-    ∀ n i : ℕ, i ∈ range n.succ → (t n.succ (Nat.succ i)) =
-      x * t n i + y * t n i.succ := by
+      ∀ n i : ℕ, i ∈ range n.succ → (t n.succ i.succ) = x * t n i + y * t n i.succ := by
     intro n i h_mem
-    have h_le : i ≤ n := Nat.le_of_lt_succ (mem_range.mp h_mem)
+    have h_le : i ≤ n := le_of_lt_succ (mem_range.mp h_mem)
     dsimp only [t]
-    rw [choose_succ_succ, Nat.cast_add, mul_add]
+    rw [choose_succ_succ, cast_add, mul_add]
     congr 1
     · rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
     · rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
       by_cases h_eq : i = n
-      · rw [h_eq, choose_succ_self, Nat.cast_zero, mul_zero, mul_zero]
+      · rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
       · rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
         rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
-  induction' n with n ih
-  · rw [_root_.pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
+  induction n with
+  | zero =>
+    rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
     dsimp only [t]
-    rw [_root_.pow_zero, _root_.pow_zero, choose_self, Nat.cast_one, mul_one, mul_one]
-  · rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
+    rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
+  | succ n ih =>
+    rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
       pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]
     congr 1
     rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
 
 /-- A version of `Commute.add_pow` that avoids ℕ-subtraction by summing over the antidiagonal and
 also with the binomial coefficient applied via scalar action of ℕ. -/
 theorem add_pow' (h : Commute x y) (n : ℕ) :
-    (x + y) ^ n = ∑ m ∈ antidiagonal n, choose n m.fst • (x ^ m.fst * y ^ m.snd) := by
-  simp_rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ choose n m • (x ^ m * y ^ p),
-    _root_.nsmul_eq_mul, cast_comm, h.add_pow]
+    (x + y) ^ n = ∑ m ∈ antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2) := by
+  simp_rw [Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p),
+    nsmul_eq_mul, cast_comm, h.add_pow]
 
 end Commute
 
 /-- The **binomial theorem** -/
 theorem add_pow [CommSemiring R] (x y : R) (n : ℕ) :
-    (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * choose n m :=
+    (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * n.choose m :=
   (Commute.all x y).add_pow n
 
 namespace Nat
 
 /-- The sum of entries in a row of Pascal's triangle -/
-theorem sum_range_choose (n : ℕ) : (∑ m ∈ range (n + 1), choose n m) = 2 ^ n := by
+theorem sum_range_choose (n : ℕ) : (∑ m ∈ range (n + 1), n.choose m) = 2 ^ n := by
   have := (add_pow 1 1 n).symm
   simpa [one_add_one_eq_two] using this
 
-theorem sum_range_choose_halfway (m : Nat) : (∑ i ∈ range (m + 1), choose (2 * m + 1) i) = 4 ^ m :=
-  have : (∑ i ∈ range (m + 1), choose (2 * m + 1) (2 * m + 1 - i)) =
-      ∑ i ∈ range (m + 1), choose (2 * m + 1) i :=
+theorem sum_range_choose_halfway (m : ℕ) : (∑ i ∈ range (m + 1), (2 * m + 1).choose i) = 4 ^ m :=
+  have : (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) =
+      ∑ i ∈ range (m + 1), (2 * m + 1).choose i :=
     sum_congr rfl fun i hi ↦ choose_symm <| by linarith [mem_range.1 hi]
   mul_right_injective₀ two_ne_zero <|
     calc
-      (2 * ∑ i ∈ range (m + 1), choose (2 * m + 1) i) =
-          (∑ i ∈ range (m + 1), choose (2 * m + 1) i) +
-            ∑ i ∈ range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) := by rw [two_mul, this]
-      _ = (∑ i ∈ range (m + 1), choose (2 * m + 1) i) +
-            ∑ i ∈ Ico (m + 1) (2 * m + 2), choose (2 * m + 1) i := by
-        { rw [range_eq_Ico, sum_Ico_reflect]
-          · congr
-            have A : m + 1 ≤ 2 * m + 1 := by omega
-            rw [add_comm, add_tsub_assoc_of_le A, ← add_comm]
-            congr
-            rw [tsub_eq_iff_eq_add_of_le A]
-            ring
-          · omega }
-      _ = ∑ i ∈ range (2 * m + 2), choose (2 * m + 1) i := sum_range_add_sum_Ico _ (by omega)
+      (2 * ∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
+          (∑ i ∈ range (m + 1), (2 * m + 1).choose i) +
+            ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) := by rw [two_mul, this]
+      _ = (∑ i ∈ range (m + 1), (2 * m + 1).choose i) +
+            ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i := by
+        rw [range_eq_Ico, sum_Ico_reflect _ _ (by omega)]
+        congr
+        have A : m + 1 ≤ 2 * m + 1 := by omega
+        rw [add_comm, add_tsub_assoc_of_le A, ← add_comm]
+        congr
+        rw [tsub_eq_iff_eq_add_of_le A]
+        ring
+      _ = ∑ i ∈ range (2 * m + 2), (2 * m + 1).choose i := sum_range_add_sum_Ico _ (by omega)
       _ = 2 ^ (2 * m + 1) := sum_range_choose (2 * m + 1)
-      _ = 2 * 4 ^ m := by rw [Nat.pow_succ, pow_mul, mul_comm]; rfl
+      _ = 2 * 4 ^ m := by rw [pow_succ, pow_mul, mul_comm]; rfl
 
-theorem choose_middle_le_pow (n : ℕ) : choose (2 * n + 1) n ≤ 4 ^ n := by
-  have t : choose (2 * n + 1) n ≤ ∑ i ∈ range (n + 1), choose (2 * n + 1) i :=
+theorem choose_middle_le_pow (n : ℕ) : (2 * n + 1).choose n ≤ 4 ^ n := by
+  have t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i :=
     single_le_sum (fun x _ ↦ by omega) (self_mem_range_succ n)
   simpa [sum_range_choose_halfway n] using t
 
 theorem four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) :
-    4 ^ n ≤ (2 * n + 1) * choose (2 * n) n :=
+    4 ^ n ≤ (2 * n + 1) * (2 * n).choose n :=
   calc
     4 ^ n = (1 + 1) ^ (2 * n) := by norm_num [pow_mul]
-    _ = ∑ m ∈ range (2 * n + 1), choose (2 * n) m := by set_option simprocs false in simp [add_pow]
-    _ ≤ ∑ m ∈ range (2 * n + 1), choose (2 * n) (2 * n / 2) := by gcongr; apply choose_le_middle
+    _ = ∑ m ∈ range (2 * n + 1), (2 * n).choose m := by set_option simprocs false in simp [add_pow]
+    _ ≤ ∑ m ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2) := by gcongr; apply choose_le_middle
     _ = (2 * n + 1) * choose (2 * n) n := by simp
 
 /-- **Zhu Shijie's identity** aka hockey-stick identity. -/
 theorem sum_Icc_choose (n k : ℕ) : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1) := by
-  cases' le_or_gt k n with h h
-  · induction' n, h using le_induction with n _ ih; · simp
-    rw [← Ico_insert_right (by omega), sum_insert (by simp),
-      show Ico k (n + 1) = Icc k n by rfl, ih, choose_succ_succ' (n + 1)]
+  rcases lt_or_le n k with h | h
   · rw [choose_eq_zero_of_lt (by omega), Icc_eq_empty_of_lt h, sum_empty]
+  · induction n, h using le_induction with
+    | base => simp
+    | succ n _ ih =>
+      rw [← Ico_insert_right (by omega), sum_insert (by simp),
+        show Ico k (n + 1) = Icc k n by rfl, ih, choose_succ_succ' (n + 1)]
 
 end Nat
 
 theorem Int.alternating_sum_range_choose {n : ℕ} :
-    (∑ m ∈ range (n + 1), ((-1) ^ m * ↑(choose n m) : ℤ)) = if n = 0 then 1 else 0 := by
+    (∑ m ∈ range (n + 1), ((-1) ^ m * n.choose m : ℤ)) = if n = 0 then 1 else 0 := by
   cases n with
   | zero => simp
   | succ n =>
     have h := add_pow (-1 : ℤ) 1 n.succ
     simp only [one_pow, mul_one, neg_add_cancel] at h
-    rw [← h, zero_pow n.succ_ne_zero, if_neg (Nat.succ_ne_zero n)]
+    rw [← h, zero_pow n.succ_ne_zero, if_neg n.succ_ne_zero]
 
 theorem Int.alternating_sum_range_choose_of_ne {n : ℕ} (h0 : n ≠ 0) :
-    (∑ m ∈ range (n + 1), ((-1) ^ m * ↑(choose n m) : ℤ)) = 0 := by
+    (∑ m ∈ range (n + 1), ((-1) ^ m * n.choose m : ℤ)) = 0 := by
   rw [Int.alternating_sum_range_choose, if_neg h0]
 
 namespace Finset
@@ -166,9 +164,8 @@ theorem sum_powerset_neg_one_pow_card {α : Type*} [DecidableEq α] {x : Finset
 theorem sum_powerset_neg_one_pow_card_of_nonempty {α : Type*} {x : Finset α} (h0 : x.Nonempty) :
     (∑ m ∈ x.powerset, (-1 : ℤ) ^ m.card) = 0 := by
   classical
-    rw [sum_powerset_neg_one_pow_card, if_neg]
-    rw [← Ne, ← nonempty_iff_ne_empty]
-    apply h0
+  rw [sum_powerset_neg_one_pow_card]
+  exact if_neg (nonempty_iff_ne_empty.mp h0)
 
 variable {M R : Type*} [CommMonoid M] [NonAssocSemiring R]
 
@@ -179,10 +176,9 @@ theorem prod_pow_choose_succ {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M)
         ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i := by
   have A : (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ (n.choose (i + 1))) * f 0 (n + 1) =
       ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ (n.choose i) := by
-    rw [prod_range_succ, prod_range_succ']
-    simp
+    rw [prod_range_succ, prod_range_succ']; simp
   rw [prod_range_succ']
-  simpa [Nat.choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using mul_comm _ _
+  simpa [choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using mul_comm _ _
 
 @[to_additive sum_antidiagonal_choose_succ_nsmul]
 theorem prod_antidiagonal_pow_choose_succ {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) :
@@ -195,9 +191,8 @@ theorem prod_antidiagonal_pow_choose_succ {M : Type*} [CommMonoid M] (f : ℕ 
   · refine prod_congr rfl fun i hi ↦ ?_
     rw [tsub_add_eq_add_tsub (this _ hi)]
   · refine prod_congr rfl fun i hi ↦ ?_
-    rw [Nat.choose_symm (this _ hi)]
+    rw [choose_symm (this _ hi)]
 
--- Porting note: moved from `Mathlib.Analysis.Calculus.ContDiff`
 /-- The sum of `(n+1).choose i * f i (n+1-i)` can be split into two sums at rank `n`,
 respectively of `n.choose i * f i (n+1-i)` and `n.choose i * f (i+1) (n-i)`. -/
 theorem sum_choose_succ_mul (f : ℕ → ℕ → R) (n : ℕ) :
@@ -215,8 +210,7 @@ theorem sum_antidiagonal_choose_succ_mul (f : ℕ → ℕ → R) (n : ℕ) :
   simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n
 
 theorem sum_antidiagonal_choose_add (d n : ℕ) :
-    (Finset.sum (antidiagonal n) fun ij => (d + ij.2).choose d) =
-    (d + n).choose d + (d + n).choose (succ d) := by
+    (∑ ij ∈ antidiagonal n, (d + ij.2).choose d) = (d + n).choose d + (d + n).choose (d + 1) := by
   induction n with
   | zero => simp
   | succ n hn => simpa [Nat.sum_antidiagonal_succ] using hn