case refine_3
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
n✝ : ℕ
a✝¹ : R
a✝ : comp (comp (↑C a✝¹ * X ^ n✝) ψ) χ = comp (↑C a✝¹ * X ^ n✝) (comp ψ χ)
⊢ comp (comp (↑C a✝¹ * X ^ (n✝ + 1)) ψ) χ = comp (↑C a✝¹ * X ^ (n✝ + 1)) (comp ψ χ)
case refine_3
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (n : ℕ) (a : R),
    comp (comp (↑C a * X ^ n) ψ) χ = comp (↑C a * X ^ n) (comp ψ χ) →
      comp (comp (↑C a * X ^ (n + 1)) ψ) χ = comp (↑C a * X ^ (n + 1)) (comp ψ χ)
intros
no goals
case refine_3
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
n✝ : ℕ
a✝¹ : R
a✝ : comp (comp (↑C a✝¹ * X ^ n✝) ψ) χ = comp (↑C a✝¹ * X ^ n✝) (comp ψ χ)
⊢ comp (comp (↑C a✝¹ * X ^ (n✝ + 1)) ψ) χ = comp (↑C a✝¹ * X ^ (n✝ + 1)) (comp ψ χ)
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ', ← mul_assoc]