awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
⊢ 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 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) 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
-- 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) ⋯)
⊢ 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 : (↑(cons a s has) : Set α).Pairwise (Commute on f)) (n : ℕ),
  HPow.hPow (α := R) (∑ i ∈ cons a s has, f i) n =
    ∑ k ∈ (cons a s has).piAntidiag n,
      HMul.hMul (α := R) (↑(multinomial (cons a s has) k) : R) ((cons a s has).noncommProd (fun (i : α) ↦ f i ^ k 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
-- 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
hc : (↑∅ : Set α).Pairwise (Commute on x)
⊢ ∀ (n : ℕ),
    Finset.sum ∅ x ^ n =
      ∑ k : ↥(∅.sym n),
        (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯
have empty : ∀ (n : ℕ),
  HPow.hPow (α := R) 0 n =
    ∑ k : ↥(∅.sym n),
      (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd sorry
Tactic: rw [sum_empty]
-- 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
hc : (↑∅ : Set α).Pairwise (Commute on x)
⊢ HPow.hPow (α := R) (β := ℕ) 0 0 =
    ∑ k : ↥(∅.sym 0),
      (↑(↑(↑k : Sym α 0) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α 0) : Multiset α)).noncommProd ⋯
have empty : 1 =
  (↑(Multiset.countPerms.{u_1} (α := α)
          (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 sorry) :
                Sym α 0) :
            Multiset α)) :
      R) *
    (Multiset.map x
          (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 sorry) :
                Sym α 0) :
            Multiset α)).noncommProd
      sorry
Tactic: rw [_root_.pow_zero, Fintype.sum_subsingleton]
-- 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
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
        ⋯
⊢ HPow.hPow (α := R) (β := ℕ) 0 0 =
    ∑ k : ↥(∅.sym 0),
      (↑(↑(↑k : Sym α 0) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α 0) : Multiset α)).noncommProd ⋯
have empty₁ : ↥(Finset.sym ∅ 0)
Tactic: rw [_root_.pow_zero, Fintype.sum_subsingleton]
-- 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
hc : (↑∅ : Set α).Pairwise (Commute on x)
⊢ 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
        ⋯
have 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 sorry) :
              Sym α 0) :
          Multiset α)) :
    R)
  1
Tactic: convert! (@one_mul R _ _).symm
-- 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
hc : (↑∅ : Set α).Pairwise (Commute on x)
⊢ 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
have h : Multiset.countPerms.{u_1} (α := α)
    (↑(↑(Subtype.mk (p := fun (x : Sym α 0) ↦ Membership.mem (γ := Finset (Sym α 0)) (Finset.sym ∅ 0) x) 0 sorry) :
          Sym α 0) :
      Multiset α) =
  1
Tactic: convert! @Nat.cast_one R _
-- 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
hc : (↑∅ : Set α).Pairwise (Commute on x)
n : ℕ
⊢ 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 ⋯
have 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 sorry)
Tactic: rw [_root_.pow_succ, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (hypothesis)
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : Semiring R
x : α → R
hc : (↑∅ : Set α).Pairwise (Commute on x)
n : ℕ
⊢ 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 ⋯)
have this : IsEmpty.{u_1 + 1} ↥(Finset.sym ∅ n.succ)
Tactic: haveI : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty
-- 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
s : Finset α
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 ⋯
have 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 sorry)
  (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 sorry
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 => ?_
Cleared hypotheses: s, hc
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (hypothesis)
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 ⋯
have ih₁ : ∀ (n : ℕ),
  s.sum x ^ n =
    ∑ k : ↥(s.sym n),
      (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd sorry
Tactic: specialize ih (hc.mono <| s.subset_insert a)
Cleared hypotheses: ih
-- 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 ⋯
⊢ (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 ⋯
have 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 a s).sym n),
    (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd sorry)
Tactic: rw [sum_insert ha, (Commute.sum_right s _ _ _).add_pow, sum_range]
-- 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.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 ⋯)
⊢ (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 ⋯
have rw : ∀ i ∈ s, Commute (x a) (x i)
Tactic: rw [sum_insert ha, (Commute.sum_right s _ _ _).add_pow, sum_range]
-- 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 ⋯
⊢ 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 a s).sym n),
      (↑(↑(↑k : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑k : Sym α n) : Multiset α)).noncommProd ⋯)
have 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
            sorry) *
      (↑(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 sorry)
Tactic: simp_rw [ih, mul_sum, sum_mul, sum_sigma', univ_sigma_univ]
-- 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.map x (↑(↑m : Sym α n) : Multiset α)
have 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 α))
Tactic: rw [← m.1.1.filter_add_not (a = ·), Multiset.map_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
f : α → R
n : ℕ
⊢ HPow.hPow (α := R) (∑ i ∈ s, f i) n =
    ∑ k ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s k) : R) (∏ i ∈ s, f i ^ k i)
