Theorem: PolynomialMap.comp_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✝
R : Type u
inst✝¹⁰ : CommRing R
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ (g.comp f).toFun S m = g.toFun S (f.toFun S m)
Tactic:
simp only [comp_toFun, Function.comp_apply]
State after:
no goals