α : Type u_2
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_1
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x in toEnumFinset m, f x.fst x.snd = ∏ x : { x // x ∈ toEnumFinset m }, f (↑x).fst (↑x).snd

α : Type u_2
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_1
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∀ (x : ToType m), f x.fst ↑x.snd = f (↑(↑(coeEquiv m) x)).fst (↑(↑(coeEquiv m) x)).snd
α : Type u_2
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_1
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x in toEnumFinset m, f x.fst x.snd = ∏ x : ToType m, f x.fst ↑x.snd
rw [Fintype.prod_equiv m.coeEquiv (fun x ↦ f x x.2) fun x ↦ f x.1.1 x.1.2]
no goals
α : Type u_2
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_1
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x in toEnumFinset m, f x.fst x.snd = ∏ x : { x // x ∈ toEnumFinset m }, f (↑x).fst (↑x).snd
rw [← m.toEnumFinset.prod_coe_sort fun x ↦ f x.1 x.2]
α : Type u_2
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_1
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
x : ToType m
⊢ f x.fst ↑x.snd = f (↑(↑(coeEquiv m) x)).fst (↑(↑(coeEquiv m) x)).snd
α : Type u_2
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_1
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∀ (x : ToType m), f x.fst ↑x.snd = f (↑(↑(coeEquiv m) x)).fst (↑(↑(coeEquiv m) x)).snd
intro x
no goals
α : Type u_2
inst✝¹ : DecidableEq α
m✝ : Multiset α
β : Type u_1
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
x : ToType m
⊢ f x.fst ↑x.snd = f (↑(↑(coeEquiv m) x)).fst (↑(↑(coeEquiv m) x)).snd
rfl