awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
have zero : descPochhammer ℤ (HAdd.hAdd (α := ℕ) 0 1) = descPochhammer ℤ 0 * HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X])
Tactic: induction n with
  | zero => simp [descPochhammer]
  | succ n ih =>
    conv_lhs =>
      rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]
    rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
zero : descPochhammer ℤ (HAdd.hAdd (α := ℕ) 0 1) = descPochhammer ℤ 0 * HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X])
⊢ descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
have succ : ∀ (n : ℕ) (ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])),
  descPochhammer ℤ (n + 1 + 1) = descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])
Tactic: induction n with
  | zero => simp [descPochhammer]
  | succ n ih =>
    conv_lhs =>
      rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]
    rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
n : ℕ
hn : natDegree (descPochhammer R n) = n
⊢ natDegree (descPochhammer R (n + 1)) = n + 1
have this : (HSub.hSub (α := R[X]) X (↑n : R[X])).natDegree = 1
Tactic: have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
n : ℕ
hn : natDegree (descPochhammer R n) = n
this : (HSub.hSub (α := R[X]) X (↑n : R[X])).natDegree = 1
⊢ natDegree (descPochhammer R (n + 1)) = n + 1
have rw : Ne (α := R[X]) (descPochhammer R n) 0
Tactic: rw [descPochhammer_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:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
n : ℕ
hn : natDegree (descPochhammer R n) = n
this : (HSub.hSub (α := R[X]) X (↑n : R[X])).natDegree = 1
⊢ Ne (α := R[X]) (descPochhammer R n) 0
have zero : ∀ (hn : natDegree (descPochhammer R 0) = 0) (this : (HSub.hSub (α := R[X]) X (↑0 : R[X])).natDegree = 1),
  Ne (α := R[X]) (descPochhammer R 0) 0
Tactic: cases n
Cleared hypotheses: n, hn, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
n : ℕ
hn : natDegree (descPochhammer R n) = n
this : (HSub.hSub (α := R[X]) X (↑n : R[X])).natDegree = 1
zero :
  ∀ (hn : natDegree (descPochhammer R 0) = 0) (this : (HSub.hSub (α := R[X]) X (↑0 : R[X])).natDegree = 1),
    Ne (α := R[X]) (descPochhammer R 0) 0
⊢ Ne (α := R[X]) (descPochhammer R n) 0
have succ : ∀ (n : ℕ) (hn : natDegree (descPochhammer R (n + 1)) = n + 1)
  (this : (HSub.hSub (α := R[X]) X (↑(n + 1) : R[X])).natDegree = 1), Ne (α := R[X]) (descPochhammer R (n + 1)) 0
Tactic: cases n
Cleared hypotheses: n, hn, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
⊢ natDegree (descPochhammer R n) = n
have zero : natDegree (descPochhammer R 0) = 0
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)
    rw [descPochhammer_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:
R : Type u
inst : Ring R
n : ℕ
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
zero : natDegree (descPochhammer R 0) = 0
⊢ natDegree (descPochhammer R n) = n
have succ : ∀ (n : ℕ) (hn : natDegree (descPochhammer R n) = n), natDegree (descPochhammer R (n + 1)) = n + 1
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)
    rw [descPochhammer_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 : Ring S
n : ℕ
k : S
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))
have rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
Tactic: rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
n : ℕ
k : S
rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))
have rw₁ : eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X - HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
  eval k (descPochhammer S n) * (k - (↑n : S))
Tactic: rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
n : ℕ
k : S
rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X - HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))
have rw₂ : eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X) -
    eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
  eval k (descPochhammer S n) * (k - (↑n : S))
Tactic: rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
n : ℕ
k : S
rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X - HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X) -
      eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))
have rw₃ : eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
  eval k (descPochhammer S n) * (k - (↑n : S))
Tactic: rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
n : ℕ
k : S
rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X - HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X) -
      eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₃ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))
have rw₄ : eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (descPochhammer S n)) =
  eval k (descPochhammer S n) * (k - (↑n : S))
Tactic: rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
n : ℕ
k : S
rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X - HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X) -
      eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₃ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₄ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (descPochhammer S n)) =
    eval k (descPochhammer S n) * (k - (↑n : S))
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))
have rw₅ : eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (descPochhammer S n)) =
  eval k (descPochhammer S n) * (k - (↑n : S))
Tactic: rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
n : ℕ
k : S
rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X - HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X) -
      eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₃ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₄ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (descPochhammer S n)) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₅ :
  eval k (descPochhammer S n) * k -
      eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (descPochhammer S n)) =
    eval k (descPochhammer S n) * (k - (↑n : S))
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))
have rw₆ : eval k (descPochhammer S n) * k - (↑n : S) * eval k (descPochhammer S n) = eval k (descPochhammer S n) * (k - (↑n : S))
Tactic: rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
n : ℕ
k : S
rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X - HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X) -
      eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₃ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₄ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (descPochhammer S n)) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₅ :
  eval k (descPochhammer S n) * k -
      eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (descPochhammer S n)) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₆ :
  eval k (descPochhammer S n) * k - (↑n : S) * eval k (descPochhammer S n) =
    eval k (descPochhammer S n) * (k - (↑n : S))
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))
have rw₇ : eval k (descPochhammer S n) * k - eval k (descPochhammer S n) * (↑n : S) = eval k (descPochhammer S n) * (k - (↑n : S))
Tactic: rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
n : ℕ
k : S
rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X - HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X) -
      eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₃ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₄ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (descPochhammer S n)) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₅ :
  eval k (descPochhammer S n) * k -
      eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (descPochhammer S n)) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₆ :
  eval k (descPochhammer S n) * k - (↑n : S) * eval k (descPochhammer S n) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₇ :
  eval k (descPochhammer S n) * k - eval k (descPochhammer S n) * (↑n : S) =
    eval k (descPochhammer S n) * (k - (↑n : S))
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))
have rw₈ : eval k (descPochhammer S n) * (k - (↑n : S)) = eval k (descPochhammer S n) * (k - (↑n : S))
Tactic: rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ comp (descPochhammer R (n + 1)) (HSub.hSub (α := R[X]) X 1) =
    descPochhammer R (n + 1) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 • comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)
have suffices : comp (descPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X 1) =
  descPochhammer ℤ (n + 1) - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1)
Tactic: suffices (descPochhammer ℤ (n + 1)).comp (X - 1) =
      descPochhammer ℤ (n + 1) - (n + 1) * (descPochhammer ℤ n).comp (X - 1)
    by simpa [map_comp] using congr_arg (Polynomial.map (Int.castRingHom R)) this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ comp (descPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X 1) =
    X * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1) -
      HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1)
have rw : (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1) =
  (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1) * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1)
Tactic: rw [← sub_mul, descPochhammer_succ_right ℤ n, mul_comp, mul_comm, sub_comp, X_comp, natCast_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
⊢ descPochhammer ℤ 0 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
have zero : 1 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
Tactic: rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
zero : 1 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
⊢ descPochhammer ℤ 0 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
have zero₁ : 1 = comp 1 (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
Tactic: rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
zero : 1 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
zero₁ : 1 = comp 1 (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
⊢ descPochhammer ℤ 0 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
have zero₂ : Eq (α := ℤ[X]) 1 1
Tactic: rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₃ : descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
  comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₃ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₄ : descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
  (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₃ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₄ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₅ : comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
  (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₃ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₄ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₅ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₆ : comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
  (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1) * X).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]