awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
cons : Eq.{u_2 + 1} (α := R) (↑((p.1 + p.2).choose p.1) : R) (↑(n.choose p.1) : R)
cons₁ :
  Eq.{u_2 + 1} (α := R) (↑(multinomial s (f + fun (i : α) ↦ if i = a then p.1 else 0)) : R) (↑(multinomial s f) : R)
cons₂ :
  Eq.{u_2 + 1} (α := R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ (f i + if i = a then p.1 else 0)) ⋯)
    (s.noncommProd (fun (i : α) ↦ f_1 i ^ f i) ⋯)
⊢ HMul.hMul (α := R) (↑((p.1 + p.2).choose p.1) : R)
        (↑(multinomial s (f + fun (i : α) ↦ if i = a then p.1 else 0)) : R) *
      (f_1 a ^ p.1 * s.noncommProd (fun (i : α) ↦ f_1 i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    HMul.hMul (α := R) (↑(n.choose p.1) : R) (↑(multinomial s f) : R) *
      (f_1 a ^ p.1 * s.noncommProd (fun (i : α) ↦ f_1 i ^ f i) ⋯)

Tactic:
congr 2
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
cons cons₁ : Eq.{u_2 + 1} (α := R) (↑(n.choose p.1) : R) (↑(n.choose p.1) : R)
⊢ Eq.{u_2 + 1} (α := R) (↑((p.1 + p.2).choose p.1) : R) (↑(n.choose p.1) : R)

Tactic:
rw [mem_antidiagonal.1 hp]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
cons : ∀ a_1 ∈ s, HAdd.hAdd (β := (i : α) → ℕ) f (fun (i : α) ↦ if i = a then p.1 else 0) a_1 = f a_1
⊢ Eq.{u_2 + 1} (α := R) (↑(multinomial s (f + fun (i : α) ↦ if i = a then p.1 else 0)) : R) (↑(multinomial s f) : R)

Tactic:
rw [multinomial_congr]

Premises used: Nat.multinomial_congr
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
t : α
ht : t ∈ s
cons : ¬t = a
⊢ HAdd.hAdd (β := (i : α) → ℕ) f (fun (i : α) ↦ if i = a then p.1 else 0) t = f t

Tactic:
rw [Pi.add_apply, if_neg, add_zero]

Premises used: Pi.add_apply, add_zero, if_neg
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
t : α
ht : t ∈ s
⊢ ¬t = a

Tactic:
ne_of_mem_of_not_mem ht has

Premises used: ne_of_mem_of_not_mem
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
t : α
ht : t ∈ s
⊢ ¬t = a

Tactic:
exact ne_of_mem_of_not_mem ht has

Premises used: ne_of_mem_of_not_mem
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ Eq.{u_2 + 1} (α := R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ (f i + if i = a then p.1 else 0)) ⋯)
    (s.noncommProd (fun (i : α) ↦ f_1 i ^ f i) ⋯)

Tactic:
noncommProd_congr rfl (fun t ht ↦ ?_) _

Premises used: Finset.noncommProd_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
cons : ∀ (t : α) (ht : t ∈ s), f_1 t ^ (f t + if t = a then p.1 else 0) = f_1 t ^ f t
⊢ Eq.{u_2 + 1} (α := R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ (f i + if i = a then p.1 else 0)) ⋯)
    (s.noncommProd (fun (i : α) ↦ f_1 i ^ f i) ⋯)

Tactic:
refine noncommProd_congr rfl (fun t ht ↦ ?_) _

Premises used: Finset.noncommProd_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
f_1 : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on f_1)) (n : ℕ),
    HPow.hPow (α := R) (∑ i ∈ s, f_1 i) n =
      ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (s.noncommProd (fun (i : α) ↦ f_1 i ^ k i) ⋯)
hc : (↑(Finset.cons a s has) : Set α).Pairwise (Commute on f_1)
n : ℕ
p : ℕ × ℕ
hp : p ∈ @antidiagonal _ instAddMonoid _ n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
t : α
ht : t ∈ s
cons : ¬t = a
⊢ f_1 t ^ (f t + if t = a then p.1 else 0) = f_1 t ^ f t

Tactic:
rw [if_neg, add_zero]

Premises used: add_zero, if_neg
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
empty :
  ∀ (n : ℕ),
    HPow.hPow (α := R) 0 n =
      ∑ k : ↥(∅.sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯
⊢ ∀ (n : ℕ),
    Finset.sum ∅ x ^ n =
      ∑ k : ↥(∅.sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯

Tactic:
rw [sum_empty]

Premises used: Finset.sum_empty
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
empty :
  1 =
    (↑(Multiset.countPerms.{u_1} (α := α)
            (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 ⋯) :
                  Sym α 0) :
              Multiset α)) :
        R) *
      (Multiset.map x
            (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 ⋯) :
                  Sym α 0) :
              Multiset α)).noncommProd
        ⋯
