Theorem: PolynomialMap.coeff_eq (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
k : ι →₀ ℕ
f : M →ₚ[R] N
⊢ ((coeff m) f) k =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)))
Tactic:
rw [coeff, coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ]
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
k : ι →₀ ℕ
f : M →ₚ[R] N
⊢ (scalarRTensor ((generize m) f)) k =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)))

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
k : ι →₀ ℕ
f : M →ₚ[R] N
⊢ (scalarRTensor ((generize m) f)) k =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)))
Tactic:
exact scalarRTensor_apply _ _
State after:
no goals