Theorem: PolynomialMap.isCompat_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 : M →ₚ[R] N
S : Type u
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x : S ⊗[R] M
⊢ (LinearMap.rTensor N φ.toLinearMap) (f.toFun' S x) = f.toFun' S' ((LinearMap.rTensor M φ.toLinearMap) x)
Tactic:
simpa only using _root_.congr_fun (f.isCompat' φ) x
State after:
no goals