awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₅ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (X * comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1))
succ₆ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1) * X)
succ₇ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1)) * (r - (↑n : R))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₈ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
  eval (r - (↑n : R)) (comp (ascPochhammer R n) (map (algebraMap ℕ R) (HAdd.hAdd (α := ℕ[X]) X 1))) * (r - (↑n : R))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₅ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (X * comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1))
succ₆ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1) * X)
succ₇ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1)) * (r - (↑n : R))
succ₈ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (map (algebraMap ℕ R) (HAdd.hAdd (α := ℕ[X]) X 1))) * (r - (↑n : R))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₉ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
  eval (eval₂ (algebraMap ℕ R) (r - (↑n : R)) (HAdd.hAdd (α := ℕ[X]) X 1)) (ascPochhammer R n) * (r - (↑n : R))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₅ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (X * comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1))
succ₆ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1) * X)
succ₇ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1)) * (r - (↑n : R))
succ₈ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (map (algebraMap ℕ R) (HAdd.hAdd (α := ℕ[X]) X 1))) * (r - (↑n : R))
succ₉ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (eval₂ (algebraMap ℕ R) (r - (↑n : R)) (HAdd.hAdd (α := ℕ[X]) X 1)) (ascPochhammer R n) * (r - (↑n : R))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₁₀ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
  eval (eval₂ (algebraMap ℕ R) (r - (↑n : R)) X + eval₂ (algebraMap ℕ R) (r - (↑n : R)) 1) (ascPochhammer R n) *
    (r - (↑n : R))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₅ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (X * comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1))
succ₆ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1) * X)
succ₇ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1)) * (r - (↑n : R))
succ₈ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (map (algebraMap ℕ R) (HAdd.hAdd (α := ℕ[X]) X 1))) * (r - (↑n : R))
succ₉ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (eval₂ (algebraMap ℕ R) (r - (↑n : R)) (HAdd.hAdd (α := ℕ[X]) X 1)) (ascPochhammer R n) * (r - (↑n : R))
succ₁₀ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (eval₂ (algebraMap ℕ R) (r - (↑n : R)) X + eval₂ (algebraMap ℕ R) (r - (↑n : R)) 1) (ascPochhammer R n) *
      (r - (↑n : R))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₁₁ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
  eval (r - (↑n : R) + eval₂ (algebraMap ℕ R) (r - (↑n : R)) 1) (ascPochhammer R n) * (r - (↑n : R))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₅ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (X * comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1))
succ₆ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1) * X)
succ₇ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1)) * (r - (↑n : R))
succ₈ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (map (algebraMap ℕ R) (HAdd.hAdd (α := ℕ[X]) X 1))) * (r - (↑n : R))
succ₉ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (eval₂ (algebraMap ℕ R) (r - (↑n : R)) (HAdd.hAdd (α := ℕ[X]) X 1)) (ascPochhammer R n) * (r - (↑n : R))
succ₁₀ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (eval₂ (algebraMap ℕ R) (r - (↑n : R)) X + eval₂ (algebraMap ℕ R) (r - (↑n : R)) 1) (ascPochhammer R n) *
      (r - (↑n : R))
succ₁₁ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R) + eval₂ (algebraMap ℕ R) (r - (↑n : R)) 1) (ascPochhammer R n) * (r - (↑n : R))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₁₂ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
⊢ eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
have zero : eval r (descPochhammer R 0) = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
Tactic: induction n with
  | zero => rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
zero : eval r (descPochhammer R 0) = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
⊢ eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
have succ : ∀ (n : ℕ) (ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)),
  eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
Tactic: induction n with
  | zero => rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n m : ℕ
ih : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
⊢ descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
have succ : descPochhammer R n *
    (descPochhammer R m * HSub.hSub (α := R[X]) X (↑m : R[X])).comp (HSub.hSub (α := R[X]) X (↑n : R[X])) =
  descPochhammer R (n + (m + 1))
