-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(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 a s).sym n)
⊢ (↑(Multiset.filter (fun (x : α) ↦ a ≠ x) (↑(↑m : Sym α n) : Multiset α)).countPerms : R) *
      (x a ^ Multiset.count a (↑(↑m : Sym α n) : Multiset α) *
        (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 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 a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                            m)) :
                      Sym α
                        (n -
                          (↑((symInsertEquiv ha :
                                    (a : ↥((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 a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                          m)) :
                    Sym α
                      (n -
                        (↑((symInsertEquiv ha :
                                  (a : ↥((insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                                m).fst :
                          ℕ))) :
                Multiset α)).noncommProd
          ⋯)
have insert : x a ^ Multiset.count a (↑(↑m : Sym α n) : Multiset α) *
      (↑(Multiset.filter (fun (x : α) ↦ a ≠ x) (↑(↑m : Sym α n) : Multiset α)).countPerms : R) *
    (Multiset.map x (Multiset.filter (fun (a_1 : α) ↦ ¬a = a_1) (↑(↑m : Sym α n) : Multiset α))).noncommProd sorry =
  x a ^
        (↑(Sigma.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
              ((symInsertEquiv ha : (a : ↥((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 a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                          m)) :
                    Sym α
                      (n -
                        (↑((symInsertEquiv ha :
                                  (a : ↥((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 a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                      m)) :
                Sym α
                  (n -
                    (↑((symInsertEquiv ha : (a : ↥((insert a s).sym n)) → (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
                            m).fst :
                      ℕ))) :
            Multiset α)).noncommProd
      sorry
Tactic: simp_rw [← mul_assoc, Nat.cast_comm]