awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
refine :
  ∀ (i₁ i₂ : Finset σ),
    i₁ ≠ i₂ →
      Disjoint (α := Finset (σ →₀ ℕ))
        (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ i₁, Finsupp.single i 1) 1))
        (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ i₂, Finsupp.single i 1) 1))
⊢ Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
    (support.{u_6, u_5} (R := R) (∑ x ∈ powersetCard n univ, Finsupp.single (∑ i ∈ x, Finsupp.single i 1) 1))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦
      Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))

Tactic:
refine Finsupp.support_sum_eq_biUnion (powersetCard n (univ : Finset σ)) ?_

Premises used: Finset.univ, Finset.powersetCard, Finsupp.support_sum_eq_biUnion
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
rw :
  ∀ ⦃a : σ →₀ ℕ⦄,
    Membership.mem (γ := Finset (σ →₀ ℕ)) {∑ i ∈ s, Finsupp.single i 1} a →
      a ∉ Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1)
⊢ Disjoint (α := Finset (σ →₀ ℕ)) (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ s, Finsupp.single i 1) 1))
    (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))

Tactic:
rw [disjoint_left, Finsupp.support_single _ one_ne_zero]

Premises used: Finsupp.support_single, Finset.disjoint_left, one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
rw :
  ∀ ⦃a : σ →₀ ℕ⦄,
    Membership.mem (γ := Finset (σ →₀ ℕ)) {∑ i ∈ s, Finsupp.single i 1} a → a ∉ {∑ i ∈ t, Finsupp.single i 1}
⊢ ∀ ⦃a : σ →₀ ℕ⦄,
    Membership.mem (γ := Finset (σ →₀ ℕ)) {∑ i ∈ s, Finsupp.single i 1} a →
      a ∉ Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1)

Tactic:
rw [Finsupp.support_single _ one_ne_zero]

Premises used: Finsupp.support_single, one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
simp : ∀ ⦃a : σ →₀ ℕ⦄, a = ∑ i ∈ s, Finsupp.single i 1 → ¬a = ∑ i ∈ t, Finsupp.single i 1
⊢ ∀ ⦃a : σ →₀ ℕ⦄,
    Membership.mem (γ := Finset (σ →₀ ℕ)) {∑ i ∈ s, Finsupp.single i 1} a → a ∉ {∑ i ∈ t, Finsupp.single i 1}

Tactic:
simp only [mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
h : Eq (α := σ →₀ ℕ) (∑ i ∈ t, Finsupp.single i 1) (∑ i ∈ s, Finsupp.single i 1)
⊢ Eq (α := Finset σ) (Finsupp.support (M := ℕ) (∑ i ∈ t, Finsupp.single i 1))
    (Finsupp.support (M := ℕ) (∑ i ∈ s, Finsupp.single i 1))

Tactic:
have := congr_arg Finsupp.support h
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
h : Eq (α := σ →₀ ℕ) (∑ i ∈ t, Finsupp.single i 1) (∑ i ∈ s, Finsupp.single i 1)
this :
  Eq (α := Finset σ) (Finsupp.support (M := ℕ) (∑ i ∈ t, Finsupp.single i 1))
    (Finsupp.support (M := ℕ) (∑ i ∈ s, Finsupp.single i 1))
⊢ ∀ (i₁ i₂ : σ),
    i₁ ≠ i₂ → Disjoint (Finsupp.support (M := ℕ) (Finsupp.single i₁ 1)) (Finsupp.support (M := ℕ) (Finsupp.single i₂ 1))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
h : Eq (α := σ →₀ ℕ) (∑ i ∈ t, Finsupp.single i 1) (∑ i ∈ s, Finsupp.single i 1)
this :
  Eq (α := Finset σ) (t.biUnion fun (i : σ) ↦ Finsupp.support (M := ℕ) (Finsupp.single i 1))
    (Finsupp.support (M := ℕ) (∑ i ∈ s, Finsupp.single i 1))
⊢ ∀ (i₁ i₂ : σ),
    i₁ ≠ i₂ → Disjoint (Finsupp.support (M := ℕ) (Finsupp.single i₁ 1)) (Finsupp.support (M := ℕ) (Finsupp.single i₂ 1))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
h : Eq (α := σ →₀ ℕ) (∑ i ∈ t, Finsupp.single i 1) (∑ i ∈ s, Finsupp.single i 1)
this :
  Eq (α := Finset σ) (Finsupp.support (M := ℕ) (∑ i ∈ t, Finsupp.single i 1))
    (Finsupp.support (M := ℕ) (∑ i ∈ s, Finsupp.single i 1))
⊢ Eq (α := Finset σ) (t.biUnion fun (i : σ) ↦ Finsupp.support (M := ℕ) (Finsupp.single i 1))
    (s.biUnion fun (i : σ) ↦ Finsupp.support (M := ℕ) (Finsupp.single i 1))

Tactic:
rw [Finsupp.support_sum_eq_biUnion _ (by simp), Finsupp.support_sum_eq_biUnion _ (by simp)]
    at this

Premises used: Finsupp.support_sum_eq_biUnion
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
h : Eq (α := σ →₀ ℕ) (∑ i ∈ t, Finsupp.single i 1) (∑ i ∈ s, Finsupp.single i 1)
this :
  Eq (α := Finset σ) (t.biUnion fun (i : σ) ↦ Finsupp.support (M := ℕ) (Finsupp.single i 1))
    (s.biUnion fun (i : σ) ↦ Finsupp.support (M := ℕ) (Finsupp.single i 1))
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
rw :
  Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦
      Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦ {∑ i ∈ t, Finsupp.single i 1})