Tactic: rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n m : ℕ
ih : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
succ :
  descPochhammer R n *
      (descPochhammer R m * HSub.hSub (α := R[X]) X (↑m : R[X])).comp (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
⊢ descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
have succ₁ : descPochhammer R n *
    (comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
      (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))) =
  descPochhammer R (n + (m + 1))
Tactic: rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n m : ℕ
ih : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
succ :
  descPochhammer R n *
      (descPochhammer R m * HSub.hSub (α := R[X]) X (↑m : R[X])).comp (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
succ₁ :
  descPochhammer R n *
      (comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
        (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))) =
    descPochhammer R (n + (m + 1))
⊢ descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
have succ₂ : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
    (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
  descPochhammer R (n + (m + 1))
Tactic: rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n m : ℕ
ih : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
succ :
  descPochhammer R n *
      (descPochhammer R m * HSub.hSub (α := R[X]) X (↑m : R[X])).comp (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
succ₁ :
  descPochhammer R n *
      (comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
        (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))) =
    descPochhammer R (n + (m + 1))
succ₂ :
  descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
      (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + (m + 1))
⊢ descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
have succ₃ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + (m + 1))
Tactic: rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n m : ℕ
ih : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
succ :
  descPochhammer R n *
      (descPochhammer R m * HSub.hSub (α := R[X]) X (↑m : R[X])).comp (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
succ₁ :
  descPochhammer R n *
      (comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
        (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))) =
    descPochhammer R (n + (m + 1))
succ₂ :
  descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
      (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + (m + 1))
succ₃ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + (m + 1))
⊢ descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
have succ₄ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + m + 1)
Tactic: rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n m : ℕ
ih : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
succ :
  descPochhammer R n *
      (descPochhammer R m * HSub.hSub (α := R[X]) X (↑m : R[X])).comp (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
succ₁ :
  descPochhammer R n *
      (comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
        (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))) =
    descPochhammer R (n + (m + 1))
succ₂ :
  descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
      (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + (m + 1))
succ₃ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + (m + 1))
succ₄ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + m + 1)
⊢ descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
have succ₅ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
  descPochhammer R (n + m) * HSub.hSub (α := R[X]) X (↑(n + m) : R[X])
Tactic: rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n m : ℕ
ih : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
succ :
  descPochhammer R n *
      (descPochhammer R m * HSub.hSub (α := R[X]) X (↑m : R[X])).comp (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
succ₁ :
  descPochhammer R n *
      (comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
        (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))) =
    descPochhammer R (n + (m + 1))
succ₂ :
  descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
      (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + (m + 1))
succ₃ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + (m + 1))
succ₄ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + m + 1)
succ₅ :
  descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + m) * HSub.hSub (α := R[X]) X (↑(n + m) : R[X])
⊢ descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
have succ₆ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
  descPochhammer R (n + m) * (X - HAdd.hAdd (α := R[X]) (↑n : R[X]) (↑m : R[X]))
Tactic: rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n m : ℕ
ih : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
succ :
  descPochhammer R n *
      (descPochhammer R m * HSub.hSub (α := R[X]) X (↑m : R[X])).comp (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
succ₁ :
  descPochhammer R n *
      (comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
        (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))) =
    descPochhammer R (n + (m + 1))
succ₂ :
  descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
      (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + (m + 1))
succ₃ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + (m + 1))
succ₄ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + m + 1)
succ₅ :
  descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + m) * HSub.hSub (α := R[X]) X (↑(n + m) : R[X])
succ₆ :
  descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + m) * (X - HAdd.hAdd (α := R[X]) (↑n : R[X]) (↑m : R[X]))
⊢ descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
have succ₇ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
  descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))
Tactic: rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n m : ℕ
⊢ descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
have zero : descPochhammer R n * comp (descPochhammer R 0) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + 0)
Tactic: induction m with
  | zero => simp
  | succ m ih =>
    rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
Cleared hypotheses: m