-- 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 ⋯
insert :
  ∀ (m : ↥((Insert.insert a s).sym n)),
    (↑(↑(↑m : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑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)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x_1 : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))),
      x a ^ (↑(x_1.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))) : ℕ) *
          ((↑(↑(↑(x_1.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))) : Sym α (n - (↑x_1.fst : ℕ))) :
                    Multiset α).countPerms :
              R) *
            (Multiset.map x
                  (↑(↑(x_1.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))) : Sym α (n - (↑x_1.fst : ℕ))) :
                    Multiset α)).noncommProd
              ⋯) *
        (↑(n.choose (↑(x_1.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))) : ℕ)) : R))
    (∑ k : ↥((Insert.insert a s).sym n),
      (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯)

Tactic:
refine (Fintype.sum_equiv (symInsertEquiv ha) _ _ fun m => ?_).symm

Premises used: Finset.symInsertEquiv, Fintype.sum_equiv, Eq.symm