-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
rw :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r -
        smeval (R := ℤ) ((C : (a : ℤ) → ℤ[X]) (↑k : ℤ)) r * smeval (descPochhammer ℤ k) r)
rw₁ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r -
        HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0) * smeval (descPochhammer ℤ k) r)
rw₂ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r)
rw₃ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + k • smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r)
rw₄ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
      (k • smeval (descPochhammer ℤ k) r +
        (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r))
rw₅ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
        k • smeval (descPochhammer ℤ k) r)
rw₆ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
        (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r) +
      k • smeval (descPochhammer ℤ k) r
rw₇ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + r * smeval (descPochhammer ℤ k) r -
        HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
      k • smeval (descPochhammer ℤ k) r
rw₈ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + r * smeval (descPochhammer ℤ k) r -
        HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
      (↑k : R) * smeval (descPochhammer ℤ k) r
rw₉ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + r * smeval (descPochhammer ℤ k) r -
        (↑(↑k : ℤ) : R) * smeval (descPochhammer ℤ k) r +
      (↑k : R) * smeval (descPochhammer ℤ k) r
rw₁₀ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + r * smeval (descPochhammer ℤ k) r - (↑k : R) * smeval (descPochhammer ℤ k) r +
      (↑k : R) * smeval (descPochhammer ℤ k) r
⊢ r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - smeval (R := ℤ) (↑k : ℤ[X]) r * smeval (descPochhammer ℤ k) r)
have rw₁₁ : r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
  smeval (descPochhammer ℤ k) r + r * smeval (descPochhammer ℤ k) r
Tactic: rw [← C_eq_natCast, smeval_C, npow_zero, add_comm (k • smeval (descPochhammer ℤ k) r) _,
    add_assoc, add_comm (k • smeval (descPochhammer ℤ k) r) _, ← add_assoc, ← add_sub_assoc,
    nsmul_eq_mul, zsmul_one, Int.cast_natCast, sub_add_cancel, add_comm]