From 71767a964ddad045e893970075a54f7a55cdd2f5 Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Sun, 22 Oct 2023 04:11:54 +0900
Subject: [PATCH 01/12] Update Basic.lean

shift Nat.ascFactorial by one to agree with ascending factorial in mathematical literature.
---
 Mathlib/Data/Nat/Factorial/Basic.lean | 114 ++++++++++++--------------
 1 file changed, 53 insertions(+), 61 deletions(-)

diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index 94d16f785ef1e..3b4a22e2eb703 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -18,9 +18,10 @@ This file defines the factorial, along with the ascending and descending variant
 ## Main declarations
 
 * `Nat.factorial`: The factorial.
-* `Nat.ascFactorial`: The ascending factorial. Note that it runs from `n + 1` to `n + k`
-  and *not* from `n` to `n + k - 1`. We might want to change that in the future.
-* `Nat.descFactorial`: The descending factorial. It runs from `n - k` to `n`.
+* `Nat.ascFactorial`: The ascending factorial. It is the product of natural numbers from `n` to
+  `n + k - 1`.
+* `Nat.descFactorial`: The descending factorial. It is the product of natural numbers from
+  `n - k + 1` to `n`.
 -/
 
 
@@ -226,12 +227,11 @@ end Factorial
 
 section AscFactorial
 
-/-- `n.ascFactorial k = (n + k)! / n!` (as seen in `Nat.ascFactorial_eq_div`), but implemented
-recursively to allow for "quick" computation when using `norm_num`. This is closely related to
-`ascPochhammer`, but much less general. -/
+/-- `n.ascFactorial k = n (n + 1) ⋯ (n + k - 1)`. This is closely related to `ascPochhammer`, but
+much less general. -/
 def ascFactorial (n : ℕ) : ℕ → ℕ
   | 0 => 1
-  | k + 1 => (n + k + 1) * ascFactorial n k
+  | k + 1 => (n + k) * ascFactorial n k
 #align nat.asc_factorial Nat.ascFactorial
 
 @[simp]
@@ -239,97 +239,88 @@ theorem ascFactorial_zero (n : ℕ) : n.ascFactorial 0 = 1 :=
   rfl
 #align nat.asc_factorial_zero Nat.ascFactorial_zero
 
-@[simp]
-theorem zero_ascFactorial (k : ℕ) : (0 : ℕ).ascFactorial k = k ! := by
-  induction' k with t ht
-  · rfl
-  rw [ascFactorial, ht, zero_add, Nat.factorial_succ]
-#align nat.zero_asc_factorial Nat.zero_ascFactorial
-
-theorem ascFactorial_succ {n k : ℕ} : n.ascFactorial k.succ = (n + k + 1) * n.ascFactorial k :=
+theorem ascFactorial_succ {n k : ℕ} : n.ascFactorial k.succ = (n + k) * n.ascFactorial k :=
   rfl
 #align nat.asc_factorial_succ Nat.ascFactorial_succ
 
--- Porting note: Explicit arguments are required to show that the recursion terminates
+@[simp]
+theorem zero_ascFactorial : ∀ (k : ℕ), (0 : ℕ).ascFactorial k.succ = 0
+  | 0 => by
+    simp only
+  | (k+1) => by
+    rw [ascFactorial_succ, zero_ascFactorial k, mul_zero]
+
 theorem succ_ascFactorial (n : ℕ) :
-    ∀ k, (n + 1) * n.succ.ascFactorial k = (n + k + 1) * n.ascFactorial k
+    ∀ k, n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
   | 0 => by rw [add_zero, ascFactorial_zero, ascFactorial_zero]
   | k + 1 => by
     rw [ascFactorial, mul_left_comm, succ_ascFactorial n k, ascFactorial,
       succ_add, ← add_assoc, succ_eq_add_one]
 #align nat.succ_asc_factorial Nat.succ_ascFactorial
 
-/-- `n.ascFactorial k = (n + k)! / n!` but without ℕ-division. See `Nat.ascFactorial_eq_div` for
-the version with ℕ-division. -/
--- Porting note: Explicit arguments are required to show that the recursion terminates
--- Porting note: Interconversion between `succ` and `· + 1` has to be done manually
-theorem factorial_mul_ascFactorial (n : ℕ) : ∀ k, n ! * n.ascFactorial k = (n + k)!
+/-- `n.ascFactorial k = (n + k - 1)! / (n - 1)!` for `n > 0` but without ℕ-division. See
+`Nat.ascFactorial_eq_div` for the version with ℕ-division. -/
+theorem factorial_mul_ascFactorial (n : ℕ) (h : 0 < n) :
+    ∀ k, (n - 1) ! * n.ascFactorial k = (n + k - 1)!
   | 0 => by rw [ascFactorial, add_zero, mul_one]
   | k + 1 => by
-    rw [ascFactorial_succ, mul_left_comm, factorial_mul_ascFactorial n k,
-      ← add_assoc, ← Nat.succ_eq_add_one (n + k), factorial]
+    rw [ascFactorial_succ, mul_left_comm, factorial_mul_ascFactorial n h k, ← add_assoc]
+    exact mul_factorial_pred (add_pos_left h k)
 #align nat.factorial_mul_asc_factorial Nat.factorial_mul_ascFactorial
 
 /-- Avoid in favor of `Nat.factorial_mul_ascFactorial` if you can. ℕ-division isn't worth it. -/
-theorem ascFactorial_eq_div (n k : ℕ) : n.ascFactorial k = (n + k)! / n ! := by
-  apply mul_left_cancel₀ n.factorial_ne_zero
-  rw [factorial_mul_ascFactorial]
-  exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| le.intro rfl).symm
+theorem ascFactorial_eq_div (n k : ℕ) (h : 0 < n) :
+    n.ascFactorial k = (n + k - 1)! / (n - 1) ! := by
+  apply mul_left_cancel₀ (n-1).factorial_ne_zero
+  rw [factorial_mul_ascFactorial _ h]
+  exact (Nat.mul_div_cancel_left' <| factorial_dvd_factorial <| Nat.sub_le_sub_right
+    (le_add_right n k) 1).symm
 #align nat.asc_factorial_eq_div Nat.ascFactorial_eq_div
 
-theorem ascFactorial_of_sub {n k : ℕ} (h : k < n) :
-    (n - k) * (n - k).ascFactorial k = (n - (k + 1)).ascFactorial (k + 1) := by
-  let t := n - k.succ
-  let ht : t = n - k.succ := rfl
-  suffices h' : n - k = t.succ by rw [← ht, h', succ_ascFactorial, ascFactorial_succ]
-  rw [ht, succ_eq_add_one, ← tsub_tsub_assoc (succ_le_of_lt h) (succ_pos _), succ_sub_one]
+theorem ascFactorial_of_sub {n k : ℕ}:
+    (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1) := by
+  rw [succ_ascFactorial, ascFactorial_succ]
 #align nat.asc_factorial_of_sub Nat.ascFactorial_of_sub
 
-theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, (n + 1) ^ k ≤ n.ascFactorial k
+theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, n ^ k ≤ n.ascFactorial k
   | 0 => by rw [ascFactorial_zero, pow_zero]
   | k + 1 => by
-    rw [pow_succ, mul_comm]
-    exact Nat.mul_le_mul (Nat.add_le_add_right le_self_add _) (pow_succ_le_ascFactorial _ k)
+    rw [pow_succ, mul_comm, ascFactorial_succ, ← succ_ascFactorial]
+    exact Nat.mul_le_mul (Nat.le_refl n)
+      ((pow_le_pow_of_le_left' (le_succ n) k).trans (pow_succ_le_ascFactorial n.succ k))
 #align nat.pow_succ_le_asc_factorial Nat.pow_succ_le_ascFactorial
 
-theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < n.ascFactorial (k + 2) := by
+theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2) := by
   rw [pow_succ, ascFactorial, mul_comm]
-  exact
-    Nat.mul_lt_mul (Nat.add_lt_add_right (Nat.lt_add_of_pos_right succ_pos') 1)
-      (pow_succ_le_ascFactorial n _) (pow_pos succ_pos' _)
+  exact Nat.mul_lt_mul (lt_add_of_pos_right (n + 1) (succ_pos k))
+    (pow_succ_le_ascFactorial n.succ _) (NeZero.pos ((n + 1) ^ (k + 1)))
 #align nat.pow_lt_asc_factorial' Nat.pow_lt_ascFactorial'
 
-theorem pow_lt_ascFactorial (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1) ^ k < n.ascFactorial k
+theorem pow_lt_ascFactorial (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k
   | 0 => by rintro ⟨⟩
   | 1 => by intro; contradiction
   | k + 2 => fun _ => pow_lt_ascFactorial' n k
 #align nat.pow_lt_asc_factorial Nat.pow_lt_ascFactorial
 
-theorem ascFactorial_le_pow_add (n : ℕ) : ∀ k : ℕ, n.ascFactorial k ≤ (n + k) ^ k
+theorem ascFactorial_le_pow_add (n : ℕ) : ∀ k : ℕ, (n+1).ascFactorial k ≤ (n + k) ^ k
   | 0 => by rw [ascFactorial_zero, pow_zero]
   | k + 1 => by
-    rw [ascFactorial_succ, pow_succ, ← add_assoc,
-    ← Nat.succ_eq_add_one (n + k), mul_comm _ (succ (n + k))]
-    exact
-      Nat.mul_le_mul_of_nonneg_left
-        ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_of_le_left (le_succ _) _))
+    rw [ascFactorial_succ, pow_succ, mul_comm, ← add_assoc, add_right_comm n 1 k]
+    exact Nat.mul_le_mul_of_nonneg_right
+      ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_of_le_left (le_succ _) _))
 #align nat.asc_factorial_le_pow_add Nat.ascFactorial_le_pow_add
 
-theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → n.ascFactorial k < (n + k) ^ k
+theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1).ascFactorial k < (n + k) ^ k
   | 0 => by rintro ⟨⟩
   | 1 => by intro; contradiction
   | k + 2 => fun _ => by
-    rw [ascFactorial_succ, pow_succ]
-    rw [add_assoc n (k + 1) 1, mul_comm <| (n + (k + 2)) ^ (k + 1)]
-    refine'
-      Nat.mul_lt_mul' le_rfl
-        ((ascFactorial_le_pow_add n _).trans_lt
-          (pow_lt_pow_of_lt_left (lt_add_one _) (succ_pos _)))
-        (succ_pos _)
+    rw [pow_succ, mul_comm, ascFactorial_succ, succ_add_eq_succ_add n (k + 1)]
+    exact Nat.mul_lt_mul' le_rfl ((ascFactorial_le_pow_add n _).trans_lt
+      (pow_lt_pow_of_lt_left (lt_add_one _) (succ_pos _))) (succ_pos _)
 #align nat.asc_factorial_lt_pow_add Nat.ascFactorial_lt_pow_add
 
-theorem ascFactorial_pos (n k : ℕ) : 0 < n.ascFactorial k :=
-  (pow_pos (succ_pos n) k).trans_le (pow_succ_le_ascFactorial n k)
+theorem ascFactorial_pos (n k : ℕ) : 0 < (n + 1).ascFactorial k :=
+  (pow_pos (succ_pos n) k).trans_le (pow_succ_le_ascFactorial (n + 1) k)
 #align nat.asc_factorial_pos Nat.ascFactorial_pos
 
 end AscFactorial
@@ -409,11 +400,12 @@ alias ⟨_, descFactorial_of_lt⟩ := descFactorial_eq_zero_iff_lt
 #align nat.desc_factorial_of_lt Nat.descFactorial_of_lt
 
 theorem add_descFactorial_eq_ascFactorial (n : ℕ) :
-    ∀ k : ℕ, (n + k).descFactorial k = n.ascFactorial k
+    ∀ k : ℕ, (n + k - 1).descFactorial k = n.ascFactorial k
   | 0 => by rw [ascFactorial_zero, descFactorial_zero]
   | succ k => by
-    rw [Nat.add_succ, Nat.succ_eq_add_one, Nat.succ_eq_add_one,
-        succ_descFactorial_succ, ascFactorial_succ, add_descFactorial_eq_ascFactorial _ k]
+    rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_succ_add,
+      add_descFactorial_eq_ascFactorial _ k, ← succ_ascFactorial, succ_add_sub_one,
+      Nat.add_sub_cancel]
 #align nat.add_desc_factorial_eq_asc_factorial Nat.add_descFactorial_eq_ascFactorial
 
 /-- `n.descFactorial k = n! / (n - k)!` but without ℕ-division. See `Nat.descFactorial_eq_div`

From 4753ef03dfa394d2dfe6c85bd881b96f4c4a529f Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Sun, 22 Oct 2023 06:29:11 +0900
Subject: [PATCH 02/12] Update Basic.lean

fix theorems that use changed ascFactorial.
---
 Mathlib/Data/Nat/Choose/Basic.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Nat/Choose/Basic.lean b/Mathlib/Data/Nat/Choose/Basic.lean
index 5adc92bb73d49..4909aa805e280 100644
--- a/Mathlib/Data/Nat/Choose/Basic.lean
+++ b/Mathlib/Data/Nat/Choose/Basic.lean
@@ -233,20 +233,20 @@ theorem choose_mul_succ_eq (n k : ℕ) : n.choose k * (n + 1) = (n + 1).choose k
 #align nat.choose_mul_succ_eq Nat.choose_mul_succ_eq
 
 theorem ascFactorial_eq_factorial_mul_choose (n k : ℕ) :
