-- 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
s : Finset α
f : α → R
hc : (↑s : Set α).Pairwise (Commute on f)
n : ℕ
empty :
  ∀ (hc : (↑∅ : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ ∅, f i) n =
      ∑ k ∈ piAntidiag ∅ n, HMul.hMul (α := R) (↑(multinomial ∅ k) : R) (noncommProd ∅ (fun (i : α) ↦ f i ^ k i) ⋯)
cons cons₁ :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (ih :
      ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
        HPow.hPow (α := R) (∑ i ∈ s, f i) n =
          ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯))
    (hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ Finset.cons a s has, f i) n =
      ∑ k ∈ (Finset.cons a s has).piAntidiag n,
        HMul.hMul (α := R) (↑(multinomial (Finset.cons a s has) k) : R)
          ((Finset.cons a s has).noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
cons₂ :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (ih :
      ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
        HPow.hPow (α := R) (∑ i ∈ s, f i) n =
          ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯))
    (hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f)) (n : ℕ),
    (f a + ∑ x ∈ s, f x) ^ n =
      ∑ i ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
        ∑ x ∈ map (addRightEmbedding fun (t : α) ↦ if t = a then i.1 else 0) (s.piAntidiag i.2),
          HMul.hMul (α := R) (↑(multinomial (Finset.cons a s has) x) : R)
            ((Finset.cons a s has).noncommProd (fun (i : α) ↦ f i ^ x i) ⋯)
cons₃ :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (ih :
      ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
        HPow.hPow (α := R) (∑ i ∈ s, f i) n =
          ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯))
    (hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f)) (n : ℕ),
    (f a + ∑ x ∈ s, f x) ^ n =
      ∑ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
        ∑ x_1 ∈ s.piAntidiag x.2,
          HMul.hMul (α := R) (↑((x_1 a + x.1 + ∑ x ∈ s, x_1 x).choose (x_1 a + x.1)) : R)
              (↑(multinomial s (x_1 + fun (t : α) ↦ if t = a then x.1 else 0)) : R) *
            (f a ^ (x_1 a + x.1) * s.noncommProd (fun (x_2 : α) ↦ f x_2 ^ (x_1 x_2 + if x_2 = a then x.1 else 0)) ⋯)
cons₄ :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (ih :
      ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
        HPow.hPow (α := R) (∑ i ∈ s, f i) n =
          ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯))
    (hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f)) (n : ℕ),
    ∀ p ∈ @antidiagonal _ instAddMonoid _ n,
      Eq.{u_2 + 1} (α := R)
        (∑ g ∈ s.piAntidiag p.2,
          HMul.hMul (α := R) (↑((g a + p.1 + s.sum g).choose (g a + p.1)) : R)
              (↑(multinomial s (g + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
            (f a ^ (g a + p.1) * s.noncommProd (fun (i : α) ↦ f i ^ (g i + if i = a then p.1 else 0)) ⋯))
        (∑ g ∈ s.piAntidiag p.2,
          HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s g) : R) *
            (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ g i) ⋯))
⊢ HPow.hPow (α := R) (∑ i ∈ s, f i) n =
    ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) ⋯)
have cons₅ : ∀ (a : α) (s : Finset α) (has : a ∉ s)
  (ih :
    ∀ (hc : (↑s : Set α).Pairwise (Commute on f)) (n : ℕ),
      HPow.hPow (α := R) (∑ i ∈ s, f i) n =
        ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f i ^ k i) sorry))
  (hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f)) (n : ℕ) (p : ℕ × ℕ)
  (hp : p ∈ @antidiagonal _ instAddMonoid _ n) (f_1 : α → ℕ) (hf : f_1 ∈ s.piAntidiag p.2),
  HMul.hMul (α := R) (↑((f_1 a + p.1 + s.sum f_1).choose (f_1 a + p.1)) : R)
        (↑(multinomial s (f_1 + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
      (f a ^ (f_1 a + p.1) * s.noncommProd (fun (i : α) ↦ f i ^ (f_1 i + if i = a then p.1 else 0)) sorry) =
    HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s f_1) : R) *
      (f a ^ p.1 * s.noncommProd (fun (i : α) ↦ f i ^ f_1 i) sorry)
Tactic: classical
  induction s using Finset.cons_induction generalizing n with
  | empty => cases n <;> simp
  | cons a s has ih => ?_
  rw [Finset.sum_cons, piAntidiag_cons, sum_disjiUnion]
  simp only [sum_map, Pi.add_apply, multinomial_cons,
    Pi.add_apply, if_true, Nat.cast_mul, noncommProd_cons,
    if_true, sum_add_distrib, sum_ite_eq', has, if_false, add_zero,
    addRightEmbedding_apply]
  suffices ∀ p : ℕ × ℕ, p ∈ antidiagonal n →
    ∑ g ∈ piAntidiag s p.2, ((g a + p.1 + s.sum g).choose (g a + p.1) : R) *
      multinomial s (g + fun i ↦ ite (i = a) p.1 0) *
        (f a ^ (g a + p.1) * s.noncommProd (fun i ↦ f i ^ (g i + ite (i = a) p.1 0))
          ((hc.mono (by simp)).mono' fun i j h ↦ h.pow_pow ..)) =
      ∑ g ∈ piAntidiag s p.2, n.choose p.1 * multinomial s g * (f a ^ p.1 *
        s.noncommProd (fun i ↦ f i ^ g i) ((hc.mono (by simp)).mono' fun i j h ↦ h.pow_pow ..)) by
    rw [sum_congr rfl this]
    simp only [Nat.antidiagonal_eq_map, sum_map, Function.Embedding.coeFn_mk]
    rw [(Commute.sum_right _ _ _ fun i hi ↦ hc (by simp) (by simp [hi])
      (by simpa [eq_comm] using ne_of_mem_of_not_mem hi has)).add_pow]
    simp only [ih (hc.mono (by simp)), sum_mul, mul_sum]
    refine sum_congr rfl fun i _ ↦ sum_congr rfl fun g _ ↦ ?_
    rw [← Nat.cast_comm, (Nat.commute_cast (f a ^ i) _).left_comm, mul_assoc]
  refine fun p hp ↦ sum_congr rfl fun f hf ↦ ?_
  rw [mem_piAntidiag] at hf
  rw [not_imp_comm.1 (hf.2 _) has, zero_add, hf.1]
  congr 2
  · rw [mem_antidiagonal.1 hp]
  · rw [multinomial_congr]
    intro t ht
    rw [Pi.add_apply, if_neg, add_zero]
    exact ne_of_mem_of_not_mem ht has
  refine noncommProd_congr rfl (fun t ht ↦ ?_) _
  rw [if_neg, add_zero]
  exact ne_of_mem_of_not_mem ht has
Cleared hypotheses: s, hc, n