no goals
ι : Sort ?u.144589
𝕜 : Type ?u.144592
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(neighborSet G v ∪ neighborSet (Gᶜ) v)
⊢ card (Set.toFinset (neighborSet G v ∪ neighborSet (Gᶜ) v)) = Fintype.card V - 1
classical simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
    Finset.card_compl, Set.toFinset_card, Set.card_singleton]
no goals
ι : Sort ?u.144589
𝕜 : Type ?u.144592
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝¹ : Fintype V
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(neighborSet G v ∪ neighborSet (Gᶜ) v)
⊢ card (Set.toFinset (neighborSet G v ∪ neighborSet (Gᶜ) v)) = Fintype.card V - 1
simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
Finset.card_compl, Set.toFinset_card, Set.card_singleton]