-    n.ascFactorial k = k ! * (n + k).choose k := by
+    (n + 1).ascFactorial k = k ! * (n + k).choose k := by
   rw [mul_comm]
   apply mul_right_cancel₀ (factorial_ne_zero (n + k - k))
-  rw [choose_mul_factorial_mul_factorial, add_tsub_cancel_right, ← factorial_mul_ascFactorial,
-    mul_comm]
-  exact Nat.le_add_left k n
+  rw [choose_mul_factorial_mul_factorial (le_add_left k n), add_tsub_cancel_right,
+    ← add_tsub_cancel_right (n + k) 1, add_right_comm, ← factorial_mul_ascFactorial (n + 1)
+    (choose_eq_zero_iff.mp rfl), mul_comm, add_tsub_cancel_right]
 #align nat.asc_factorial_eq_factorial_mul_choose Nat.ascFactorial_eq_factorial_mul_choose
 
-theorem factorial_dvd_ascFactorial (n k : ℕ) : k ! ∣ n.ascFactorial k :=
+theorem factorial_dvd_ascFactorial (n k : ℕ) : k ! ∣ (n + 1).ascFactorial k :=
   ⟨(n + k).choose k, ascFactorial_eq_factorial_mul_choose _ _⟩
 #align nat.factorial_dvd_asc_factorial Nat.factorial_dvd_ascFactorial
 
 theorem choose_eq_asc_factorial_div_factorial (n k : ℕ) :
-    (n + k).choose k = n.ascFactorial k / k ! := by
+    (n + k).choose k = (n + 1).ascFactorial k / k ! := by
   apply mul_left_cancel₀ (factorial_ne_zero k)
   rw [← ascFactorial_eq_factorial_mul_choose]
   exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm

From 4d9dcd2e622f4568a525bb1b0c507d5bb2a6d9b0 Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Sun, 22 Oct 2023 11:58:39 +0900
Subject: [PATCH 03/12] adapt shift in ascFactorial def

fix some proofs and statements to work with shifted ascFactorial definition.
---
 .../Combinatorics/Derangements/Finite.lean    |  6 ++--
 Mathlib/Data/Nat/Choose/Basic.lean            | 31 +++++++++++++------
 Mathlib/Data/Nat/Factorial/Basic.lean         |  7 ++++-
 Mathlib/RingTheory/Polynomial/Pochhammer.lean | 26 ++++++----------
 4 files changed, 40 insertions(+), 30 deletions(-)

diff --git a/Mathlib/Combinatorics/Derangements/Finite.lean b/Mathlib/Combinatorics/Derangements/Finite.lean
index eab83e05742e8..2fc41bf002693 100644
--- a/Mathlib/Combinatorics/Derangements/Finite.lean
+++ b/Mathlib/Combinatorics/Derangements/Finite.lean
@@ -115,7 +115,7 @@ theorem card_derangements_eq_numDerangements (α : Type*) [Fintype α] [Decidabl
 
 theorem numDerangements_sum (n : ℕ) :
     (numDerangements n : ℤ) =
-      ∑ k in Finset.range (n + 1), (-1 : ℤ) ^ k * Nat.ascFactorial k (n - k) := by
+      ∑ k in Finset.range (n + 1), (-1 : ℤ) ^ k * Nat.ascFactorial (k + 1) (n - k) := by
   induction' n with n hn; · rfl
   rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
     Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ, neg_one_mul, sub_eq_add_neg,
@@ -123,6 +123,6 @@ theorem numDerangements_sum (n : ℕ) :
   -- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x)
   intro x hx
   have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
-  rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_tsub_cancel_of_le h_le, Int.ofNat_mul,
-    Int.ofNat_succ, mul_left_comm]
+  rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
+    Int.ofNat_mul, Int.ofNat_succ, mul_left_comm]
 #align num_derangements_sum numDerangements_sum
diff --git a/Mathlib/Data/Nat/Choose/Basic.lean b/Mathlib/Data/Nat/Choose/Basic.lean
index 4909aa805e280..7421289f06a94 100644
--- a/Mathlib/Data/Nat/Choose/Basic.lean
+++ b/Mathlib/Data/Nat/Choose/Basic.lean
@@ -232,21 +232,32 @@ theorem choose_mul_succ_eq (n k : ℕ) : n.choose k * (n + 1) = (n + 1).choose k
         zero_mul]
 #align nat.choose_mul_succ_eq Nat.choose_mul_succ_eq
 
-theorem ascFactorial_eq_factorial_mul_choose (n k : ℕ) :
-    (n + 1).ascFactorial k = k ! * (n + k).choose k := by
-  rw [mul_comm]
-  apply mul_right_cancel₀ (factorial_ne_zero (n + k - k))
-  rw [choose_mul_factorial_mul_factorial (le_add_left k n), add_tsub_cancel_right,
-    ← add_tsub_cancel_right (n + k) 1, add_right_comm, ← factorial_mul_ascFactorial (n + 1)
-    (choose_eq_zero_iff.mp rfl), mul_comm, add_tsub_cancel_right]
+theorem ascFactorial_eq_factorial_mul_choose (n : ℕ) : ∀ (k : ℕ),
+    n.ascFactorial k = k ! * (n + k - 1).choose k
+  | 0 => by
+    rw [ascFactorial_zero, choose_zero_right, factorial_zero, mul_one]
+  | (k+1) => by
+    cases n with
+    | zero =>
+      rw [zero_ascFactorial]
+      simp only [zero_eq, zero_add, ge_iff_le, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
+        add_tsub_cancel_right, choose_succ_self, mul_zero]
+    | succ n =>
+      apply mul_right_cancel₀ (factorial_ne_zero (n + 1 - 1))
+      rw [mul_comm _ (n + 1 - 1).factorial, factorial_mul_ascFactorial (n+1)
+        (lt_succ.mpr (zero_le n)), add_succ_sub_one, add_succ_sub_one, add_zero,
+        Nat.add_right_comm n 1 k, mul_comm (k+1).factorial]
+      nth_rw 3 [← Nat.add_sub_cancel n (k+1)]
+      have h : k + 1 ≤ n + k + 1 := le_add_left (k + 1) n
+      rw [← add_assoc, choose_mul_factorial_mul_factorial h]
 #align nat.asc_factorial_eq_factorial_mul_choose Nat.ascFactorial_eq_factorial_mul_choose
 
