-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
rw :
  n.choose k • smeval (descPochhammer ℤ (k + (n - k))) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₁ :
  n.choose k •
      (descPochhammer ℤ k * Polynomial.comp (descPochhammer ℤ (n - k)) (HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X]))).smeval r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₂ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        (Polynomial.comp (descPochhammer ℤ (n - k)) (HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X]))).smeval r) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₃ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) ((HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X])).smeval r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₄ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (smeval (R := ℤ) X r - smeval (R := ℤ) (↑k : ℤ[X]) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₅ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) (↑k : ℤ[X]) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₆ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k))
          (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) ((C : (a : ℤ) → ℤ[X]) (↑k : ℤ)) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₇ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k))
          (HPow.hPow (β := ℕ) r 1 - HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0))) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₈ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (r - HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0))) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₉ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₁₀ :
  n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑(↑k : ℤ) : R))) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₁₁ :
  n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R))) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
⊢ n.choose k • smeval (descPochhammer ℤ (n - k + k)) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
have rw₁₂ : (↑(n.choose k) : R) * (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R))) =
  (↑(n.choose k) : R) * (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
Tactic: rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X,
    ← C_eq_natCast, smeval_C, npow_one, npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]