awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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
⊢ ∀ ⦃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)
have rw : ∀ ⦃a : σ →₀ ℕ⦄,
  Membership.mem (γ := Finset (σ →₀ ℕ)) {∑ i ∈ s, Finsupp.single i 1} a → a ∉ {∑ i ∈ t, Finsupp.single i 1}
Tactic: rw [Finsupp.support_single _ one_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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
⊢ ∀ ⦃a : σ →₀ ℕ⦄,
    Membership.mem (γ := Finset (σ →₀ ℕ)) {∑ i ∈ s, Finsupp.single i 1} a → a ∉ {∑ i ∈ t, Finsupp.single i 1}
have simp : ∀ ⦃a : σ →₀ ℕ⦄, a = ∑ i ∈ s, Finsupp.single i 1 → ¬a = ∑ i ∈ t, Finsupp.single i 1
Tactic: simp only [mem_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (hypothesis)
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)
⊢ False
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (hypothesis)
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))
⊢ False
have 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))
Tactic: rw [Finsupp.support_sum_eq_biUnion _ (by simp), Finsupp.support_sum_eq_biUnion _ (by simp)]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
⊢ support (esymm σ R n) = Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦ {∑ i ∈ t, Finsupp.single i 1}
have 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})
Tactic: rw [support_esymm'']
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 σ) ↦
      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})
have 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}
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 (σ →₀ ℕ))
    (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}
have 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}
Tactic: funext
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
⊢ support (esymm σ R n) = image (fun (t : Finset σ) ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)
have 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))
Tactic: rw [support_esymm']
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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
have h : ∀ (x : Finset σ),
  Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ)
      (fun (t : Finset σ) ↦ ∑ i ∈ t, Finsupp.single i 1) x =
    x.val
Tactic: funext
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (hypothesis)
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 σ
⊢ degrees (esymm σ R n) = val univ
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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
⊢ degrees (esymm σ R n) = val univ
have rw : Eq.{u_5 + 1} (α := Multiset σ) (sup (powersetCard n univ) val) (val univ)
Tactic: rw [degrees_def, support_esymm, sup_image, this]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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)
have refine_1 : ∀ (x y : Finset σ), (x ⊔ y).val = x.val ⊔ y.val
Tactic: refine comp_sup_eq_sup_comp _ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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
⊢ Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x))
    (sup (powersetCard n univ) val)
have refine_2 : Eq.{u_5 + 1} (α := Multiset σ) (val ⊥) ⊥
Tactic: refine comp_sup_eq_sup_comp _ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (hypothesis)
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 σ) (sup (powersetCard n univ) val) (val univ)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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)
⊢ Eq.{u_5 + 1} (α := Multiset σ) (sup (powersetCard n univ) val) (val univ)
have rw : Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x)) (val univ)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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)
⊢ Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x)) (val univ)
have 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)
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
Cleared hypotheses: n, hpos, hn, this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 σ
⊢ degrees (esymm σ R n) = val univ
have have : Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
  (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
    ∑ i ∈ t, Finsupp.single i 1)
  val
