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 k : ℕ
rw : (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (map (algebraMap ℕ S) (ascPochhammer ℕ n))
rw₁ : (↑(eval k (ascPochhammer ℕ n)) : S) = eval₂ (algebraMap ℕ S) (↑k : S) (ascPochhammer ℕ n)
rw₂ : (algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) = eval₂ (algebraMap ℕ S) (↑k : S) (ascPochhammer ℕ n)
rw₃ :
  Eq (α := S) ((algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) : S)
    ((algebraMap ℕ S : (a : ℕ) → S) (eval (↑k : ℕ) (ascPochhammer ℕ n)) : S)
⊢ (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (ascPochhammer S n)
have rw₄ : Eq (α := S) ((algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) : S)
  ((algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) : S)
Tactic: rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
      eval₂_at_natCast, Nat.cast_id]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
⊢ eval 0 (ascPochhammer S n) = if n = 0 then 1 else 0
have zero : eval 0 (ascPochhammer S 0) = if Eq (α := ℕ) 0 0 then 1 else 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
zero : eval 0 (ascPochhammer S 0) = if Eq (α := ℕ) 0 0 then 1 else 0
⊢ eval 0 (ascPochhammer S n) = if n = 0 then 1 else 0
have succ : ∀ (n : ℕ), eval 0 (ascPochhammer S (n + 1)) = if n + 1 = 0 then 1 else 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
S : Type u
inst : Semiring S
n : ℕ
h : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
⊢ ascPochhammer S (n + 1) = ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])
have h₁ : Eq (α := S[X]) (map (algebraMap ℕ S) (ascPochhammer ℕ (n + 1)))
  (map (algebraMap ℕ S) (ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])))
Tactic: apply_fun Polynomial.map (algebraMap ℕ S) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
⊢ ascPochhammer S (n + 1) = ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])
have suffices : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
Tactic: suffices h : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + (n : ℕ[X])) by
    apply_fun Polynomial.map (algebraMap ℕ S) at h
    simpa only [ascPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_natCast] using h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
| ascPochhammer ℕ (n + 1 + 1)
have rw : ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑n.succ : ℕ[X])
Tactic: rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
⊢ ascPochhammer ℕ (n + 1 + 1) = ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])
have conv_lhs : ascPochhammer ℕ (n + 1 + 1) = ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])
Tactic: conv_lhs =>
      rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
conv_lhs : ascPochhammer ℕ (n + 1 + 1) = ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])
⊢ ascPochhammer ℕ (n + 1 + 1) = ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])
have succ : ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑n.succ : ℕ[X]) =
  ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])
Tactic: conv_lhs =>
      rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
⊢ ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
have zero : ascPochhammer ℕ (HAdd.hAdd (α := ℕ) 0 1) = ascPochhammer ℕ 0 * HAdd.hAdd (α := ℕ[X]) X (↑0 : ℕ[X])
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    conv_lhs =>
      rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
zero : ascPochhammer ℕ (HAdd.hAdd (α := ℕ) 0 1) = ascPochhammer ℕ 0 * HAdd.hAdd (α := ℕ[X]) X (↑0 : ℕ[X])
⊢ ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
have succ : ∀ (n : ℕ) (ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])),
  ascPochhammer ℕ (n + 1 + 1) = ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    conv_lhs =>
      rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))
have rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))
have rw₁ : eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X + HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
  eval k (ascPochhammer S n) * (k + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X + HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))
have rw₂ : eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X) + eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
  eval k (ascPochhammer S n) * (k + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X + HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X) +
      eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))
have rw₃ : eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
  eval k (ascPochhammer S n) * (k + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X + HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X) +
      eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₃ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))
have rw₄ : eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (ascPochhammer S n)) =
  eval k (ascPochhammer S n) * (k + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X + HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X) +
      eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₃ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₄ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (ascPochhammer S n)) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))
have rw₅ : eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (ascPochhammer S n)) =
  eval k (ascPochhammer S n) * (k + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X + HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X) +
      eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₃ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₄ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (ascPochhammer S n)) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₅ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (ascPochhammer S n)) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))
have rw₆ : eval k (ascPochhammer S n) * k + (↑n : S) * eval k (ascPochhammer S n) = eval k (ascPochhammer S n) * (k + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X + HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X) +
      eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₃ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₄ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (ascPochhammer S n)) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₅ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (ascPochhammer S n)) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₆ :
  eval k (ascPochhammer S n) * k + (↑n : S) * eval k (ascPochhammer S n) = eval k (ascPochhammer S n) * (k + (↑n : S))
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))
have rw₇ : eval k (ascPochhammer S n) * k + eval k (ascPochhammer S n) * (↑n : S) = eval k (ascPochhammer S n) * (k + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X + HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X) +
      eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₃ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₄ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (ascPochhammer S n)) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₅ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (ascPochhammer S n)) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₆ :
  eval k (ascPochhammer S n) * k + (↑n : S) * eval k (ascPochhammer S n) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₇ :
  eval k (ascPochhammer S n) * k + eval k (ascPochhammer S n) * (↑n : S) = eval k (ascPochhammer S n) * (k + (↑n : S))
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))
have rw₈ : eval k (ascPochhammer S n) * (k + (↑n : S)) = eval k (ascPochhammer S n) * (k + (↑n : S))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
⊢ comp (ascPochhammer S (n + 1)) (HAdd.hAdd (α := S[X]) X 1) =
    ascPochhammer S (n + 1) + (n + 1) • comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)
have suffices : comp (ascPochhammer ℕ (n + 1)) (HAdd.hAdd (α := ℕ[X]) X 1) =
  ascPochhammer ℕ (n + 1) + HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) 1 * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)
Tactic: suffices (ascPochhammer ℕ (n + 1)).comp (X + 1) =
      ascPochhammer ℕ (n + 1) + (n + 1) * (ascPochhammer ℕ n).comp (X + 1)
    by simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
⊢ comp (ascPochhammer ℕ (n + 1)) (HAdd.hAdd (α := ℕ[X]) X 1) =
    X * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1) +
      HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) 1 * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)
have rw : (HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) X + 1) * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1) =
  (X + HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) 1) * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)
Tactic: rw [← add_mul, ascPochhammer_succ_right ℕ n, mul_comp, mul_comm, add_comp, X_comp, natCast_comp,
    add_comm, ← 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)
⊢ 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 *
    (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))
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))
⊢ 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 *
    (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))
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))
⊢ 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 * 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))
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))
⊢ 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 + 1))
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))
⊢ 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 + 1)
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)
⊢ 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) * HAdd.hAdd (α := S[X]) X (↑(n + 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]