rw [Ne.def, filter_eq_self] at this
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
this : filter (fun x => Odd (degree G x)) univ ≠ univ
⊢ ∃ v, Even (degree G v)
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
this : ¬∀ x ∈ univ, Odd (degree G x)
⊢ ∃ v, Even (degree G v)