Tactic: classical
    have :
      (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val := by
      funext
      simp
    rw [degrees_def, support_esymm, sup_image, this]
    have : ((powersetCard n univ).sup (fun (x : Finset σ) => x)).val
        = sup (powersetCard n univ) val := by
      refine comp_sup_eq_sup_comp _ ?_ ?_ <;> simp
    rw [← this]
    obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
    simpa using powersetCard_sup _ _ (Nat.lt_of_succ_le hn)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 σ
have :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
⊢ degrees (esymm σ R n) = val univ
have have₁ : ∀
  (this :
    Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
      (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
        ∑ i ∈ t, Finsupp.single i 1)
      val),
  degrees (esymm σ R n) = val univ
Tactic: classical
    have :
      (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val := by
      funext
      simp
    rw [degrees_def, support_esymm, sup_image, this]
    have : ((powersetCard n univ).sup (fun (x : Finset σ) => x)).val
        = sup (powersetCard n univ) val := by
      refine comp_sup_eq_sup_comp _ ?_ ?_ <;> simp
    rw [← this]
    obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
    simpa using powersetCard_sup _ _ (Nat.lt_of_succ_le hn)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 σ
have :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
have₁ :
  ∀
    (this :
      Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
        (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
          ∑ i ∈ t, Finsupp.single i 1)
        val),
    degrees (esymm σ R n) = val univ
have₂ :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
have₃ have₄ :
  ∀
    (this :
      Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
        (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
          ∑ i ∈ t, Finsupp.single i 1)
        val),
    degrees (esymm σ R n) = val univ
⊢ degrees (esymm σ R n) = val univ
have have₅ : ∀
  (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 σ) (sup (powersetCard n univ) val) (val univ)
Tactic: classical
    have :
      (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val := by
      funext
      simp
    rw [degrees_def, support_esymm, sup_image, this]
    have : ((powersetCard n univ).sup (fun (x : Finset σ) => x)).val
        = sup (powersetCard n univ) val := by
      refine comp_sup_eq_sup_comp _ ?_ ?_ <;> simp
    rw [← this]
    obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
    simpa using powersetCard_sup _ _ (Nat.lt_of_succ_le hn)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 σ
have :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
have₁ :
  ∀
    (this :
      Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
        (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
          ∑ i ∈ t, Finsupp.single i 1)
        val),
    degrees (esymm σ R n) = val univ
have₂ :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
have₃ have₄ :
  ∀
    (this :
      Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
        (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
          ∑ i ∈ t, Finsupp.single i 1)
        val),
    degrees (esymm σ R n) = val univ
have₅ :
  ∀
    (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 σ) (sup (powersetCard n univ) val) (val univ)
⊢ degrees (esymm σ R n) = val univ
have have₆ : ∀
  (this :
    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)),
  Eq.{u_5 + 1} (α := Multiset σ) (sup (powersetCard n univ) val) (val univ)
Tactic: classical
    have :
      (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val := by
      funext
      simp
    rw [degrees_def, support_esymm, sup_image, this]
    have : ((powersetCard n univ).sup (fun (x : Finset σ) => x)).val
        = sup (powersetCard n univ) val := by
      refine comp_sup_eq_sup_comp _ ?_ ?_ <;> simp
    rw [← this]
    obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
    simpa using powersetCard_sup _ _ (Nat.lt_of_succ_le hn)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 σ
have :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
have₁ :
  ∀
    (this :
      Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
        (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
          ∑ i ∈ t, Finsupp.single i 1)
        val),
    degrees (esymm σ R n) = val univ
have₂ :
  Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
    (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
      ∑ i ∈ t, Finsupp.single i 1)
    val
have₃ have₄ :
  ∀
    (this :
      Eq.{u_5 + 1} (α := Finset σ → Multiset σ)
        (Function.comp (β := σ →₀ ℕ) (⇑Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) fun (t : Finset σ) ↦
          ∑ i ∈ t, Finsupp.single i 1)
        val),
    degrees (esymm σ R n) = val univ
have₅ :
  ∀
    (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 σ) (sup (powersetCard n univ) val) (val univ)
have₆ :
  ∀
    (this :
      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)),
    Eq.{u_5 + 1} (α := Multiset σ) (sup (powersetCard n univ) val) (val univ)
⊢ degrees (esymm σ R n) = val univ
have have₇ : ∀
  (this :
    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)),
  Eq.{u_5 + 1} (α := Multiset σ) (val (sup (powersetCard n univ) fun (x : Finset σ) ↦ x)) (val univ)
Tactic: classical
    have :
      (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val := by
      funext
      simp
    rw [degrees_def, support_esymm, sup_image, this]
    have : ((powersetCard n univ).sup (fun (x : Finset σ) => x)).val
        = sup (powersetCard n univ) val := by
      refine comp_sup_eq_sup_comp _ ?_ ?_ <;> simp
    rw [← this]
    obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
    simpa using powersetCard_sup _ _ (Nat.lt_of_succ_le hn)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ R) (hsymm σ R 1) (∑ i : σ, X i)
have symm : Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (hsymm σ R 1)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (hsymm σ R 1)
have h : ∀ (x : σ), Eq (α := MvPolynomial σ R) (X x) (prod (Multiset.map X (↑((oneEquiv : (a : σ) → Sym σ 1) x) : Multiset σ)))
Tactic: apply Fintype.sum_equiv oneEquiv
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
n : ℕ
⊢ Eq (α := MvPolynomial σ R) (hsymmPart σ R (Nat.Partition.indiscrete n)) (hsymm σ R n)
have zero : Eq (α := MvPolynomial σ R) (hsymmPart σ R (n := 0) (Nat.Partition.indiscrete 0)) (hsymm σ R 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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)
⊢ Eq (α := MvPolynomial σ R) (hsymmPart σ R (Nat.Partition.indiscrete n)) (hsymm σ R n)
have succ : ∀ (n : ℕ),
  Eq (α := MvPolynomial σ R) (hsymmPart σ R (n := n + 1) (Nat.Partition.indiscrete (n + 1))) (hsymm σ R (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 : σ ≃ τ
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (hsymm σ R n) : MvPolynomial τ R)
    (hsymm τ R n : MvPolynomial τ R)
have 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 τ)))
Tactic: simp_rw [hsymm, map_sum, ← prod_hom', rename_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 : σ ≃ τ
⊢ 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 τ)))
have 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 τ)))
Tactic: apply Fintype.sum_equiv (equivCongr e)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (psum σ R n) : MvPolynomial τ R)
    (psum τ R n : MvPolynomial τ R)
have simp_rw : Eq (α := MvPolynomial τ R)
  ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
    (∑ i : σ, HPow.hPow (α := MvPolynomial σ R) (X i) n))
  (∑ i : τ, HPow.hPow (α := MvPolynomial τ R) (X i) n)
Tactic: simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]