[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
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))
[PROOFSTEP]
induction' s using Multiset.induction with a s ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
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))
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
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))
[PROOFSTEP]
simp [add_smul, ih, ← Multiset.smul_sum]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
⊢ (∑ i in s, f i) • ∑ i in t, g i = ∑ p in s ×ˢ t, f p.fst • g p.snd
[PROOFSTEP]
rw [Finset.sum_product, Finset.sum_smul, Finset.sum_congr rfl]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
⊢ ∀ (x : α), x ∈ s → f x • ∑ i in t, g i = ∑ y in t, f (x, y).fst • g (x, y).snd
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
x✝ : α
a✝ : x✝ ∈ s
⊢ f x✝ • ∑ i in t, g i = ∑ y in t, f (x✝, y).fst • g (x✝, y).snd
[PROOFSTEP]
rw [Finset.smul_sum]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝ : CommSemiring R
s : Finset α
⊢ ↑(card s) = ∑ a in s, 1
[PROOFSTEP]
rw [Finset.sum_const, Nat.smul_one_eq_coe]
