Theorem: PolynomialMap.isCompat (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 : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
⊢ ⇑(LinearMap.rTensor N h.toLinearMap) ∘ f.toFun S = f.toFun T ∘ ⇑(LinearMap.rTensor M h.toLinearMap)
Tactic:
ext t
State after:
case h
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 : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
⊢ (⇑(LinearMap.rTensor N h.toLinearMap) ∘ f.toFun S) t = (f.toFun T ∘ ⇑(LinearMap.rTensor M h.toLinearMap)) t

State before:
case h
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 : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
⊢ (⇑(LinearMap.rTensor N h.toLinearMap) ∘ f.toFun S) t = (f.toFun T ∘ ⇑(LinearMap.rTensor M h.toLinearMap)) t
Tactic:
simp only [Function.comp_apply, PolynomialMap.isCompat_apply]
State after:
no goals