empty₁ : ↥(Finset.sym ∅ 0)
⊢ HPow.hPow (α := R) (β := ℕ) 0 0 =
    ∑ k : ↥(∅.sym 0),
      (↑(↑(↑k : Sym α 0) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α 0) : Multiset α)).noncommProd ⋯

Tactic:
rw [_root_.pow_zero, Fintype.sum_subsingleton]

Premises used: pow_zero, Fintype.sum_subsingleton
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
⊢ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
⊢ ↥(Finset.sym ∅ 0)

Tactic:
exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
⊢ 1 = HMul.hMul (α := R) 1 1

Tactic:
(@one_mul R _ _).symm

Premises used: Eq.symm, one_mul
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
h :
  Eq.{u_2 + 1} (α := R)
    (↑(Multiset.countPerms.{u_1} (α := α)
          (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 ⋯) :
                Sym α 0) :
            Multiset α)) :
      R)
    1
⊢ 1 =
    (↑(Multiset.countPerms.{u_1} (α := α)
            (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 ⋯) :
                  Sym α 0) :
              Multiset α)) :
        R) *
      (Multiset.map x
            (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 ⋯) :
                  Sym α 0) :
              Multiset α)).noncommProd
        ⋯

Tactic:
convert! (@one_mul R _ _).symm

Premises used: Eq.symm, one_mul
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
⊢ Eq.{u_2 + 1} (α := R) (↑1 : R) 1

Tactic:
@Nat.cast_one R _

Premises used: Nat.cast_one
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
h :
  Multiset.countPerms.{u_1} (α := α)
      (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 ⋯) :
            Sym α 0) :
        Multiset α) =
    1
⊢ Eq.{u_2 + 1} (α := R)
    (↑(Multiset.countPerms.{u_1} (α := α)
          (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 ⋯) :
                Sym α 0) :
            Multiset α)) :
      R)
    1

Tactic:
convert! @Nat.cast_one R _

Premises used: Nat.cast_one
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
⊢ Multiset.countPerms.{u_1} (α := α)
      (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 ⋯) :
            Sym α 0) :
        Multiset α) =
    1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
n : ℕ
empty :
  Eq.{u_2 + 1} (α := R) 0
    (∑ k : ↥(∅.sym (n + 1)),
      (↑(↑(↑k : Sym α (n + 1)) : Multiset α).countPerms : R) *
        (Multiset.map x (↑(↑k : Sym α (n + 1)) : Multiset α)).noncommProd ⋯)
⊢ HPow.hPow (α := R) 0 (n + 1) =
    ∑ k : ↥(∅.sym (n + 1)),
      (↑(↑(↑k : Sym α (n + 1)) : Multiset α).countPerms : R) *
        (Multiset.map x (↑(↑k : Sym α (n + 1)) : Multiset α)).noncommProd ⋯

Tactic:
rw [_root_.pow_succ, mul_zero]

Premises used: pow_succ, MulZeroClass.mul_zero
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
n : ℕ
⊢ IsEmpty.{u_1 + 1} ↥(Finset.sym ∅ n.succ)

Tactic:
haveI : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
n : ℕ
this : IsEmpty.{u_1 + 1} ↥(Finset.sym ∅ n.succ)
⊢ Eq.{u_2 + 1} (α := R) 0
    (∑ k : ↥(∅.sym (n + 1)),
      (↑(↑(↑k : Sym α (n + 1)) : Multiset α).countPerms : R) *
        (Multiset.map x (↑(↑k : Sym α (n + 1)) : Multiset α)).noncommProd ⋯)

Tactic:
apply (Fintype.sum_empty _).symm