-theorem factorial_dvd_ascFactorial (n k : ℕ) : k ! ∣ (n + 1).ascFactorial k :=
-  ⟨(n + k).choose k, ascFactorial_eq_factorial_mul_choose _ _⟩
+theorem factorial_dvd_ascFactorial (n k : ℕ) : k ! ∣ n.ascFactorial k :=
+  ⟨(n + k - 1).choose k, ascFactorial_eq_factorial_mul_choose _ _⟩
 #align nat.factorial_dvd_asc_factorial Nat.factorial_dvd_ascFactorial
 
 theorem choose_eq_asc_factorial_div_factorial (n k : ℕ) :
-    (n + k).choose k = (n + 1).ascFactorial k / k ! := by
+    (n + k - 1).choose k = n.ascFactorial k / k ! := by
   apply mul_left_cancel₀ (factorial_ne_zero k)
   rw [← ascFactorial_eq_factorial_mul_choose]
   exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm
diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index 3b4a22e2eb703..5a62a85bebf7c 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -243,13 +243,18 @@ theorem ascFactorial_succ {n k : ℕ} : n.ascFactorial k.succ = (n + k) * n.ascF
   rfl
 #align nat.asc_factorial_succ Nat.ascFactorial_succ
 
-@[simp]
 theorem zero_ascFactorial : ∀ (k : ℕ), (0 : ℕ).ascFactorial k.succ = 0
   | 0 => by
     simp only
   | (k+1) => by
     rw [ascFactorial_succ, zero_ascFactorial k, mul_zero]
 
+@[simp]
+theorem one_ascFactorial : ∀ (k : ℕ), (1 : ℕ).ascFactorial k = k.factorial
+  | 0 => ascFactorial_zero 1
+  | (k+1) => by
+    rw [ascFactorial_succ, one_ascFactorial k, add_comm, factorial_succ]
+
 theorem succ_ascFactorial (n : ℕ) :
     ∀ k, n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
   | 0 => by rw [add_zero, ascFactorial_zero, ascFactorial_zero]
diff --git a/Mathlib/RingTheory/Polynomial/Pochhammer.lean b/Mathlib/RingTheory/Polynomial/Pochhammer.lean
index f81166c85ba97..88b0def1c5e29 100644
--- a/Mathlib/RingTheory/Polynomial/Pochhammer.lean
+++ b/Mathlib/RingTheory/Polynomial/Pochhammer.lean
@@ -151,24 +151,16 @@ theorem ascPochhammer_mul (n m : ℕ) :
 #align pochhammer_mul ascPochhammer_mul
 
 theorem ascPochhammer_nat_eq_ascFactorial (n : ℕ) :
-    ∀ k, (ascPochhammer ℕ k).eval (n + 1) = n.ascFactorial k
+    ∀ k, (ascPochhammer ℕ k).eval n = n.ascFactorial k
   | 0 => by rw [ascPochhammer_zero, eval_one, Nat.ascFactorial_zero]
   | t + 1 => by
-    rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t]
-    simp only [eval_add, eval_X, eval_nat_cast, Nat.cast_id]
-    rw [Nat.ascFactorial_succ, add_right_comm, mul_comm]
+    rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
+      eval_nat_cast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
 #align pochhammer_nat_eq_asc_factorial ascPochhammer_nat_eq_ascFactorial
 
 theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) :
     (ascPochhammer ℕ b).eval a = (a + b - 1).descFactorial b := by
-  cases' b with b
-  · rw [Nat.descFactorial_zero, ascPochhammer_zero, Polynomial.eval_one]
-  rw [Nat.add_succ, Nat.succ_sub_succ, tsub_zero]
-  cases a
-  · simp only [Nat.zero_eq, ne_eq, Nat.succ_ne_zero, not_false_iff, ascPochhammer_ne_zero_eval_zero,
-    zero_add, Nat.descFactorial_succ, le_refl, tsub_eq_zero_of_le, zero_mul]
-  · rw [Nat.succ_add, ← Nat.add_succ, Nat.add_descFactorial_eq_ascFactorial,
-      ascPochhammer_nat_eq_ascFactorial]
+  rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial]
 #align pochhammer_nat_eq_desc_factorial ascPochhammer_nat_eq_descFactorial
 
 @[simp]
@@ -209,12 +201,14 @@ variable (S : Type*) [Semiring S] (r n : ℕ)
 @[simp]
 theorem ascPochhammer_eval_one (S : Type*) [Semiring S] (n : ℕ) :
     (ascPochhammer S n).eval (1 : S) = (n ! : S) := by
-  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.zero_ascFactorial]
+  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.one_ascFactorial]
 #align pochhammer_eval_one ascPochhammer_eval_one
 
 theorem factorial_mul_ascPochhammer (S : Type*) [Semiring S] (r n : ℕ) :
     (r ! : S) * (ascPochhammer S n).eval (r + 1 : S) = (r + n)! := by
-  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
+  nth_rw 1 [← Nat.add_sub_cancel r 1]
+  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial, succ_add_sub_one]
+  exact succ_pos r
 #align factorial_mul_pochhammer factorial_mul_ascPochhammer
 
 theorem ascPochhammer_nat_eval_succ (r : ℕ) :
@@ -360,8 +354,8 @@ theorem descPochhammer_int_eq_descFactorial (n : ℕ) :
       exact (Int.ofNat_sub <| not_lt.mp h).symm
 
 theorem descPochhammer_int_eq_ascFactorial (a b : ℕ) :
-    (descPochhammer ℤ b).eval (a + b : ℤ) = a.ascFactorial b := by
-  rw [← Nat.cast_add, descPochhammer_int_eq_descFactorial (a + b) b,
+    (descPochhammer ℤ b).eval (a + b : ℤ) = (a + 1).ascFactorial b := by
+  rw [← Nat.cast_add, descPochhammer_int_eq_descFactorial (a + b) b, ← Nat.succ_add_sub_one a b,
       Nat.add_descFactorial_eq_ascFactorial]
 
 end Ring

From f6d0bc4470b3ccb464b64b760081f5213e25c6fe Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Mon, 23 Oct 2023 00:57:25 +0900
Subject: [PATCH 04/12] Update Cast.lean

fix some proofs and statements to work with shifted ascFactorial definition.
---
 Mathlib/Data/Nat/Factorial/Cast.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Nat/Factorial/Cast.lean b/Mathlib/Data/Nat/Factorial/Cast.lean
index fb7730b8dcf50..e594e50c5c7b3 100644
--- a/Mathlib/Data/Nat/Factorial/Cast.lean
+++ b/Mathlib/Data/Nat/Factorial/Cast.lean
@@ -31,8 +31,8 @@ section Semiring
 variable [Semiring S] (a b : ℕ)
 
 -- Porting note: added type ascription around a + 1
-theorem cast_ascFactorial : (a.ascFactorial b : S) = (ascPochhammer S b).eval (a + 1 : S) := by
-  rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast, Nat.cast_add, Nat.cast_one]
+theorem cast_ascFactorial : (a.ascFactorial b : S) = (ascPochhammer S b).eval (a : S) := by
+  rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast]
 #align nat.cast_asc_factorial Nat.cast_ascFactorial
 
 -- Porting note: added type ascription around a - (b - 1)
