-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem degrees_esymm [Nontrivial R] {n : ℕ} (hpos : 0 < n) (hn : n ≤ Fintype.card σ) :
    (esymm σ R n).degrees = (univ : Finset σ).val

Proof state:
case refine_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
⊢ ⊥.val = ⊥

Tactic:
rfl

Result:
no goals

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val

Tactic:
funext

Result:
case h
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
x✝ : Finset σ
⊢ (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) x✝ = x✝.val

Proof state:
case refine_1
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ (x✝ ⊔ y✝).val = x✝.val ⊔ y✝.val

Tactic:
simp only [union_val, sup_eq_union]

Result:
case refine_1
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ x✝.val ∪ y✝.val = x✝.val ⊔ y✝.val

Proof state:
case intro
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
this✝ : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
k : ℕ
hpos : 0 < k.succ
hn : k.succ ≤ Fintype.card σ
this : ((powersetCard k.succ univ).sup fun x => x).val = (powersetCard k.succ univ).sup val
⊢ ((powersetCard k.succ univ).sup fun x => x).val = univ.val

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

Result:
no goals

Proof state:
case refine_1
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ x✝.val ∪ y✝.val = x✝.val ⊔ y✝.val

Tactic:
congr

Result:
no goals

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
⊢ ((powersetCard n univ).sup fun x => x).val = (powersetCard n univ).sup val

Tactic:
refine comp_sup_eq_sup_comp _ ?_ ?_

Result:
case refine_1
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
⊢ ∀ (x y : Finset σ), (x ⊔ y).val = x.val ⊔ y.val

case refine_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
⊢ ⊥.val = ⊥

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
this : ((powersetCard n univ).sup fun x => x).val = (powersetCard n univ).sup val
⊢ ((powersetCard n univ).sup fun x => x).val = univ.val

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

Result:
case intro
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
this✝ : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
k : ℕ
hpos : 0 < k.succ
hn : k.succ ≤ Fintype.card σ
this : ((powersetCard k.succ univ).sup fun x => x).val = (powersetCard k.succ univ).sup val
⊢ ((powersetCard k.succ univ).sup fun x => x).val = univ.val

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
this : ((powersetCard n univ).sup fun x => x).val = (powersetCard n univ).sup val
⊢ (powersetCard n univ).sup val = univ.val

Tactic:
rw [← this]

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
this : ((powersetCard n univ).sup fun x => x).val = (powersetCard n univ).sup val
⊢ ((powersetCard n univ).sup fun x => x).val = univ.val

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ (esymm σ R n).degrees = univ.val

Tactic:
have :
  (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val := by
  funext
  simp [Finsupp.toMultiset_sum_single]

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
⊢ (esymm σ R n).degrees = univ.val

Proof state:
case h
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
x✝ : Finset σ
⊢ (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) x✝ = x✝.val

Tactic:
simp [Finsupp.toMultiset_sum_single]

Result:
no goals

Proof state:
case refine_1
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
⊢ ∀ (x y : Finset σ), (x ⊔ y).val = x.val ⊔ y.val

Tactic:
intros

Result:
case refine_1
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ (x✝ ⊔ y✝).val = x✝.val ⊔ y✝.val

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
⊢ (esymm σ R n).degrees = univ.val

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

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t => ∑ i ∈ t, Finsupp.single i 1) = val
⊢ (powersetCard n univ).sup val = univ.val