-- Mathlib/RingTheory/Binomial.lean
theorem ascPochhammer_smeval_cast (R : Type*) [Semiring R] {S : Type*} [NonAssocSemiring S]
    [Pow S ℕ] [Module R S] [IsScalarTower R S S] [NatPowAssoc S]
    (x : S) (n : ℕ) : (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x

Proof state:
case succ
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Pow S ℕ
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : NatPowAssoc S
x : S
n : ℕ
hn : (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x
⊢ (ascPochhammer R (n + 1)).smeval x = (ascPochhammer ℕ (n + 1)).smeval x

Tactic:
simp only [ascPochhammer_succ_right, mul_add, smeval_add, smeval_mul_X, ← Nat.cast_comm]

Result:
case succ
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Pow S ℕ
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : NatPowAssoc S
x : S
n : ℕ
hn : (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x
⊢ (ascPochhammer R n).smeval x * x + (↑n * ascPochhammer R n).smeval x =
    (ascPochhammer ℕ n).smeval x * x + (↑n * ascPochhammer ℕ n).smeval x

Proof state:
case succ
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Pow S ℕ
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : NatPowAssoc S
x : S
n : ℕ
hn : (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x
⊢ (ascPochhammer ℕ n).smeval x * x + n • (ascPochhammer ℕ n).smeval x =
    (ascPochhammer ℕ n).smeval x * x + ↑n • (ascPochhammer ℕ n).smeval x

Tactic:
simp only [nsmul_eq_mul, Nat.cast_id]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Pow S ℕ
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : NatPowAssoc S
x : S
n : ℕ
⊢ (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x

Tactic:
induction n with
| zero => simp only [ascPochhammer_zero, smeval_one, one_smul]
| succ n hn =>
  simp only [ascPochhammer_succ_right, mul_add, smeval_add, smeval_mul_X, ← Nat.cast_comm]
  simp only [← C_eq_natCast, smeval_C_mul, hn, Nat.cast_smul_eq_nsmul R n]
  simp only [nsmul_eq_mul, Nat.cast_id]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Pow S ℕ
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : NatPowAssoc S
x : S
n : ℕ
hn : (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x
⊢ (ascPochhammer R n).smeval x * x + (↑n * ascPochhammer R n).smeval x =
    (ascPochhammer ℕ n).smeval x * x + (↑n * ascPochhammer ℕ n).smeval x

Tactic:
simp only [← C_eq_natCast, smeval_C_mul, hn, Nat.cast_smul_eq_nsmul R n]

Result:
case succ
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Pow S ℕ
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : NatPowAssoc S
x : S
n : ℕ
hn : (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x
⊢ (ascPochhammer ℕ n).smeval x * x + n • (ascPochhammer ℕ n).smeval x =
    (ascPochhammer ℕ n).smeval x * x + ↑n • (ascPochhammer ℕ n).smeval x

Proof state:
case zero
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Pow S ℕ
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : NatPowAssoc S
x : S
⊢ (ascPochhammer R 0).smeval x = (ascPochhammer ℕ 0).smeval x

Tactic:
simp only [ascPochhammer_zero, smeval_one, one_smul]

Result:
no goals