@@ -49,7 +49,7 @@ theorem cast_descFactorial :
 #align nat.cast_desc_factorial Nat.cast_descFactorial
 
 theorem cast_factorial : (a ! : S) = (ascPochhammer S a).eval 1 := by
-  rw [← zero_ascFactorial, cast_ascFactorial, cast_zero, zero_add]
+  rw [← one_ascFactorial, cast_ascFactorial, cast_one]
 #align nat.cast_factorial Nat.cast_factorial
 
 end Semiring

From 45346f2cac1acb09dcbb11cad5b2a198f2febc16 Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Mon, 23 Oct 2023 01:50:02 +0900
Subject: [PATCH 05/12] Update Exponential.lean

fix some proofs and statements to work with shifted ascFactorial definition.
---
 Mathlib/Combinatorics/Derangements/Exponential.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/Derangements/Exponential.lean b/Mathlib/Combinatorics/Derangements/Exponential.lean
index 4a071739713bb..b588748ade9da 100644
--- a/Mathlib/Combinatorics/Derangements/Exponential.lean
+++ b/Mathlib/Combinatorics/Derangements/Exponential.lean
@@ -48,7 +48,8 @@ theorem numDerangements_tendsto_inv_e :
   refine' Finset.sum_congr (refl _) _
   intro k hk
   have h_le : k ≤ n := Finset.mem_range_succ_iff.mp hk
-  rw [Nat.ascFactorial_eq_div, add_tsub_cancel_of_le h_le]
+  rw [Nat.ascFactorial_eq_div (k+1) (n-k) (Nat.succ_pos k), add_right_comm,
+    add_tsub_cancel_of_le h_le, add_tsub_cancel_right k, add_tsub_cancel_right n]
   push_cast [Nat.factorial_dvd_factorial h_le]
   field_simp [Nat.factorial_ne_zero]
   ring

From 82c46c5c077263682da05674f25b03ff35da901c Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Thu, 9 Nov 2023 18:20:06 +0900
Subject: [PATCH 06/12] Restore thms with no Nat sub

New versions with Nat sub get dashes.
---
 .../Derangements/Exponential.lean             |  3 +-
 Mathlib/Data/Nat/Choose/Basic.lean            | 44 +++++++++---------
 Mathlib/Data/Nat/Factorial/Basic.lean         | 45 ++++++++++++++-----
 Mathlib/RingTheory/Polynomial/Pochhammer.lean | 10 ++---
 4 files changed, 62 insertions(+), 40 deletions(-)

diff --git a/Mathlib/Combinatorics/Derangements/Exponential.lean b/Mathlib/Combinatorics/Derangements/Exponential.lean
index b588748ade9da..4a071739713bb 100644
--- a/Mathlib/Combinatorics/Derangements/Exponential.lean
+++ b/Mathlib/Combinatorics/Derangements/Exponential.lean
@@ -48,8 +48,7 @@ theorem numDerangements_tendsto_inv_e :
   refine' Finset.sum_congr (refl _) _
   intro k hk
   have h_le : k ≤ n := Finset.mem_range_succ_iff.mp hk
-  rw [Nat.ascFactorial_eq_div (k+1) (n-k) (Nat.succ_pos k), add_right_comm,
-    add_tsub_cancel_of_le h_le, add_tsub_cancel_right k, add_tsub_cancel_right n]
+  rw [Nat.ascFactorial_eq_div, add_tsub_cancel_of_le h_le]
   push_cast [Nat.factorial_dvd_factorial h_le]
   field_simp [Nat.factorial_ne_zero]
   ring
diff --git a/Mathlib/Data/Nat/Choose/Basic.lean b/Mathlib/Data/Nat/Choose/Basic.lean
index 7421289f06a94..580150d44da31 100644
--- a/Mathlib/Data/Nat/Choose/Basic.lean
+++ b/Mathlib/Data/Nat/Choose/Basic.lean
@@ -232,37 +232,41 @@ theorem choose_mul_succ_eq (n k : ℕ) : n.choose k * (n + 1) = (n + 1).choose k
         zero_mul]
 #align nat.choose_mul_succ_eq Nat.choose_mul_succ_eq
 
-theorem ascFactorial_eq_factorial_mul_choose (n : ℕ) : ∀ (k : ℕ),
-    n.ascFactorial k = k ! * (n + k - 1).choose k
-  | 0 => by
-    rw [ascFactorial_zero, choose_zero_right, factorial_zero, mul_one]
-  | (k+1) => by
-    cases n with
-    | zero =>
-      rw [zero_ascFactorial]
-      simp only [zero_eq, zero_add, ge_iff_le, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
-        add_tsub_cancel_right, choose_succ_self, mul_zero]
-    | succ n =>
-      apply mul_right_cancel₀ (factorial_ne_zero (n + 1 - 1))
-      rw [mul_comm _ (n + 1 - 1).factorial, factorial_mul_ascFactorial (n+1)
-        (lt_succ.mpr (zero_le n)), add_succ_sub_one, add_succ_sub_one, add_zero,
-        Nat.add_right_comm n 1 k, mul_comm (k+1).factorial]
-      nth_rw 3 [← Nat.add_sub_cancel n (k+1)]
-      have h : k + 1 ≤ n + k + 1 := le_add_left (k + 1) n
-      rw [← add_assoc, choose_mul_factorial_mul_factorial h]
+theorem ascFactorial_eq_factorial_mul_choose (n k : ℕ) :
+    (n + 1).ascFactorial k = k ! * (n + k).choose k := by
+  rw [mul_comm]
+  apply mul_right_cancel₀ (factorial_ne_zero (n + k - k))
+  rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, add_tsub_cancel_right,
+    ← factorial_mul_ascFactorial, mul_comm]
 #align nat.asc_factorial_eq_factorial_mul_choose Nat.ascFactorial_eq_factorial_mul_choose
 
+theorem ascFactorial_eq_factorial_mul_choose' (n k : ℕ) :
+    n.ascFactorial k = k ! * (n + k - 1).choose k := by
+  cases hn : n
+  cases hk : k
+  rw [ascFactorial_zero, choose_zero_right, factorial_zero, mul_one]
+  simp only [zero_ascFactorial, zero_eq, zero_add, ge_iff_le, succ_sub_succ_eq_sub, nonpos_iff_eq_zero, tsub_zero,
+    choose_succ_self, mul_zero]
+  rw [ascFactorial_eq_factorial_mul_choose]
+  simp only [ge_iff_le, succ_add_sub_one]
+
 theorem factorial_dvd_ascFactorial (n k : ℕ) : k ! ∣ n.ascFactorial k :=
