R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ ∀ (x : Multiset R), x ∈ powersetLen k s → (prod ∘ map Neg.neg) x = (-1) ^ k * prod x
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ esymm (map Neg.neg s) k = (-1) ^ k * esymm s k
rw [esymm, esymm, ← Multiset.sum_map_mul_left, Multiset.powersetLen_map, Multiset.map_map,
  map_congr (Eq.refl _)]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = (-1) ^ k * prod x
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ ∀ (x : Multiset R), x ∈ powersetLen k s → (prod ∘ map Neg.neg) x = (-1) ^ k * prod x
intro x hx
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * prod x
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = (-1) ^ k * prod x
rw [(mem_powersetLen.mp hx).right.symm, ← prod_replicate, ← Multiset.map_const]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * prod (map (fun x => x) x)
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * prod x
nth_rw 3 [← map_id' x]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = prod (map ?m.791744 x)

R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ ∀ (x_1 : R), x_1 ∈ x → Function.const R (-1) x_1 * x_1 = ?m.791744 x_1

R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ R → R
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * prod (map (fun x => x) x)
rw [← prod_map_mul, map_congr (Eq.refl _)]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ ∀ (x_1 : R), x_1 ∈ x → Function.const R (-1) x_1 * x_1 = -x_1
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = prod (map ?m.791744 x)

R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ ∀ (x_1 : R), x_1 ∈ x → Function.const R (-1) x_1 * x_1 = ?m.791744 x_1

R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ R → R
rfl
no goals
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ ∀ (x_1 : R), x_1 ∈ x → Function.const R (-1) x_1 * x_1 = -x_1
exact fun z _ => neg_one_mul z