K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ ∀ (i : σ), Multiset.count i (degrees (∏ n : σ, (1 - (X n - ↑C (c n)) ^ (Fintype.card K - 1)))) ≤ Fintype.card K - 1
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ indicator c ∈ restrictDegree σ K (Fintype.card K - 1)
rw [mem_restrictDegree_iff_sup, indicator]
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (degrees (∏ n : σ, (1 - (X n - ↑C (c n)) ^ (Fintype.card K - 1)))) ≤ Fintype.card K - 1
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ ∀ (i : σ), Multiset.count i (degrees (∏ n : σ, (1 - (X n - ↑C (c n)) ^ (Fintype.card K - 1)))) ≤ Fintype.card K - 1
intro n
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (∑ s : σ, (Fintype.card K - 1) • {s}) = Fintype.card K - 1
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (degrees (∏ n : σ, (1 - (X n - ↑C (c n)) ^ (Fintype.card K - 1)))) ≤ Fintype.card K - 1
refine' le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq _)
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (∑ s : σ, (Fintype.card K - 1) • {s}) = Fintype.card K - 1
simp_rw [← Multiset.coe_countAddMonoidHom, (Multiset.countAddMonoidHom n).map_sum,
  AddMonoidHom.map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = ?m.179638

K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ?m.179638 = Fintype.card K - 1

K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ℕ
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
trans
case refine'_1
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∀ (b : σ), b ∈ Finset.univ → b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0

case refine'_2
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ¬n ∈ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0

K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = ?m.179638

K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ?m.179638 = Fintype.card K - 1

K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ℕ
refine' Finset.sum_eq_single n _ _
case refine'_1
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n b : σ
a✝ : b ∈ Finset.univ
ne : b ≠ n
⊢ (Fintype.card K - 1) * Multiset.count n {b} = 0
case refine'_1
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∀ (b : σ), b ∈ Finset.univ → b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0
intro b _ ne
no goals
case refine'_1
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n b : σ
a✝ : b ∈ Finset.univ
ne : b ≠ n
⊢ (Fintype.card K - 1) * Multiset.count n {b} = 0
simp [Multiset.count_singleton, ne, if_neg (Ne.symm _)]
case refine'_2
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
h : ¬n ∈ Finset.univ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = 0
case refine'_2
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ¬n ∈ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0
intro h
no goals
case refine'_2
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
h : ¬n ∈ Finset.univ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = 0
exact (h <| Finset.mem_univ _).elim
no goals
K : Type u_2
σ : Type u_1
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
rw [Multiset.count_singleton_self, mul_one]