σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ degrees (esymm σ R n) = univ.val
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ degrees (esymm σ R n) = univ.val
have :
  (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i : σ in t, Finsupp.single i 1) = Finset.val := by
  funext
  simp [Finsupp.toMultiset_sum_single]
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ sup (powersetLen n univ) val = univ.val
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ degrees (esymm σ R n) = univ.val
rw [degrees_def, support_esymm, sup_image, this]
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
this : (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
⊢ (sup (powersetLen n univ) fun x => x).val = univ.val
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
this : (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
⊢ sup (powersetLen n univ) val = univ.val
rw [← this]
case intro
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
k : ℕ
hpos : 0 < Nat.succ k
hn : Nat.succ k ≤ Fintype.card σ
this : (sup (powersetLen (Nat.succ k) univ) fun x => x).val = sup (powersetLen (Nat.succ k) univ) val
⊢ (sup (powersetLen (Nat.succ k) univ) fun x => x).val = univ.val
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
this : (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
⊢ (sup (powersetLen n univ) fun x => x).val = univ.val
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
no goals
case intro
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
k : ℕ
hpos : 0 < Nat.succ k
hn : Nat.succ k ≤ Fintype.card σ
this : (sup (powersetLen (Nat.succ k) univ) fun x => x).val = sup (powersetLen (Nat.succ k) univ) val
⊢ (sup (powersetLen (Nat.succ k) univ) fun x => x).val = univ.val
simpa using powerset_len_sup _ _ (Nat.lt_of_succ_le hn)
case h
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
x✝ : Finset σ
⊢ (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) x✝ = x✝.val
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
funext
no goals
case h
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
x✝ : Finset σ
⊢ (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) x✝ = x✝.val
simp [Finsupp.toMultiset_sum_single]
case refine'_1
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ ∀ (x y : Finset σ), (x ⊔ y).val = x.val ⊔ y.val

case refine'_2
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ ⊥.val = ⊥
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
refine' comp_sup_eq_sup_comp _ _ _
case refine'_1
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ (x✝ ⊔ y✝).val = x✝.val ⊔ y✝.val
case refine'_1
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ ∀ (x y : Finset σ), (x ⊔ y).val = x.val ⊔ y.val
intros
case refine'_1
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ x✝.val ∪ y✝.val = x✝.val ⊔ y✝.val
case refine'_1
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ (x✝ ⊔ y✝).val = x✝.val ⊔ y✝.val
simp only [union_val, sup_eq_union]
no goals
case refine'_1
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ x✝.val ∪ y✝.val = x✝.val ⊔ y✝.val
congr
no goals
case refine'_2
σ : Type u_2
R : Type u_1
τ : Type ?u.196415
S : Type ?u.196418
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ ⊥.val = ⊥
rfl