-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(Insert.insert a s) : Set α).Pairwise (Commute on x)
n : ℕ
ih :
  ∀ (n : ℕ),
    s.sum x ^ n =
      ∑ k : ↥(s.sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯
m : ↥((Insert.insert a s).sym n)
insert :
  (↑(n.choose (Multiset.count a (↑(↑m : Sym α n) : Multiset α)) *
            (Multiset.filter (fun (x : α) ↦ a ≠ x) (↑(↑m : Sym α n) : Multiset α)).countPerms) :
        R) *
      (x a ^ (Multiset.replicate (Multiset.count a (↑(↑m : Sym α n) : Multiset α)) (x a)).card *
        (Multiset.map x (Multiset.filter (fun (a_1 : α) ↦ ¬a = a_1) (↑(↑m : Sym α n) : Multiset α))).noncommProd ⋯) =
    x a ^
          (↑(Sigma.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                ((symInsertEquiv ha : (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                  m)) :
            ℕ) *
        ((↑(Multiset.countPerms (α := α)
                ((↑(↑(Sigma.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                            ((symInsertEquiv ha :
                                (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                              m)) :
                        Sym α
                          (n -
                            (↑((symInsertEquiv ha :
                                      (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                                    m).fst :
                              ℕ))) :
                    Multiset α) :
                  Multiset α)) :
            R) *
          (Multiset.map x
                (↑(↑(Sigma.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                          ((symInsertEquiv ha :
                              (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                            m)) :
                      Sym α
                        (n -
                          (↑((symInsertEquiv ha :
                                    (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                                  m).fst :
                            ℕ))) :
                  Multiset α)).noncommProd
            ⋯) *
      (↑(n.choose
            (↑(Sigma.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                  ((symInsertEquiv ha :
                      (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                    m)) :
              ℕ)) :
        R)
⊢ (↑(n.choose (Multiset.count a (↑(↑m : Sym α n) : Multiset α)) *
            (Multiset.filter (fun (x : α) ↦ a ≠ x) (↑(↑m : Sym α n) : Multiset α)).countPerms) :
        R) *
      ((Multiset.replicate (Multiset.count a (↑(↑m : Sym α n) : Multiset α)) (x a)).noncommProd ⋯ *
        (Multiset.map x (Multiset.filter (fun (a_1 : α) ↦ ¬a = a_1) (↑(↑m : Sym α n) : Multiset α))).noncommProd ⋯) =
    x a ^
          (↑(Sigma.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                ((symInsertEquiv ha : (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                  m)) :
            ℕ) *
        ((↑(Multiset.countPerms (α := α)
                ((↑(↑(Sigma.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                            ((symInsertEquiv ha :
                                (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                              m)) :
                        Sym α
                          (n -
                            (↑((symInsertEquiv ha :
                                      (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                                    m).fst :
                              ℕ))) :
                    Multiset α) :
                  Multiset α)) :
            R) *
          (Multiset.map x
                (↑(↑(Sigma.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                          ((symInsertEquiv ha :
                              (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                            m)) :
                      Sym α
                        (n -
                          (↑((symInsertEquiv ha :
                                    (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                                  m).fst :
                            ℕ))) :
                  Multiset α)).noncommProd
            ⋯) *
      (↑(n.choose
            (↑(Sigma.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
                  ((symInsertEquiv ha :
                      (a : ↥((Insert.insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                    m)) :
              ℕ)) :
        R)

Tactic:
rw [Multiset.noncommProd_eq_pow_card _ _ _ fun _ => Multiset.eq_of_mem_replicate]

Premises used: Multiset.noncommProd_eq_pow_card, Multiset.eq_of_mem_replicate