Theorem: Multiset.prod_toFinset (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
m : Multiset α
hm : Nodup m
⊢ Finset.prod (toFinset m) f = prod (map f m)
Tactic:
induction' m using Multiset.induction with a m ih
State after:
case empty
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
hm : Nodup 0
⊢ Finset.prod (toFinset 0) f = prod (map f 0)

case cons
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm : Nodup (a ::ₘ m)
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))

State before:
case empty
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
hm : Nodup 0
⊢ Finset.prod (toFinset 0) f = prod (map f 0)

case cons
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm : Nodup (a ::ₘ m)
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))
Tactic:
simp
State after:
case cons
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm : Nodup (a ::ₘ m)
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))

State before:
case cons
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm : Nodup (a ::ₘ m)
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))
Tactic:
obtain ⟨not_mem, hm⟩ := Multiset.nodup_cons.mp hm
State after:
case cons.intro
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm✝ : Nodup (a ::ₘ m)
not_mem : a ∉ m
hm : Nodup m
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))

State before:
case cons.intro
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm✝ : Nodup (a ::ₘ m)
not_mem : a ∉ m
hm : Nodup m
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))
Tactic:
simp [Finset.prod_insert (mt Multiset.mem_toFinset.mp not_mem), ih hm]
State after:
no goals