Theorem: PolynomialMap.add_smul (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
⊢ (a + b) • f = a • f + b • f
Tactic:
ext S _ _ x
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
r a b : R
f g : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
x : S ⊗[R] M
⊢ ((a + b) • f).toFun' S x = (a • f + b • f).toFun' S 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
r a b : R
f g : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
x : S ⊗[R] M
⊢ ((a + b) • f).toFun' S x = (a • f + b • f).toFun' S x
Tactic:
simp only [add_def, smul_def, _root_.add_smul]
State after:
no goals