case empty
α : Type ?u.20507
β : Type ?u.20510
R : Type u_1
M : Type u_2
ι : Type ?u.20519
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
x y : M
t : Multiset M
⊢ sum 0 • sum t = sum (map (fun p => p.fst • p.snd) (0 ×ˢ t))

case cons
α : Type ?u.20507
β : Type ?u.20510
R : Type u_1
M : Type u_2
ι : Type ?u.20519
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
t : Multiset M
a : R
s : Multiset R
ih : sum s • sum t = sum (map (fun p => p.fst • p.snd) (s ×ˢ t))
⊢ sum (a ::ₘ s) • sum t = sum (map (fun p => p.fst • p.snd) ((a ::ₘ s) ×ˢ t))
α : Type ?u.20507
β : Type ?u.20510
R : Type u_1
M : Type u_2
ι : Type ?u.20519
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
s : Multiset R
t : Multiset M
⊢ sum s • sum t = sum (map (fun p => p.fst • p.snd) (s ×ˢ t))
induction' s using Multiset.induction with a s ih
no goals
case empty
α : Type ?u.20507
β : Type ?u.20510
R : Type u_1
M : Type u_2
ι : Type ?u.20519
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
x y : M
t : Multiset M
⊢ sum 0 • sum t = sum (map (fun p => p.fst • p.snd) (0 ×ˢ t))
simp
no goals
case cons
α : Type ?u.20507
β : Type ?u.20510
R : Type u_1
M : Type u_2
ι : Type ?u.20519
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
t : Multiset M
a : R
s : Multiset R
ih : sum s • sum t = sum (map (fun p => p.fst • p.snd) (s ×ˢ t))
⊢ sum (a ::ₘ s) • sum t = sum (map (fun p => p.fst • p.snd) ((a ::ₘ s) ×ˢ t))
simp [add_smul, ih, ← Multiset.smul_sum]