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 m : ℕ
zero : descPochhammer R n * comp (descPochhammer R 0) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + 0)
⊢ descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
have succ : ∀ (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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
⊢ eval (-r) (ascPochhammer R 0) = HPow.hPow (α := R) (β := ℕ) (-1) 0 * eval r (descPochhammer R 0)
have rw : eval (-r) 1 = HPow.hPow (α := R) (β := ℕ) (-1) 0 * eval r 1
Tactic: rw [ascPochhammer_zero, descPochhammer_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw : eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₁ : eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₂ : eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
    eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₃ : eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₃ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₄ : eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (↑k : R[X]) (ascPochhammer R k)) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₃ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₄ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (↑k : R[X]) (ascPochhammer R k)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₅ : eval (-r) (ascPochhammer R k) * -r + (↑k : R) * eval (-r) (ascPochhammer R k) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₃ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₄ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (↑k : R[X]) (ascPochhammer R k)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₅ :
  eval (-r) (ascPochhammer R k) * -r + (↑k : R) * eval (-r) (ascPochhammer R k) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₆ : eval (-r) (ascPochhammer R k) * -r + eval (-r) (ascPochhammer R k) * (↑k : R) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₃ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₄ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (↑k : R[X]) (ascPochhammer R k)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₅ :
  eval (-r) (ascPochhammer R k) * -r + (↑k : R) * eval (-r) (ascPochhammer R k) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₆ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (ascPochhammer R k) * (↑k : R) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₇ : eval (-r) (ascPochhammer R k) * (-r + (↑k : R)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₃ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₄ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (↑k : R[X]) (ascPochhammer R k)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₅ :
  eval (-r) (ascPochhammer R k) * -r + (↑k : R) * eval (-r) (ascPochhammer R k) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₆ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (ascPochhammer R k) * (↑k : R) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₇ :
  eval (-r) (ascPochhammer R k) * (-r + (↑k : R)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₈ : HPow.hPow (α := R) (-1) k * eval r (descPochhammer R k) * (-r + (↑k : R)) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₃ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₄ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (↑k : R[X]) (ascPochhammer R k)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₅ :
  eval (-r) (ascPochhammer R k) * -r + (↑k : R) * eval (-r) (ascPochhammer R k) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₆ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (ascPochhammer R k) * (↑k : R) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₇ :
  eval (-r) (ascPochhammer R k) * (-r + (↑k : R)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₈ :
  HPow.hPow (α := R) (-1) k * eval r (descPochhammer R k) * (-r + (↑k : R)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₉ : HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₃ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₄ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (↑k : R[X]) (ascPochhammer R k)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₅ :
  eval (-r) (ascPochhammer R k) * -r + (↑k : R) * eval (-r) (ascPochhammer R k) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₆ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (ascPochhammer R k) * (↑k : R) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₇ :
  eval (-r) (ascPochhammer R k) * (-r + (↑k : R)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₈ :
  HPow.hPow (α := R) (-1) k * eval r (descPochhammer R k) * (-r + (↑k : R)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₉ :
  HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₁₀ : HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
  HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R k * HSub.hSub (α := R[X]) X (↑k : R[X]))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₃ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₄ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (↑k : R[X]) (ascPochhammer R k)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₅ :
  eval (-r) (ascPochhammer R k) * -r + (↑k : R) * eval (-r) (ascPochhammer R k) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₆ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (ascPochhammer R k) * (↑k : R) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₇ :
  eval (-r) (ascPochhammer R k) * (-r + (↑k : R)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₈ :
  HPow.hPow (α := R) (-1) k * eval r (descPochhammer R k) * (-r + (↑k : R)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₉ :
  HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁₀ :
  HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R k * HSub.hSub (α := R[X]) X (↑k : R[X]))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₁₁ : HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
  HPow.hPow (α := R) (-1) (k + 1) *
    eval r (HMul.hMul (α := R[X]) (descPochhammer R k) X - HMul.hMul (α := R[X]) (descPochhammer R k) (↑k : R[X]))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]