awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n m : ℕ
ih : ascPochhammer S n * comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + m)
succ :
  ascPochhammer S n *
      (ascPochhammer S m * HAdd.hAdd (α := S[X]) X (↑m : S[X])).comp (HAdd.hAdd (α := S[X]) X (↑n : S[X])) =
    ascPochhammer S (n + (m + 1))
succ₁ :
  ascPochhammer S n *
      (comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) *
        (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X]))) =
    ascPochhammer S (n + (m + 1))
succ₂ :
  ascPochhammer S n * comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) *
      (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) =
    ascPochhammer S (n + (m + 1))
succ₃ : ascPochhammer S (n + m) * (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) = ascPochhammer S (n + (m + 1))
succ₄ : ascPochhammer S (n + m) * (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) = ascPochhammer S (n + m + 1)
succ₅ :
  ascPochhammer S (n + m) * (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) =
    ascPochhammer S (n + m) * HAdd.hAdd (α := S[X]) X (↑(n + m) : S[X])
⊢ ascPochhammer S n * comp (ascPochhammer S (m + 1)) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) =
    ascPochhammer S (n + (m + 1))
have succ₆ : ascPochhammer S (n + m) * (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) =
  ascPochhammer S (n + m) * (X + HAdd.hAdd (α := S[X]) (↑n : S[X]) (↑m : S[X]))
Tactic: rw [ascPochhammer_succ_right, Polynomial.mul_X_add_natCast_comp, ← mul_assoc, ih,
      ← add_assoc, ascPochhammer_succ_right, Nat.cast_add, add_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n m : ℕ
ih : ascPochhammer S n * comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + m)
succ :
  ascPochhammer S n *
      (ascPochhammer S m * HAdd.hAdd (α := S[X]) X (↑m : S[X])).comp (HAdd.hAdd (α := S[X]) X (↑n : S[X])) =
    ascPochhammer S (n + (m + 1))
succ₁ :
  ascPochhammer S n *
      (comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) *
        (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X]))) =
    ascPochhammer S (n + (m + 1))
succ₂ :
  ascPochhammer S n * comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) *
      (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) =
    ascPochhammer S (n + (m + 1))
succ₃ : ascPochhammer S (n + m) * (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) = ascPochhammer S (n + (m + 1))
succ₄ : ascPochhammer S (n + m) * (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) = ascPochhammer S (n + m + 1)
succ₅ :
  ascPochhammer S (n + m) * (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) =
    ascPochhammer S (n + m) * HAdd.hAdd (α := S[X]) X (↑(n + m) : S[X])
succ₆ :
  ascPochhammer S (n + m) * (HAdd.hAdd (α := S[X]) X (↑n : S[X]) + (↑m : S[X])) =
    ascPochhammer S (n + m) * (X + HAdd.hAdd (α := S[X]) (↑n : S[X]) (↑m : S[X]))
⊢ ascPochhammer S n * comp (ascPochhammer S (m + 1)) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) =
    ascPochhammer S (n + (m + 1))
have succ₇ : ascPochhammer S (n + m) * (X + HAdd.hAdd (α := S[X]) (↑n : S[X]) (↑m : S[X])) =
  ascPochhammer S (n + m) * (X + HAdd.hAdd (α := S[X]) (↑n : S[X]) (↑m : S[X]))
Tactic: rw [ascPochhammer_succ_right, Polynomial.mul_X_add_natCast_comp, ← mul_assoc, ih,
      ← add_assoc, ascPochhammer_succ_right, Nat.cast_add, add_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n m : ℕ
⊢ ascPochhammer S n * comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + m)
have zero : ascPochhammer S n * comp (ascPochhammer S 0) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + 0)
Tactic: induction m with
  | zero => simp
  | succ m ih =>
    rw [ascPochhammer_succ_right, Polynomial.mul_X_add_natCast_comp, ← mul_assoc, ih,
      ← add_assoc, ascPochhammer_succ_right, Nat.cast_add, add_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n m : ℕ
zero : ascPochhammer S n * comp (ascPochhammer S 0) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + 0)
⊢ ascPochhammer S n * comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + m)
have succ : ∀ (m : ℕ)
  (ih : ascPochhammer S n * comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + m)),
  ascPochhammer S n * comp (ascPochhammer S (m + 1)) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) =
    ascPochhammer S (n + (m + 1))