⊢ support (esymm σ R n) = Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦ {∑ i ∈ t, Finsupp.single i 1}

Tactic:
rw [support_esymm'']

Premises used: MvPolynomial.support_esymm''
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
e_t :
  Eq.{u_5 + 1} (α := Finset σ → Finset (σ →₀ ℕ))
    (fun (t : Finset σ) ↦ Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))
    fun (t : Finset σ) ↦ {∑ i ∈ t, Finsupp.single i 1}
⊢ Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦
      Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦ {∑ i ∈ t, Finsupp.single i 1})

Tactic:
congr
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
e_t :
  ∀ (x : Finset σ),
    Eq (α := Finset (σ →₀ ℕ)) (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ x, Finsupp.single i 1) 1))
      {∑ i ∈ x, Finsupp.single i 1}
⊢ Eq.{u_5 + 1} (α := Finset σ → Finset (σ →₀ ℕ))
    (fun (t : Finset σ) ↦ Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))
    fun (t : Finset σ) ↦ {∑ i ∈ t, Finsupp.single i 1}

Tactic:
funext
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
x : Finset σ
⊢ Eq (α := Finset (σ →₀ ℕ)) (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ x, Finsupp.single i 1) 1))
    {∑ i ∈ x, Finsupp.single i 1}

Tactic:
Finsupp.support_single _ one_ne_zero

Premises used: Finsupp.support_single, one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
x : Finset σ
⊢ Eq (α := Finset (σ →₀ ℕ)) (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ x, Finsupp.single i 1) 1))
    {∑ i ∈ x, Finsupp.single i 1}

Tactic:
exact Finsupp.support_single _ one_ne_zero

Premises used: Finsupp.support_single, one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
rw :
  Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦ {∑ i ∈ t, Finsupp.single i 1})
    (image (fun (t : Finset σ) ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ))
⊢ support (esymm σ R n) = image (fun (t : Finset σ) ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)

Tactic:
rw [support_esymm']

Premises used: MvPolynomial.support_esymm'
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
⊢ Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦ {∑ i ∈ t, Finsupp.single i 1})
    (image (fun (t : Finset σ) ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ))

Tactic:
biUnion_singleton

Premises used: Finset.biUnion_singleton
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
⊢ Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦ {∑ i ∈ t, Finsupp.single i 1})
    (image (fun (t : Finset σ) ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ))

Tactic:
exact biUnion_singleton

Premises used: Finset.biUnion_singleton
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
h :
  ∀ (x : Finset σ),
    Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ)
        (fun (t : Finset σ) ↦ ∑ i ∈ t, Finsupp.single i 1) x =
      x.val
⊢ Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val

Tactic:
funext
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
x : Finset σ
⊢ Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ)
      (fun (t : Finset σ) ↦ ∑ i ∈ t, Finsupp.single i 1) x =
    x.val

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val

Tactic:
have :
      (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val := by
      funext
      simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
rw : Eq.{u_5 + 1} (α := Multiset σ) (sup (powersetCard n univ) val) (val univ)
⊢ degrees (esymm σ R n) = val univ

Tactic:
rw [degrees_def, support_esymm, sup_image, this]

Premises used: MvPolynomial.degrees_def, Finset.sup_image, MvPolynomial.support_esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
⊢ Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x))
    (sup (powersetCard n univ) val)