-  ⟨(n + k - 1).choose k, ascFactorial_eq_factorial_mul_choose _ _⟩
+  ⟨(n + k - 1).choose k, ascFactorial_eq_factorial_mul_choose' _ _⟩
 #align nat.factorial_dvd_asc_factorial Nat.factorial_dvd_ascFactorial
 
 theorem choose_eq_asc_factorial_div_factorial (n k : ℕ) :
-    (n + k - 1).choose k = n.ascFactorial k / k ! := by
+    (n + k).choose k = (n + 1).ascFactorial k / k ! := by
   apply mul_left_cancel₀ (factorial_ne_zero k)
   rw [← ascFactorial_eq_factorial_mul_choose]
   exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm
 #align nat.choose_eq_asc_factorial_div_factorial Nat.choose_eq_asc_factorial_div_factorial
 
+theorem choose_eq_asc_factorial_div_factorial' (n k : ℕ) :
+    (n + k - 1).choose k = n.ascFactorial k / k ! := by
+  apply mul_left_cancel₀ (factorial_ne_zero k)
+  rw [← ascFactorial_eq_factorial_mul_choose']
+  exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm
+
 theorem descFactorial_eq_factorial_mul_choose (n k : ℕ) : n.descFactorial k = k ! * n.choose k := by
   obtain h | h := Nat.lt_or_ge n k
   · rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, mul_zero]
diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index 5a62a85bebf7c..ce5f39c4297a9 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -263,21 +263,36 @@ theorem succ_ascFactorial (n : ℕ) :
       succ_add, ← add_assoc, succ_eq_add_one]
 #align nat.succ_asc_factorial Nat.succ_ascFactorial
 
-/-- `n.ascFactorial k = (n + k - 1)! / (n - 1)!` for `n > 0` but without ℕ-division. See
+/-- `(n + 1).ascFactorial k = (n + k) ! / n !` but without ℕ-division. See
 `Nat.ascFactorial_eq_div` for the version with ℕ-division. -/
-theorem factorial_mul_ascFactorial (n : ℕ) (h : 0 < n) :
-    ∀ k, (n - 1) ! * n.ascFactorial k = (n + k - 1)!
-  | 0 => by rw [ascFactorial, add_zero, mul_one]
-  | k + 1 => by
-    rw [ascFactorial_succ, mul_left_comm, factorial_mul_ascFactorial n h k, ← add_assoc]
-    exact mul_factorial_pred (add_pos_left h k)
+theorem factorial_mul_ascFactorial (n : ℕ) : ∀ k, n ! * (n + 1).ascFactorial k = (n + k)!
+| 0 => by
+  rw [add_zero, ascFactorial_zero, mul_one]
+| k + 1 => by
+  rw [ascFactorial_succ, ← add_assoc, factorial_succ, mul_comm (n + 1 + k), ← mul_assoc,
+    factorial_mul_ascFactorial n k, mul_comm, add_right_comm]
 #align nat.factorial_mul_asc_factorial Nat.factorial_mul_ascFactorial
 
+/-- `n.ascFactorial k = (n + k - 1)! / (n - 1)!` for `n > 0` but without ℕ-division. See
+`Nat.ascFactorial_eq_div` for the version with ℕ-division. Consider using
+`factorial_mul_ascFactorial` to avoid complications of ℕ-subtraction. -/
+theorem factorial_mul_ascFactorial' (n k : ℕ) (h : 0 < n) :
+    (n - 1) ! * n.ascFactorial k = (n + k - 1)! := by
+  rw [Nat.sub_add_comm h, Nat.sub_one]--ascFactorial_succ, mul_left_comm, factorial_mul_ascFactorial' n h k, ← add_assoc]
+  nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]
+  rw [Nat.sub_one, factorial_mul_ascFactorial]
+
 /-- Avoid in favor of `Nat.factorial_mul_ascFactorial` if you can. ℕ-division isn't worth it. -/
-theorem ascFactorial_eq_div (n k : ℕ) (h : 0 < n) :
+theorem ascFactorial_eq_div (n k : ℕ) :  (n + 1).ascFactorial k = (n + k)! / n ! := by
+  apply mul_left_cancel₀ n.factorial_ne_zero
+  rw [factorial_mul_ascFactorial]
+  refine (Nat.mul_div_cancel_left' <| factorial_dvd_factorial <| le_add_right n k).symm
+
+/-- Avoid in favor of `Nat.factorial_mul_ascFactorial` if you can. -/
+theorem ascFactorial_eq_div' (n k : ℕ) (h : 0 < n) :
     n.ascFactorial k = (n + k - 1)! / (n - 1) ! := by
   apply mul_left_cancel₀ (n-1).factorial_ne_zero
-  rw [factorial_mul_ascFactorial _ h]
+  rw [factorial_mul_ascFactorial' _ _ h]
   exact (Nat.mul_div_cancel_left' <| factorial_dvd_factorial <| Nat.sub_le_sub_right
     (le_add_right n k) 1).symm
 #align nat.asc_factorial_eq_div Nat.ascFactorial_eq_div
@@ -404,14 +419,20 @@ theorem descFactorial_eq_zero_iff_lt {n : ℕ} : ∀ {k : ℕ}, n.descFactorial
 alias ⟨_, descFactorial_of_lt⟩ := descFactorial_eq_zero_iff_lt
 #align nat.desc_factorial_of_lt Nat.descFactorial_of_lt
 
-theorem add_descFactorial_eq_ascFactorial (n : ℕ) :
+theorem add_descFactorial_eq_ascFactorial (n : ℕ) : ∀ k : ℕ, (n + k).descFactorial k = (n + 1).ascFactorial k
+  | 0 => by rw [ascFactorial_zero, descFactorial_zero]
+  | succ k => by
+    rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
+      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]
+#align nat.add_desc_factorial_eq_asc_factorial Nat.add_descFactorial_eq_ascFactorial
+
+theorem add_descFactorial_eq_ascFactorial' (n : ℕ) :
     ∀ k : ℕ, (n + k - 1).descFactorial k = n.ascFactorial k
   | 0 => by rw [ascFactorial_zero, descFactorial_zero]
   | succ k => by
     rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_succ_add,
-      add_descFactorial_eq_ascFactorial _ k, ← succ_ascFactorial, succ_add_sub_one,
+      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
       Nat.add_sub_cancel]
