chore(Data/Nat/Choose/Sum): refined the statement of `Finset.sum_anti…

…diagonal_choose_add`. (#21022)
leanprover-community · Jan 24, 2025 · 4c0603b · 4c0603b
1 parent 8527b66
commit 4c0603b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git a/Mathlib/Data/Nat/Choose/Sum.lean b/Mathlib/Data/Nat/Choose/Sum.lean
@@ -230,9 +230,9 @@ 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 : ℕ) :
-    (∑ ij ∈ antidiagonal n, (d + ij.2).choose d) = (d + n).choose d + (d + n).choose (d + 1) := by
+    (∑ ij ∈ antidiagonal n, (d + ij.2).choose d) = (d + n + 1).choose (d + 1) := by
   induction n with
   | zero => simp
-  | succ n hn => simpa [Nat.sum_antidiagonal_succ] using hn
+  | succ n hn => rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]
 
 end Finset
diff --git a/Mathlib/RingTheory/PowerSeries/WellKnown.lean b/Mathlib/RingTheory/PowerSeries/WellKnown.lean
@@ -93,8 +93,7 @@ theorem mk_one_pow_eq_mk_choose_add :
       rw [pow_add, hd, pow_one, mul_comm, coeff_mul]
       simp_rw [coeff_mk, Pi.one_apply, one_mul]
       norm_cast
-      rw [Finset.sum_antidiagonal_choose_add, ← Nat.choose_succ_succ, Nat.succ_eq_add_one,
-        add_right_comm]
+      rw [Finset.sum_antidiagonal_choose_add, add_right_comm]
 
 /--
 Given a natural number `d : ℕ` and a commutative ring `S`, `PowerSeries.invOneSubPow S d` is the