Tactic:
comp_sup_eq_sup_comp _ ?_ ?_

Premises used: Finset.comp_sup_eq_sup_comp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
refine_1 : ∀ (x y : Finset σ), (x ⊔ y).val = x.val ⊔ y.val
refine_2 : Eq.{u_5 + 1} (α := Multiset σ) (val ⊥) ⊥
⊢ Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x))
    (sup (powersetCard n univ) val)

Tactic:
refine comp_sup_eq_sup_comp _ ?_ ?_

Premises used: Finset.comp_sup_eq_sup_comp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
⊢ ∀ (x y : Finset σ), (x ⊔ y).val = x.val ⊔ y.val

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
⊢ Eq.{u_5 + 1} (α := Multiset σ) (val ⊥) ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
⊢ Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x))
    (sup (powersetCard n univ) val)

Tactic:
have : ((powersetCard n univ).sup (fun (x : Finset σ) => x)).val
        = sup (powersetCard n univ) val := by
      refine comp_sup_eq_sup_comp _ ?_ ?_ <;> simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this_1 :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
this :
  Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x))
    (sup (powersetCard n univ) val)
rw : Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x)) (val univ)
⊢ Eq.{u_5 + 1} (α := Multiset σ) (sup (powersetCard n univ) val) (val univ)

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this_1 :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
this :
  Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x))
    (sup (powersetCard n univ) val)
obtain :
  ∀ (k : ℕ) (hpos : 0 < k.succ) (hn : k.succ ≤ Fintype.card σ)
    (this :
      Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard k.succ univ) fun (x : Finset σ) ↦ x))
        (sup (powersetCard k.succ univ) val)),
    Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard k.succ univ) fun (x : Finset σ) ↦ x)) (val univ)
⊢ Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x)) (val univ)

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'

Premises used: LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Nontrivial R
this_1 :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
k : ℕ
hpos : 0 < k.succ
hn : k.succ ≤ Fintype.card σ
this :
  Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard k.succ univ) fun (x : Finset σ) ↦ x))
    (sup (powersetCard k.succ univ) val)
⊢ Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard k.succ univ) fun (x : Finset σ) ↦ x)) (val univ)

Tactic:
simpa using powersetCard_sup _ _ (Nat.lt_of_succ_le hn)

Premises used: Nat.lt_of_succ_le, Finset.powersetCard_sup
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ R) (hsymm σ R 0) 1

Tactic:
simp [hsymm, eq_nil_of_card_zero]

Premises used: MvPolynomial.hsymm, Sym.eq_nil_of_card_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
symm : Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (hsymm σ R 1)
⊢ Eq (α := MvPolynomial σ R) (hsymm σ R 1) (∑ i : σ, X i)

Tactic:
symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
h :
  ∀ (x : σ), Eq (α := MvPolynomial σ R) (X x) (prod (Multiset.map X (↑((oneEquiv : (a : σ) → Sym σ 1) x) : Multiset σ)))
⊢ Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (hsymm σ R 1)

Tactic:
apply Fintype.sum_equiv oneEquiv

Premises used: Sym.oneEquiv, Fintype.sum_equiv
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ ∀ (x : σ), Eq (α := MvPolynomial σ R) (X x) (prod (Multiset.map X (↑((oneEquiv : (a : σ) → Sym σ 1) x) : Multiset σ)))

Tactic:
simp only [oneEquiv_apply, Multiset.map_singleton, Multiset.prod_singleton, implies_true]

Premises used: Multiset.map_singleton, Multiset.prod_singleton, Sym.oneEquiv_apply, implies_true
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ R) (hsymmPart σ R (n := 0) (Nat.Partition.indiscrete 0)) 1

Tactic:
simp [hsymmPart]

Premises used: MvPolynomial.hsymmPart
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
n : ℕ
zero : Eq (α := MvPolynomial σ R) (hsymmPart σ R (n := 0) (Nat.Partition.indiscrete 0)) (hsymm σ R 0)
succ :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial σ R) (hsymmPart σ R (n := n + 1) (Nat.Partition.indiscrete (n + 1))) (hsymm σ R (n + 1))
⊢ Eq (α := MvPolynomial σ R) (hsymmPart σ R (Nat.Partition.indiscrete n)) (hsymm σ R n)

