Theorem: PolynomialMap.smul_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
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (r • f).toFun S = r • 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
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ (r • f).toFun S t = (r • 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
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ (r • f).toFun S t = (r • 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
r a b : R
f g : M →ₚ[R] N
S : Type u_5
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
⊢ (r • f).toFun S t = (r • 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
r a b : R
f g : M →ₚ[R] N
S : Type u_5
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
⊢ (r • f).toFun S t = (r • f.toFun S) t
Tactic:
simp only [toFun_eq_toFunLifted_apply _ ha, smul_def, Pi.smul_apply, map_smul]
State after:
no goals