-#align nat.add_desc_factorial_eq_asc_factorial Nat.add_descFactorial_eq_ascFactorial
 
 /-- `n.descFactorial k = n! / (n - k)!` but without ℕ-division. See `Nat.descFactorial_eq_div`
 for the version using ℕ-division. -/
diff --git a/Mathlib/RingTheory/Polynomial/Pochhammer.lean b/Mathlib/RingTheory/Polynomial/Pochhammer.lean
index 374d72c685e5d..8dddffabd96c9 100644
--- a/Mathlib/RingTheory/Polynomial/Pochhammer.lean
+++ b/Mathlib/RingTheory/Polynomial/Pochhammer.lean
@@ -160,7 +160,7 @@ theorem ascPochhammer_nat_eq_ascFactorial (n : ℕ) :
 
 theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) :
     (ascPochhammer ℕ b).eval a = (a + b - 1).descFactorial b := by
-  rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial]
+  rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']
 #align pochhammer_nat_eq_desc_factorial ascPochhammer_nat_eq_descFactorial
 
 @[simp]
@@ -206,9 +206,7 @@ theorem ascPochhammer_eval_one (S : Type*) [Semiring S] (n : ℕ) :
 
 theorem factorial_mul_ascPochhammer (S : Type*) [Semiring S] (r n : ℕ) :
     (r ! : S) * (ascPochhammer S n).eval (r + 1 : S) = (r + n)! := by
-  nth_rw 1 [← Nat.add_sub_cancel r 1]
-  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial, succ_add_sub_one]
-  exact succ_pos r
+  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
 #align factorial_mul_pochhammer factorial_mul_ascPochhammer
 
 theorem ascPochhammer_nat_eval_succ (r : ℕ) :
@@ -355,7 +353,7 @@ theorem descPochhammer_int_eq_descFactorial (n : ℕ) :
 
 theorem descPochhammer_int_eq_ascFactorial (a b : ℕ) :
     (descPochhammer ℤ b).eval (a + b : ℤ) = (a + 1).ascFactorial b := by
-  rw [← Nat.cast_add, descPochhammer_int_eq_descFactorial (a + b) b, ← Nat.succ_add_sub_one a b,
-      Nat.add_descFactorial_eq_ascFactorial]
+  rw [← Nat.cast_add, descPochhammer_int_eq_descFactorial (a + b) b,
+    Nat.add_descFactorial_eq_ascFactorial]
 
 end Ring

From 698619935e14fdde04e317d93e0a6c79a0b58ecb Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Thu, 9 Nov 2023 18:25:01 +0900
Subject: [PATCH 07/12] indentation

also, rm commented rw
---
 Mathlib/Data/Nat/Factorial/Basic.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index ce5f39c4297a9..52d41f6118771 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -266,11 +266,11 @@ theorem succ_ascFactorial (n : ℕ) :
 /-- `(n + 1).ascFactorial k = (n + k) ! / n !` but without ℕ-division. See
 `Nat.ascFactorial_eq_div` for the version with ℕ-division. -/
 theorem factorial_mul_ascFactorial (n : ℕ) : ∀ k, n ! * (n + 1).ascFactorial k = (n + k)!
-| 0 => by
-  rw [add_zero, ascFactorial_zero, mul_one]
-| k + 1 => by
-  rw [ascFactorial_succ, ← add_assoc, factorial_succ, mul_comm (n + 1 + k), ← mul_assoc,
-    factorial_mul_ascFactorial n k, mul_comm, add_right_comm]
+  | 0 => by
+    rw [add_zero, ascFactorial_zero, mul_one]
+  | k + 1 => by
+    rw [ascFactorial_succ, ← add_assoc, factorial_succ, mul_comm (n + 1 + k), ← mul_assoc,
+      factorial_mul_ascFactorial n k, mul_comm, add_right_comm]
 #align nat.factorial_mul_asc_factorial Nat.factorial_mul_ascFactorial
 
 /-- `n.ascFactorial k = (n + k - 1)! / (n - 1)!` for `n > 0` but without ℕ-division. See
@@ -278,7 +278,7 @@ theorem factorial_mul_ascFactorial (n : ℕ) : ∀ k, n ! * (n + 1).ascFactorial
 `factorial_mul_ascFactorial` to avoid complications of ℕ-subtraction. -/
 theorem factorial_mul_ascFactorial' (n k : ℕ) (h : 0 < n) :
     (n - 1) ! * n.ascFactorial k = (n + k - 1)! := by
-  rw [Nat.sub_add_comm h, Nat.sub_one]--ascFactorial_succ, mul_left_comm, factorial_mul_ascFactorial' n h k, ← add_assoc]
+  rw [Nat.sub_add_comm h, Nat.sub_one]
   nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]
   rw [Nat.sub_one, factorial_mul_ascFactorial]
 

From 4d388eb6d75b3f1487a6768ffc0eb5df451bb4eb Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Thu, 9 Nov 2023 18:27:04 +0900
Subject: [PATCH 08/12] line length

---
 Mathlib/Data/Nat/Choose/Basic.lean    | 4 ++--
 Mathlib/Data/Nat/Factorial/Basic.lean | 3 ++-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Nat/Choose/Basic.lean b/Mathlib/Data/Nat/Choose/Basic.lean
index 580150d44da31..ccf5997aae1de 100644
--- a/Mathlib/Data/Nat/Choose/Basic.lean
+++ b/Mathlib/Data/Nat/Choose/Basic.lean
@@ -245,8 +245,8 @@ theorem ascFactorial_eq_factorial_mul_choose' (n k : ℕ) :
   cases hn : n
   cases hk : k
   rw [ascFactorial_zero, choose_zero_right, factorial_zero, mul_one]
-  simp only [zero_ascFactorial, zero_eq, zero_add, ge_iff_le, succ_sub_succ_eq_sub, nonpos_iff_eq_zero, tsub_zero,
-    choose_succ_self, mul_zero]
+  simp only [zero_ascFactorial, zero_eq, zero_add, ge_iff_le, succ_sub_succ_eq_sub,
+    nonpos_iff_eq_zero, tsub_zero, choose_succ_self, mul_zero]
   rw [ascFactorial_eq_factorial_mul_choose]
   simp only [ge_iff_le, succ_add_sub_one]
 
diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index 52d41f6118771..164d4ea5b3946 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -419,7 +419,8 @@ theorem descFactorial_eq_zero_iff_lt {n : ℕ} : ∀ {k : ℕ}, n.descFactorial
 alias ⟨_, descFactorial_of_lt⟩ := descFactorial_eq_zero_iff_lt
 #align nat.desc_factorial_of_lt Nat.descFactorial_of_lt
 
