rw [←card_lt_iff_ne_univ, (card_le_univ _).lt_iff_ne]
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
⊢ filter (fun x => Odd (degree G x)) univ ≠ univ
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
⊢ Finset.card (filter (fun x => Odd (degree G x)) univ) ≠ Fintype.card V