case empty
ι✝ : Type ?u.943028
β : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
ι : Type u_2
inst✝ : CommMonoid α
f : ι → Multiset α
⊢ prod (∑ x in ∅, f x) = ∏ x in ∅, prod (f x)

case insert
ι✝ : Type ?u.943028
β : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a✝ : α✝
f✝ g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
ι : Type u_2
inst✝ : CommMonoid α
f : ι → Multiset α
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : prod (∑ x in t, f x) = ∏ x in t, prod (f x)
⊢ prod (∑ x in insert a t, f x) = ∏ x in insert a t, prod (f x)
ι✝ : Type ?u.943028
β : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
ι : Type u_2
inst✝ : CommMonoid α
f : ι → Multiset α
s : Finset ι
⊢ prod (∑ x in s, f x) = ∏ x in s, prod (f x)
induction' s using Finset.induction_on with a t hat ih
no goals
case empty
ι✝ : Type ?u.943028
β : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
ι : Type u_2
inst✝ : CommMonoid α
f : ι → Multiset α
⊢ prod (∑ x in ∅, f x) = ∏ x in ∅, prod (f x)
rw [Finset.sum_empty, Finset.prod_empty, Multiset.prod_zero]
no goals
case insert
ι✝ : Type ?u.943028
β : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a✝ : α✝
f✝ g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
ι : Type u_2
inst✝ : CommMonoid α
f : ι → Multiset α
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : prod (∑ x in t, f x) = ∏ x in t, prod (f x)
⊢ prod (∑ x in insert a t, f x) = ∏ x in insert a t, prod (f x)
rw [Finset.sum_insert hat, Finset.prod_insert hat, Multiset.prod_add, ih]