-- 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]))
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]))
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) -
        eval r (HMul.hMul (α := R[X]) (descPochhammer R k) (↑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 (descPochhammer R k) * r - eval r (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]