Theorem: PolynomialMap.ofLinearMap_toFun (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (ofLinearMap u).toFun S = ⇑(baseChange S u)
Tactic:
ext sm
State after:
case h
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
sm : S ⊗[R] M
⊢ (ofLinearMap u).toFun S sm = (baseChange S u) sm

State before:
case h
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
sm : S ⊗[R] M
⊢ (ofLinearMap u).toFun S sm = (baseChange S u) sm
Tactic:
obtain ⟨n, φ, p, rfl⟩ := exists_lift sm
State after:
case h.intro.intro.intro
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
φ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (ofLinearMap u).toFun S ((rTensor M φ.toLinearMap) p) = (baseChange S u) ((rTensor M φ.toLinearMap) p)

State before:
case h.intro.intro.intro
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
φ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (ofLinearMap u).toFun S ((rTensor M φ.toLinearMap) p) = (baseChange S u) ((rTensor M φ.toLinearMap) p)
Tactic:
simp only [← isCompat_apply, toFun_eq_toFun', ofLinearMap_toFun', baseChange_eq_ltensor,
  ← LinearMap.comp_apply, rTensor_comp_lTensor, lTensor_comp_rTensor]
State after:
no goals