Theorem: Polynomial.lcoeff_comp_baseChange_eq (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
⊢ φ.toLinearMap ∘ₗ ↑R (lcoeff S p) = ↑R (lcoeff S' p) ∘ₗ (baseChange φ).toLinearMap
Tactic:
ext f
State after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
f : S[X]
⊢ (φ.toLinearMap ∘ₗ ↑R (lcoeff S p)) f = (↑R (lcoeff S' p) ∘ₗ (baseChange φ).toLinearMap) f

State before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
f : S[X]
⊢ (φ.toLinearMap ∘ₗ ↑R (lcoeff S p)) f = (↑R (lcoeff S' p) ∘ₗ (baseChange φ).toLinearMap) f
Tactic:
simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, lcoeff_apply,
  AlgHom.toLinearMap_apply, coeff_baseChange_apply]
State after:
no goals