have simp_rw : HPow.hPow (α := R) (∑ i ∈ s, f i) n =
  ∑ x ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s x) : R) (s.noncommProd (fun (i : α) ↦ f i ^ x i) sorry)
Tactic: simp_rw [← noncommProd_eq_prod]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
f : α → R
n : ℕ
⊢ HPow.hPow (α := R) (∑ i ∈ s, f i) n =
    ∑ x ∈ s.piAntidiag n, HMul.hMul (α := R) (↑(multinomial s x) : R) (s.noncommProd (fun (i : α) ↦ f i ^ x i) ⋯)
have rw : HPow.hPow (α := R) (∑ i ∈ s, f i) n = HPow.hPow (α := R) (∑ i ∈ s, f i) n
Tactic: rw [← sum_pow_eq_sum_piAntidiag_of_commute _ _ fun _ _ _ _ _ ↦ Commute.all ..]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
x : α → R
n : ℕ
| ∑ k ∈ s.sym n, (↑(↑k : Multiset α).countPerms : R) * (Multiset.map x (↑k : Multiset α)).prod
have rw : ∑ i : ↥(s.sym n),
  (↑(↑(↑i : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑i : Sym α n) : Multiset α)).prod
Tactic: rw [← sum_coe_sort]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
x : α → R
n : ℕ
⊢ s.sum x ^ n = ∑ k ∈ s.sym n, (↑(↑k : Multiset α).countPerms : R) * (Multiset.map x (↑k : Multiset α)).prod
have conv_rhs : s.sum x ^ n =
  ∑ i : ↥(s.sym n),
    (↑(↑(↑i : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑i : Sym α n) : Multiset α)).prod
Tactic: conv_rhs => rw [← sum_coe_sort]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
x : α → R
n : ℕ
⊢ s.sum x ^ n =
    ∑ i : ↥(s.sym n),
      (↑(↑(↑i : Sym α n) : Multiset α).countPerms : R) * (Multiset.map x (↑(↑i : Sym α n) : Multiset α)).prod
have h : ∀ (x_1 : ↥(s.sym n)),
  Membership.mem (γ := Finset ↥(s.sym n)) univ x_1 →
    (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).prod =
      (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).noncommProd sorry
Tactic: convert! sum_pow_of_commute x s (fun _ _ _ _ _ ↦ Commute.all ..) n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring R
s : Finset α
x : α → R
n : ℕ
x_1 : ↥(s.sym n)
h : Membership.mem (γ := Finset ↥(s.sym n)) univ x_1
⊢ (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).prod =
    (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).noncommProd ⋯
have h : (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).prod = (Multiset.map x (↑(↑x_1 : Sym α n) : Multiset α)).prod
Tactic: rw [Multiset.noncommProd_eq_prod]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (multinomial s fun (i : ι) ↦ 2 * f i) ≤ HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * multinomial s f
have rw : (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! / ∏ i ∈ s, (2 * f i)! ≤
  HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!
Tactic: rw [multinomial, multinomial, ← mul_sum,
    ← Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum ..)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! / ∏ i ∈ s, (2 * f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!
have refine : (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
  HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!
Tactic: refine Nat.div_le_div_of_mul_le_mul (by positivity)
    ((prod_factorial_dvd_factorial_sum ..).trans (Nat.dvd_mul_left ..)) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
have bc : (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! ≤
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      ∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)!
have rw : (∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i)) * HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
    ∏ i ∈ s, (f i)! =
  HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
    HMul.hMul (α := ℕ) (∏ x ∈ s, HPow.hPow (α := ℕ) 2 (f x)) (∏ x ∈ s, (f x)!)
Tactic: rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! *
      ∏ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!
have bc : ∀ i ∈ s, HPow.hPow (α := ℕ) 2 (f i) * (f i)! ≤ (2 * f i)!
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
i : ι
h : i ∈ s
⊢ HPow.hPow (α := ℕ) 2 (f i) * (f i)! ≤ (2 * f i)!
have bc : (2 * f i)‼ ≤ (2 * f i)!
Tactic: rw [← doubleFactorial_two_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
    HPow.hPow (α := ℕ) (β := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!
have i : (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i))! * ∏ i ∈ s, (f i)! ≤
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℕ) 2 (∑ i ∈ s, f i)) (∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
Tactic: calc
    (2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
      ≤ ((2 * ∑ i ∈ s, f i) ^ (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!) * ∏ i ∈ s, (f i)! := by
      gcongr; exact Nat.factorial_two_mul_le _
    _ = ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)! := by
      rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]; ring
    _ ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)! := by
      gcongr
      rw [← doubleFactorial_two_mul]
      exact doubleFactorial_le_factorial _