no goals
ι : Type u_2
α : Type u_1
β : Type ?u.93370
γ : Type ?u.93373
inst✝ : DivisionCommMonoid α
m : Multiset ι
f g : ι → α
⊢ prod (map (fun i => (f i)⁻¹) m) = (prod (map f m))⁻¹
simp_rw [←(m.map f).prod_map_inv', map_map, Function.comp_apply]