[Merged by Bors] - chore: shift Nat.ascFactorial down by one

Mathlib/Combinatorics/Derangements/Finite.lean

@@ -115,14 +115,14 @@ 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,
     add_left_inj, Finset.sum_congr rfl]
   -- 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

Mathlib/Data/Nat/Choose/Basic.lean

@@ -233,25 +233,40 @@ 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 <| 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).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).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]

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`.
 -/
 
 
@@ -222,100 +223,119 @@ 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]
 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 + 1) = (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
 
+theorem zero_ascFactorial : ∀ (k : ℕ), (0 : ℕ).ascFactorial k.succ = 0
+  | 0 => by
+    rw [ascFactorial_succ, ascFactorial_zero, zero_add, zero_mul]
+  | (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 + 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]
 #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. -/
-theorem factorial_mul_ascFactorial (n : ℕ) : ∀ k, n ! * n.ascFactorial k = (n + k)!
-  | 0 => by simp
+/-- `(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, mul_left_comm, factorial_mul_ascFactorial n k, ← add_assoc, factorial]
+    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]
+  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 : ℕ) : n.ascFactorial k = (n + k)! / n ! := by
+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]
-  exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| le.intro rfl).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) :
+    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 + 1)
-  suffices h' : n - k = t + 1 by rw [h', succ_ascFactorial, ascFactorial_succ]
-  rw [← tsub_tsub_assoc (succ_le_of_lt h) (succ_pos k), 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, mul_comm _ (succ (n + k))]
-    exact
-      Nat.mul_le_mul_of_nonneg_left
-        ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_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)]
-    exact mul_lt_mul_of_pos_left ((ascFactorial_le_pow_add n _).trans_lt <|
-      Nat.pow_lt_pow_left (lt_add_one _) k.succ_ne_zero) (succ_pos _)
+    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_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.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
@@ -379,13 +399,22 @@ 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.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,
-    add_descFactorial_eq_ascFactorial _ k]
+  | 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_add_succ,
+      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
+      Nat.add_sub_cancel]
+
 /-- `n.descFactorial k = n! / (n - k)!` but without ℕ-division. See `Nat.descFactorial_eq_div`
 for the version using ℕ-division. -/
 theorem factorial_mul_descFactorial : ∀ {n k : ℕ}, k ≤ n → (n - k)! * n.descFactorial k = n !

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

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,7 +201,7 @@ 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 : ℕ) :
@@ -360,8 +352,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
+    (descPochhammer ℤ b).eval (a + b : ℤ) = (a + 1).ascFactorial b := by
   rw [← Nat.cast_add, descPochhammer_int_eq_descFactorial (a + b) b,
-      Nat.add_descFactorial_eq_ascFactorial]
+    Nat.add_descFactorial_eq_ascFactorial]
 
 end Ring

Mathlib/Tactic/Positivity/Basic.lean

@@ -540,5 +540,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))

test/positivity.lean

@@ -254,7 +254,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