Tactic: induction m with
  | zero => simp
  | succ m ih =>
    rw [ascPochhammer_succ_right, Polynomial.mul_X_add_natCast_comp, ← mul_assoc, ih,
      ← add_assoc, ascPochhammer_succ_right, Nat.cast_add, add_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
⊢ eval n (ascPochhammer ℕ 0) = n.ascFactorial 0
have rw : eval n 1 = n.ascFactorial 0
Tactic: rw [ascPochhammer_zero, eval_one, Nat.ascFactorial_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
rw : eval n 1 = n.ascFactorial 0
⊢ eval n (ascPochhammer ℕ 0) = n.ascFactorial 0
have rw₁ : 1 = n.ascFactorial 0
Tactic: rw [ascPochhammer_zero, eval_one, Nat.ascFactorial_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
rw : eval n 1 = n.ascFactorial 0
rw₁ : 1 = n.ascFactorial 0
⊢ eval n (ascPochhammer ℕ 0) = n.ascFactorial 0
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [ascPochhammer_zero, eval_one, Nat.ascFactorial_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n t : ℕ
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
have rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
Tactic: rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n t : ℕ
rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
have rw₁ : eval n (ascPochhammer ℕ t) * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
Tactic: rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n t : ℕ
rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₁ : eval n (ascPochhammer ℕ t) * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
have rw₂ : n.ascFactorial t * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
Tactic: rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n t : ℕ
rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₁ : eval n (ascPochhammer ℕ t) * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₂ : n.ascFactorial t * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
have rw₃ : n.ascFactorial t * (eval n X + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
Tactic: rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n t : ℕ
rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₁ : eval n (ascPochhammer ℕ t) * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₂ : n.ascFactorial t * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₃ : n.ascFactorial t * (eval n X + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
have rw₄ : n.ascFactorial t * (n + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
Tactic: rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n t : ℕ
rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₁ : eval n (ascPochhammer ℕ t) * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₂ : n.ascFactorial t * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₃ : n.ascFactorial t * (eval n X + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₄ : n.ascFactorial t * (n + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
have rw₅ : n.ascFactorial t * (n + (↑t : ℕ)) = n.ascFactorial (t + 1)
Tactic: rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n t : ℕ
rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₁ : eval n (ascPochhammer ℕ t) * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₂ : n.ascFactorial t * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₃ : n.ascFactorial t * (eval n X + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₄ : n.ascFactorial t * (n + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₅ : n.ascFactorial t * (n + (↑t : ℕ)) = n.ascFactorial (t + 1)
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
have rw₆ : n.ascFactorial t * (n + t) = n.ascFactorial (t + 1)
Tactic: rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n t : ℕ
rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₁ : eval n (ascPochhammer ℕ t) * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₂ : n.ascFactorial t * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₃ : n.ascFactorial t * (eval n X + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₄ : n.ascFactorial t * (n + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₅ : n.ascFactorial t * (n + (↑t : ℕ)) = n.ascFactorial (t + 1)
rw₆ : n.ascFactorial t * (n + t) = n.ascFactorial (t + 1)
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
have rw₇ : n.ascFactorial t * (n + t) = (n + t) * n.ascFactorial t
Tactic: rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n t : ℕ
rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₁ : eval n (ascPochhammer ℕ t) * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₂ : n.ascFactorial t * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₃ : n.ascFactorial t * (eval n X + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₄ : n.ascFactorial t * (n + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₅ : n.ascFactorial t * (n + (↑t : ℕ)) = n.ascFactorial (t + 1)
rw₆ : n.ascFactorial t * (n + t) = n.ascFactorial (t + 1)
rw₇ : n.ascFactorial t * (n + t) = (n + t) * n.ascFactorial t
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
have rw₈ : (n + t) * n.ascFactorial t = (n + t) * n.ascFactorial t
Tactic: rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n k : ℕ
⊢ eval (↑n : S) (ascPochhammer S k) = (↑(n.ascFactorial k) : S)
have norm_cast : Eq.{u_1 + 1} (α := S) (↑(eval n (ascPochhammer ℕ k)) : S) (↑(n.ascFactorial k) : S)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n k : ℕ
⊢ Eq.{u_1 + 1} (α := S) (↑(eval n (ascPochhammer ℕ k)) : S) (↑(n.ascFactorial k) : S)
have rw : Eq.{u_1 + 1} (α := S) (↑(n.ascFactorial k) : S) (↑(n.ascFactorial k) : S)
Tactic: rw [ascPochhammer_nat_eq_ascFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
a b : ℕ
⊢ eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b
have rw : a.ascFactorial b = (a + b - 1).descFactorial b
Tactic: rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
a b : ℕ
rw : a.ascFactorial b = (a + b - 1).descFactorial b
⊢ eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b
have rw₁ : a.ascFactorial b = a.ascFactorial b
Tactic: rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
⊢ eval (↑a : S) (ascPochhammer S b) = (↑((a + b - 1).descFactorial b) : S)
have norm_cast : Eq.{u_1 + 1} (α := S) (↑(eval a (ascPochhammer ℕ b)) : S) (↑((a + b - 1).descFactorial b) : S)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
⊢ Eq.{u_1 + 1} (α := S) (↑(eval a (ascPochhammer ℕ b)) : S) (↑((a + b - 1).descFactorial b) : S)
have rw : Eq.{u_1 + 1} (α := S) (↑((a + b - 1).descFactorial b) : S) (↑((a + b - 1).descFactorial b) : S)
Tactic: rw [ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
n : ℕ
hn : natDegree (ascPochhammer S n) = n
⊢ natDegree (ascPochhammer S (n + 1)) = n + 1
have this : (HAdd.hAdd (α := S[X]) X (↑n : S[X])).natDegree = 1
Tactic: have : natDegree (X + (n : S[X])) = 1 := natDegree_X_add_C (n : S)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
n : ℕ
hn : natDegree (ascPochhammer S n) = n
this : (HAdd.hAdd (α := S[X]) X (↑n : S[X])).natDegree = 1
⊢ natDegree (ascPochhammer S (n + 1)) = n + 1
have rw : Ne (α := S[X]) (ascPochhammer S n) 0
Tactic: rw [ascPochhammer_succ_right,
        natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
n : ℕ
hn : natDegree (ascPochhammer S n) = n
this : (HAdd.hAdd (α := S[X]) X (↑n : S[X])).natDegree = 1
⊢ Ne (α := S[X]) (ascPochhammer S n) 0
have zero : ∀ (hn : natDegree (ascPochhammer S 0) = 0) (this : (HAdd.hAdd (α := S[X]) X (↑0 : S[X])).natDegree = 1),
  Ne (α := S[X]) (ascPochhammer S 0) 0
Tactic: cases n
Cleared hypotheses: n, hn, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
n : ℕ
hn : natDegree (ascPochhammer S n) = n
this : (HAdd.hAdd (α := S[X]) X (↑n : S[X])).natDegree = 1
zero :
  ∀ (hn : natDegree (ascPochhammer S 0) = 0) (this : (HAdd.hAdd (α := S[X]) X (↑0 : S[X])).natDegree = 1),
    Ne (α := S[X]) (ascPochhammer S 0) 0
⊢ Ne (α := S[X]) (ascPochhammer S n) 0
have succ : ∀ (n : ℕ) (hn : natDegree (ascPochhammer S (n + 1)) = n + 1)
  (this : (HAdd.hAdd (α := S[X]) X (↑(n + 1) : S[X])).natDegree = 1), Ne (α := S[X]) (ascPochhammer S (n + 1)) 0
Tactic: cases n
Cleared hypotheses: n, hn, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
⊢ natDegree (ascPochhammer S n) = n
have zero : natDegree (ascPochhammer S 0) = 0
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have : natDegree (X + (n : S[X])) = 1 := natDegree_X_add_C (n : S)
    rw [ascPochhammer_succ_right,
        natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]
    cases n
    · simp
    · refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
zero : natDegree (ascPochhammer S 0) = 0
⊢ natDegree (ascPochhammer S n) = n
have succ : ∀ (n : ℕ) (hn : natDegree (ascPochhammer S n) = n), natDegree (ascPochhammer S (n + 1)) = n + 1
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have : natDegree (X + (n : S[X])) = 1 := natDegree_X_add_C (n : S)
    rw [ascPochhammer_succ_right,
        natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]
    cases n
    · simp
    · refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
h : 0 < s
⊢ 0 < eval s (ascPochhammer S 0)
have zero : LT.lt.{u_1} (α := S) 0 1
Tactic: simp only [ascPochhammer_zero, eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S (n + 1))
have succ : 0 < eval s (ascPochhammer S n) * (s + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_natCast_mul, eval_mul_X,
      Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : 0 < s
⊢ 0 < eval s (ascPochhammer S n)
have zero : 0 < eval s (ascPochhammer S 0)
Tactic: induction n with
  | zero =>
    simp only [ascPochhammer_zero, eval_one]
    exact zero_lt_one
  | succ n ih =>
    rw [ascPochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_natCast_mul, eval_mul_X,
      Nat.cast_comm, ← mul_add]
    exact mul_pos ih (lt_of_lt_of_le h (le_add_of_nonneg_right (Nat.cast_nonneg n)))
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : 0 < s
zero : 0 < eval s (ascPochhammer S 0)
⊢ 0 < eval s (ascPochhammer S n)
have succ : ∀ (n : ℕ) (ih : 0 < eval s (ascPochhammer S n)), 0 < eval s (ascPochhammer S (n + 1))
Tactic: induction n with
  | zero =>
    simp only [ascPochhammer_zero, eval_one]
    exact zero_lt_one
  | succ n ih =>
    rw [ascPochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_natCast_mul, eval_mul_X,
      Nat.cast_comm, ← mul_add]
    exact mul_pos ih (lt_of_lt_of_le h (le_add_of_nonneg_right (Nat.cast_nonneg n)))
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_2
inst : Semiring S
n : ℕ
⊢ eval 1 (ascPochhammer S n) = (↑n ! : S)
have rw_mod_cast : Eq.{u_2 + 1} (α := S) (↑(eval 1 (ascPochhammer ℕ n)) : S) (↑n ! : S)
Tactic: rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.one_ascFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_2
inst : Semiring S
n : ℕ
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  Eq.{u_2 + 1} (α := S) (↑(eval 1 (ascPochhammer ℕ n)) : S) (↑n ! : S)
⊢ eval 1 (ascPochhammer S n) = (↑n ! : S)
have rw_mod_cast₆ : Eq.{u_2 + 1} (α := S) (↑(ascFactorial 1 n) : S) (↑n ! : S)
Tactic: rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.one_ascFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_2
inst : Semiring S
r n : ℕ
⊢ (↑r ! : S) * eval (HAdd.hAdd (α := S) (↑r : S) 1) (ascPochhammer S n) = (↑(r + n)! : S)
have rw_mod_cast : Eq.{u_2 + 1} (α := S) (↑(r ! * eval (r + 1) (ascPochhammer ℕ n)) : S) (↑(r + n)! : S)
Tactic: rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_2
inst : Semiring S
r n : ℕ
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  Eq.{u_2 + 1} (α := S) (↑(r ! * eval (r + 1) (ascPochhammer ℕ n)) : S) (↑(r + n)! : S)
⊢ (↑r ! : S) * eval (HAdd.hAdd (α := S) (↑r : S) 1) (ascPochhammer S n) = (↑(r + n)! : S)
have rw_mod_cast₆ : Eq.{u_2 + 1} (α := S) (↑(r ! * (r + 1).ascFactorial n) : S) (↑(r + n)! : S)
Tactic: rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
r : ℕ
⊢ 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)
have pos : ∀ (h : r = 0), 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
r : ℕ
pos : ∀ (h : r = 0), 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)
⊢ 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)
have neg : ∀ (h : ¬r = 0), 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
⊢ (↑(a.ascFactorial b) : S) = eval (↑a : S) (ascPochhammer S b)
have rw : (↑(eval a (ascPochhammer ℕ b)) : S) = eval (↑a : S) (ascPochhammer S b)
Tactic: rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
rw : (↑(eval a (ascPochhammer ℕ b)) : S) = eval (↑a : S) (ascPochhammer S b)
⊢ (↑(a.ascFactorial b) : S) = eval (↑a : S) (ascPochhammer S b)
have rw₁ : eval (↑a : S) (ascPochhammer S b) = eval (↑a : S) (ascPochhammer S b)
Tactic: rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
⊢ (↑(a.descFactorial b) : S) = eval (↑(a - (b - 1)) : S) (ascPochhammer S b)
have rw : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
Tactic: rw [← ascPochhammer_eval_cast, ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 1)) : S) (↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1)) : S)
have succ : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
Tactic: simp_rw [add_succ, Nat.add_one_sub_one]