Theorem: PolynomialMap.comp_toFun (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
⊢ (g.comp f).toFun S = g.toFun S ∘ f.toFun S
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✝ : 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
t : S ⊗[R] M
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) 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✝ : 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
t : S ⊗[R] M
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t
Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
State after:
case h.intro.mk
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
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t

State before:
case h.intro.mk
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
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t
Tactic:
have hb : PolynomialMap.π R N S ⟨s, f.toFun' _ p⟩ = f.toFun S t := by
  simp only [toFun_eq_toFunLifted_apply _ ha, π]
State after:
case h.intro.mk
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
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
hb : PolynomialMap.π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = f.toFun S t
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t

State before:
case h.intro.mk
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
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
hb : PolynomialMap.π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = f.toFun S t
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t
Tactic:
rw [Function.comp_apply, toFun_eq_toFunLifted_apply _ hb, toFun_eq_toFunLifted_apply _ ha,
  comp_toFun', Function.comp_apply]
State after:
no goals

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
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ PolynomialMap.π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = f.toFun S t
Tactic:
simp only [toFun_eq_toFunLifted_apply _ ha, π]
State after:
no goals