Premises used: Fintype.sum_empty, Eq.symm
-- 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
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on x)) (n : ℕ),
    s.sum x ^ n =
      ∑ k : ↥(s.sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯
hc : (↑(insert a s) : Set α).Pairwise (Commute on x)
⊢ ∀ (n : ℕ),
    (insert a s).sum x ^ n =
      ∑ k : ↥((insert a s).sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯

Tactic:
?_
-- Module: Mathlib.Data.Nat.Choose.Multinomial
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
s : Finset α
hc : (↑s : Set α).Pairwise (Commute on x)
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s)
    (ih :
      ∀ (hc : (↑s : Set α).Pairwise (Commute on x)) (n : ℕ),
        s.sum x ^ n =
          ∑ k : ↥(s.sym n),
            (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) *
              (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯)
    (hc : (↑(Insert.insert a s) : Set α).Pairwise (Commute on x)) (n : ℕ),
    (Insert.insert a s).sum x ^ n =
      ∑ k : ↥((Insert.insert a s).sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯
⊢ ∀ (n : ℕ),
    s.sum x ^ n =
      ∑ k : ↥(s.sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯

Tactic:
induction s using Finset.induction with
  | empty =>
    rw [sum_empty]
    rintro (_ | n)
    · rw [_root_.pow_zero, Fintype.sum_subsingleton]
      swap
      · exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩
      convert! (@one_mul R _ _).symm
      convert! @Nat.cast_one R _
      simp
    · rw [_root_.pow_succ, mul_zero]
      haveI : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty
      apply (Fintype.sum_empty _).symm
  | insert a s ha ih => ?_

Premises used: Fintype.sum_empty, pow_succ, Insert.insert, pow_zero, MulZeroClass.mul_zero, Finset.sum_empty, Fintype.sum_subsingleton, Eq.symm, Nat.cast_one, one_mul
-- 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
ih :
  ∀ (hc : (↑s : Set α).Pairwise (Commute on x)) (n : ℕ),
    s.sum x ^ n =
      ∑ k : ↥(s.sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯
hc : (↑(insert a s) : Set α).Pairwise (Commute on x)
n : ℕ
⊢ ∀ (n : ℕ),
    s.sum x ^ n =
      ∑ k : ↥(s.sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯

Tactic:
specialize ih (hc.mono <| s.subset_insert a)

Premises used: Set.Pairwise.mono, Finset.subset_insert
-- 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 :
  Eq.{u_2 + 1} (α := R)
    (∑ i : Fin (n + 1), x a ^ (↑i : ℕ) * HPow.hPow (α := R) (∑ i ∈ s, x i) (n - (↑i : ℕ)) * (↑(n.choose (↑i : ℕ)) : R))
    (∑ k : ↥((Insert.insert a s).sym n),
      (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯)
rw : ∀ i ∈ s, Commute (x a) (x i)
⊢ (Insert.insert a s).sum x ^ n =
    ∑ k : ↥((Insert.insert a s).sym n),
      (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯

Tactic:
rw [sum_insert ha, (Commute.sum_right s _ _ _).add_pow, sum_range]

Premises used: Commute.add_pow, Finset.sum_range, Commute.sum_right, Finset.sum_insert
-- 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 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 ⋯
⊢ ∀ i ∈ s, Commute (x a) (x i)

Tactic:
fun _ hb => hc (mem_insert_self a s) (mem_insert_of_mem hb)
      (ne_of_mem_of_not_mem hb ha).symm

Premises used: Finset.mem_insert_self, Ne.symm, ne_of_mem_of_not_mem, Finset.mem_insert_of_mem
-- 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 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 ⋯
⊢ ∀ i ∈ s, Commute (x a) (x i)

Tactic:
exact fun _ hb => hc (mem_insert_self a s) (mem_insert_of_mem hb)
      (ne_of_mem_of_not_mem hb ha).symm

Premises used: Finset.mem_insert_self, Ne.symm, ne_of_mem_of_not_mem, Finset.mem_insert_of_mem
-- 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 :
  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 ⋯)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ i : Fin (n + 1), x a ^ (↑i : ℕ) * HPow.hPow (α := R) (∑ i ∈ s, x i) (n - (↑i : ℕ)) * (↑(n.choose (↑i : ℕ)) : R))
    (∑ k : ↥((Insert.insert a s).sym n),
      (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯)

Tactic:
simp_rw [ih, mul_sum, sum_mul, sum_sigma', univ_sigma_univ]

Premises used: Finset.mul_sum, Finset.univ_sigma_univ, Finset.sum_sigma', Finset.sum_mul
-- 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 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 ⋯
⊢ 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 a s).sym n),
      (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯)

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

Premises used: Finset.symInsertEquiv, Fintype.sum_equiv, Eq.symm
-- 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 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)
rw :
  Multiset.map x (Multiset.filter (fun (x : α) ↦ a = x) (↑(↑m : Sym α n) : Multiset α)) +
    Multiset.map x (Multiset.filter (fun (a_1 : α) ↦ ¬a = a_1) (↑(↑m : Sym α n) : Multiset α))
| Multiset.map x (↑(↑m : Sym α n) : Multiset α)

Tactic:
rw [← m.1.1.filter_add_not (a = ·), Multiset.map_add]

Premises used: Multiset.filter_add_not, Subtype.val, Multiset.map_add, Eq