Theorem: PolynomialMap.toFun_eq_toFunLifted_apply (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ f.toFun S t = (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p)
Tactic:
rw [PolynomialMap.toFun, ← ha, (toFunLifted_factorsThrough_π f).extend_apply, toFunLifted]
State after:
no goals