-theorem add_descFactorial_eq_ascFactorial (n : ℕ) : ∀ k : ℕ, (n + k).descFactorial k = (n + 1).ascFactorial k
+theorem add_descFactorial_eq_ascFactorial (n : ℕ) : ∀ k : ℕ,
+    (n + k).descFactorial k = (n + 1).ascFactorial k
   | 0 => by rw [ascFactorial_zero, descFactorial_zero]
   | succ k => by
     rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,

From 4d63753a045643f04e1b8aca4a63309143a07cab Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Mon, 20 Nov 2023 22:37:25 +0900
Subject: [PATCH 09/12] rewrite failed simp

---
 Mathlib/Data/Nat/Factorial/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index 6d1a8aefd79f1..f716223b4f6b1 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -237,7 +237,7 @@ theorem ascFactorial_succ {n k : ℕ} : n.ascFactorial k.succ = (n + k) * n.ascF
 
 theorem zero_ascFactorial : ∀ (k : ℕ), (0 : ℕ).ascFactorial k.succ = 0
   | 0 => by
-    simp only
+    rw [ascFactorial_succ, ascFactorial_zero, zero_add, zero_mul]
   | (k+1) => by
     rw [ascFactorial_succ, zero_ascFactorial k, mul_zero]
 

From 44e17334228b0880b0bc5c25432ca223d3b4198f Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Mon, 20 Nov 2023 23:46:40 +0900
Subject: [PATCH 10/12] shift ascFactorial in positivity tactic and test

---
 Mathlib/Tactic/Positivity/Basic.lean | 2 +-
 test/positivity.lean                 | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Tactic/Positivity/Basic.lean b/Mathlib/Tactic/Positivity/Basic.lean
index 6840ce0ca5e46..bb6fe7b75f782 100644
--- a/Mathlib/Tactic/Positivity/Basic.lean
+++ b/Mathlib/Tactic/Positivity/Basic.lean
@@ -498,5 +498,5 @@ def evalFactorial : PositivityExt where eval {_ _} _ _ (e : Q(ℕ)) := do
 /-- Extension for Nat.ascFactorial. -/
 @[positivity Nat.ascFactorial _ _]
 def evalAscFactorial : PositivityExt where eval {_ _} _ _ (e : Q(ℕ)) := do
-  let ~q(Nat.ascFactorial $n $k) := e | throwError "failed to match Nat.ascFactorial"
+  let ~q(Nat.ascFactorial ($n + 1) $k) := e | throwError "failed to match Nat.ascFactorial"
   pure (.positive (q(Nat.ascFactorial_pos $n $k) : Expr))
diff --git a/test/positivity.lean b/test/positivity.lean
index 028cdba4cb6eb..0abf004b0eba0 100644
--- a/test/positivity.lean
+++ b/test/positivity.lean
@@ -253,7 +253,7 @@ example : 0 ≤ max (-3 : ℤ) 5 := by positivity
 
 example (n : ℕ) : 0 < n.succ := by positivity
 example (n : ℕ) : 0 < n ! := by positivity
-example (n k : ℕ) : 0 < n.ascFactorial k := by positivity
+example (n k : ℕ) : 0 < (n+1).ascFactorial k := by positivity
 
 -- example {α : Type _} (s : Finset α) (hs : s.Nonempty) : 0 < s.card := by positivity
 -- example {α : Type _} [Fintype α] [Nonempty α] : 0 < Fintype.card α := by positivity

From 7eb40ee4cd01225086c95db7ed74d4c45d922818 Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Mon, 25 Dec 2023 01:18:38 +0900
Subject: [PATCH 11/12] Resolve merge conflict

---
 Mathlib/Data/Nat/Factorial/Basic.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index f21a6e697e75b..fe74d0a2f4a6b 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -294,7 +294,7 @@ theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, n ^ k ≤ n.ascFactori
   | k + 1 => by
     rw [pow_succ, mul_comm, ascFactorial_succ, ← succ_ascFactorial]
     exact Nat.mul_le_mul (Nat.le_refl n)
-      ((pow_le_pow_of_le_left' (le_succ n) k).trans (pow_succ_le_ascFactorial n.succ k))
+      ((pow_le_pow_of_le_left (le_succ n) k).trans (pow_succ_le_ascFactorial n.succ k))
 #align nat.pow_succ_le_asc_factorial Nat.pow_succ_le_ascFactorial
 
 theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2) := by
@@ -321,9 +321,9 @@ theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1).a
   | 0 => by rintro ⟨⟩
   | 1 => by intro; contradiction
   | k + 2 => fun _ => by
-    rw [pow_succ, mul_comm, ascFactorial_succ, succ_add_eq_succ_add n (k + 1)]
+    rw [pow_succ, mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]
     exact Nat.mul_lt_mul' le_rfl ((ascFactorial_le_pow_add n _).trans_lt
-      (pow_lt_pow_of_lt_left (lt_add_one _) (succ_pos _))) (succ_pos _)
+      (pow_lt_pow_left (@lt_add_one ℕ _ _ _ _ _ _ _) (zero_le _) k.succ_ne_zero)) (succ_pos _)
 #align nat.asc_factorial_lt_pow_add Nat.ascFactorial_lt_pow_add
 
 theorem ascFactorial_pos (n k : ℕ) : 0 < (n + 1).ascFactorial k :=
@@ -403,7 +403,7 @@ theorem add_descFactorial_eq_ascFactorial' (n : ℕ) :
     ∀ k : ℕ, (n + k - 1).descFactorial k = n.ascFactorial k
   | 0 => by rw [ascFactorial_zero, descFactorial_zero]
   | succ k => by
-    rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_succ_add,
+    rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
       add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
       Nat.add_sub_cancel]
 

From f4105898e7ccbc24fbcce86cc99bae3011dc08ba Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Tue, 9 Jan 2024 08:46:37 +0100
Subject: [PATCH 12/12] Update Mathlib/Data/Nat/Factorial/Basic.lean

---
 Mathlib/Data/Nat/Factorial/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index 268f37d948ffa..499b7d5e1d273 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -281,7 +281,7 @@ theorem factorial_mul_ascFactorial' (n k : ℕ) (h : 0 < n) :
 theorem ascFactorial_eq_div (n k : ℕ) :  (n + 1).ascFactorial k = (n + k)! / n ! := by
   apply mul_left_cancel₀ n.factorial_ne_zero
   rw [factorial_mul_ascFactorial]
-  refine (Nat.mul_div_cancel_left' <| factorial_dvd_factorial <| le_add_right n k).symm
+  exact (Nat.mul_div_cancel_left' <| factorial_dvd_factorial <| le_add_right n k).symm
 
 /-- Avoid in favor of `Nat.factorial_mul_ascFactorial` if you can. -/
 theorem ascFactorial_eq_div' (n k : ℕ) (h : 0 < n) :