Theorem: PolynomialMap.comp_assoc (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
⊢ h.comp (g.comp f) = (h.comp g).comp f
Tactic:
ext
State after:
case toFun'.h.h.h.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✝ : 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
x✝³ : Type u
x✝² : CommRing x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (h.comp (g.comp f)).toFun' x✝³ x✝ = ((h.comp g).comp f).toFun' x✝³ x✝

State before:
case toFun'.h.h.h.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✝ : 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
x✝³ : Type u
x✝² : CommRing x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (h.comp (g.comp f)).toFun' x✝³ x✝ = ((h.comp g).comp f).toFun' x✝³ x✝
Tactic:
simp only [comp_toFun']
State after:
case toFun'.h.h.h.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✝ : 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
x✝³ : Type u
x✝² : CommRing x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (h.toFun' x✝³ ∘ g.toFun' x✝³ ∘ f.toFun' x✝³) x✝ = ((h.toFun' x✝³ ∘ g.toFun' x✝³) ∘ f.toFun' x✝³) x✝

State before:
case toFun'.h.h.h.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✝ : 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
x✝³ : Type u
x✝² : CommRing x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (h.toFun' x✝³ ∘ g.toFun' x✝³ ∘ f.toFun' x✝³) x✝ = ((h.toFun' x✝³ ∘ g.toFun' x✝³) ∘ f.toFun' x✝³) x✝
Tactic:
rfl
State after:
no goals