prod_multiset_count.lean

import algebra.big_operators

open_locale big_operators
open_locale classical

lemma filter_ne_to_finset {M : Type*} [comm_monoid M] {s : multiset M} {w} (hw : w ∈ s) :
  (multiset.filter (λ (x : M), ¬w = x) s).to_finset = s.to_finset.erase w :=
finset.ext $ λ x, ⟨λ h, finset.mem_erase.2
  ⟨ne.symm (multiset.of_mem_filter (multiset.mem_to_finset.1 h)),
   multiset.mem_to_finset.2 (multiset.filter_subset _ (multiset.mem_to_finset.1 h))⟩,
λ h, multiset.mem_to_finset.2 $ multiset.mem_filter.2
  ⟨multiset.mem_to_finset.1 (finset.mem_erase.1 h).2, ne.symm (finset.mem_erase.1 h).1⟩⟩

lemma finset.prod_multiset_count {M : Type*} [comm_monoid M] (s : multiset M)
  {n : ℕ} (hn : s.to_finset.card = n) :
  s.prod = ∏ m in s.to_finset, m ^ (s.count m) :=
begin
  revert s, induction n with n hn,
    { intros s hs,
      rw [finset.card_eq_zero.1 hs, multiset.to_finset_eq_empty.1 (finset.card_eq_zero.1 hs)],
      simp },
  intros s hs,
  cases finset.card_pos.1 (by rw hs; exact nat.succ_pos _) with w hw,
  rw [←finset.insert_erase hw, finset.prod_insert (finset.not_mem_erase w _)],
  conv_lhs {rw ←@multiset.filter_add_not _ (λ x, w = x) _ s},
  rw multiset.prod_add,
  congr' 1,
  { rw ←multiset.prod_repeat,
    congr,
    exact multiset.eq_repeat.2
      ⟨by rw ←multiset.countp_eq_card_filter; refl,
      λ b hb, eq.symm (multiset.of_mem_filter hb)⟩ },
  rw [hn (multiset.filter (λ x, ¬ w = x) s) (by
      rw [filter_ne_to_finset (multiset.mem_to_finset.1 hw), finset.card_erase_of_mem hw,
      hs, nat.pred_succ]), filter_ne_to_finset (multiset.mem_to_finset.1 hw)],
  exact finset.prod_congr rfl (λ x hx, by
    rw multiset.count_filter (ne.symm (finset.mem_erase.1 hx).1)),
end