Theorem: PolynomialMap.toFun_eq_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✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ f.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✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ f.toFun S t = 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✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ f.toFun S t = 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✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
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
⊢ f.toFun S t = 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✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
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
⊢ f.toFun S t = f.toFun' S t
Tactic:
simp only [f.toFun_eq_toFunLifted_apply ha, toFunLifted, f.isCompat_apply']
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✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
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
⊢ f.toFun' S ((LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p) = 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✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
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
⊢ f.toFun' S ((LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p) = f.toFun' S t
Tactic:
exact congr_arg _ ha
State after:
no goals