Tactic:
cases n
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ R) (hsymmPart σ R (n := 0) (Nat.Partition.indiscrete 0)) (hsymm σ R 0)

Tactic:
simp [hsymmPart]

Premises used: MvPolynomial.hsymmPart
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
n : ℕ
⊢ Eq (α := MvPolynomial σ R) (hsymmPart σ R (n := n + 1) (Nat.Partition.indiscrete (n + 1))) (hsymm σ R (n + 1))

Tactic:
simp [hsymmPart]

Premises used: MvPolynomial.hsymmPart
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Fintype σ
inst_3 : DecidableEq σ
n : ℕ
f : R →+* S
⊢ Eq (α := MvPolynomial σ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (hsymm σ R n) : MvPolynomial σ S)
    (hsymm σ S n : MvPolynomial σ S)

Tactic:
simp [hsymm, ← Multiset.prod_hom']

Premises used: MvPolynomial.hsymm, Multiset.prod_hom'
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
inst_3 : DecidableEq σ
inst_4 : DecidableEq τ
n : ℕ
e : σ ≃ τ
simp_rw :
  Eq (α := MvPolynomial τ R)
    (∑ x : Sym σ n, prod (Multiset.map (fun (x : σ) ↦ X ((e : (a : σ) → τ) x)) (↑x : Multiset σ)))
    (∑ s : Sym τ n, prod (Multiset.map X (↑s : Multiset τ)))
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (hsymm σ R n) : MvPolynomial τ R)
    (hsymm τ R n : MvPolynomial τ R)

Tactic:
simp_rw [hsymm, map_sum, ← prod_hom', rename_X]

Premises used: MvPolynomial.hsymm, map_sum, MvPolynomial.rename_X, Multiset.prod_hom'
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
inst_3 : DecidableEq σ
inst_4 : DecidableEq τ
n : ℕ
e : σ ≃ τ
h :
  ∀ (x : Sym σ n),
    Eq (α := MvPolynomial τ R) (prod (Multiset.map (fun (x : σ) ↦ X ((e : (a : σ) → τ) x)) (↑x : Multiset σ)))
      (prod
        (Multiset.map X
          (↑(((equivCongr e : Equiv.{u_5 + 1, u_2 + 1} (Sym σ n) (Sym τ n)) : (a : Sym σ n) → Sym τ n) x) :
            Multiset τ)))
⊢ Eq (α := MvPolynomial τ R)
    (∑ x : Sym σ n, prod (Multiset.map (fun (x : σ) ↦ X ((e : (a : σ) → τ) x)) (↑x : Multiset σ)))
    (∑ s : Sym τ n, prod (Multiset.map X (↑s : Multiset τ)))

Tactic:
apply Fintype.sum_equiv (equivCongr e)

Premises used: Sym.equivCongr, Fintype.sum_equiv
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
inst_3 : DecidableEq σ
inst_4 : DecidableEq τ
n : ℕ
e : σ ≃ τ
⊢ ∀ (x : Sym σ n),
    Eq (α := MvPolynomial τ R) (prod (Multiset.map (fun (x : σ) ↦ X ((e : (a : σ) → τ) x)) (↑x : Multiset σ)))
      (prod
        (Multiset.map X
          (↑(((equivCongr e : Equiv.{u_5 + 1, u_2 + 1} (Sym σ n) (Sym τ n)) : (a : Sym σ n) → Sym τ n) x) :
            Multiset τ)))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
n : ℕ
⊢ IsSymmetric (hsymm σ R n)

Tactic:
rename_hsymm _ _ n

Premises used: MvPolynomial.IsSymmetric, MvPolynomial.rename_hsymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
⊢ Eq (α := MvPolynomial σ R) (psum σ R 0) (↑(Fintype.card σ) : MvPolynomial σ R)

Tactic:
simp [psum]

Premises used: MvPolynomial.psum
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
⊢ Eq (α := MvPolynomial σ R) (psum σ R 1) (∑ i : σ, X i)

Tactic:
simp [psum]

Premises used: MvPolynomial.psum
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
⊢ Eq (α := MvPolynomial σ R) (psumPart σ R (n := 0) (Nat.Partition.indiscrete 0)) 1

Tactic:
simp [psumPart]

Premises used: MvPolynomial.psumPart