case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ esymm s (↑card s - k) = coeff (∑ j in Finset.range (↑card s + 1), ↑C (esymm s j) * X ^ (↑card s - j)) k
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ coeff (prod (map (fun r => X + ↑C r) s)) k = esymm s (↑card s - k)
convert Polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k using 1
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ esymm s (↑card s - k) = ∑ x in Finset.range (↑card s + 1), if k = ↑card s - x then esymm s x else 0
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ esymm s (↑card s - k) = coeff (∑ j in Finset.range (↑card s + 1), ↑C (esymm s j) * X ^ (↑card s - j)) k
simp_rw [finset_sum_coeff, coeff_C_mul_X_pow]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ esymm s (↑card s - k) = if k = ↑card s - (↑card s - k) then esymm s (↑card s - k) else 0

case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ∀ (b : (fun x => ℕ) s),
    b ∈ Finset.range (↑card s + 1) → b ≠ ↑card s - k → (if k = ↑card s - b then esymm s b else 0) = 0

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ↑card s - k ∈ Finset.range (↑card s + 1)
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ esymm s (↑card s - k) = ∑ x in Finset.range (↑card s + 1), if k = ↑card s - x then esymm s x else 0
rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _]
no goals
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ esymm s (↑card s - k) = if k = ↑card s - (↑card s - k) then esymm s (↑card s - k) else 0
rw [if_pos (Nat.sub_sub_self h).symm]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
⊢ (if k = ↑card s - j then esymm s j else 0) = 0
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ∀ (b : (fun x => ℕ) s),
    b ∈ Finset.range (↑card s + 1) → b ≠ ↑card s - k → (if k = ↑card s - b then esymm s b else 0) = 0
intro j hj1 hj2
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
⊢ k ≠ ↑card s - j
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
⊢ (if k = ↑card s - j then esymm s j else 0) = 0
suffices k ≠ card s - j by rw [if_neg this]
no goals
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
this : k ≠ ↑card s - j
⊢ (if k = ↑card s - j then esymm s j else 0) = 0
rw [if_neg this]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
hn : k = ↑card s - j
⊢ False
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
⊢ k ≠ ↑card s - j
intro hn
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ j
hn : k = ↑card s - j
⊢ False
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
hn : k = ↑card s - j
⊢ False
rw [hn, Nat.sub_sub_self (Nat.lt_succ_iff.mp (Finset.mem_range.mp hj1))] at hj2
no goals
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ j
hn : k = ↑card s - j
⊢ False
exact Ne.irrefl hj2
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ↑card s - k < ↑card s + 1
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ↑card s - k ∈ Finset.range (↑card s + 1)
rw [Finset.mem_range]
no goals
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ↑card s - k < ↑card s + 1
exact Nat.sub_lt_succ (Multiset.card s) k