Theorem: MvPolynomial.lcoeff_comp_baseChange_eq (DividedPowers/DPAlgebra/BaseChange.lean)

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

State before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
f : MvPolynomial σ S
⊢ (φ.toLinearMap ∘ₗ ↑R (lcoeff S m)) f = (↑R (lcoeff S' m) ∘ₗ (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