-- 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 σ
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)
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)
have₈ :
  ∀
    (this :
      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)
⊢ 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)

Premises used: MvPolynomial.degrees_def, LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, Finset.sup_image, MvPolynomial.support_esymm, rfl