Theorem: SimpleGraph.neighborFinset_top (ExponentialRamsey/Prereq/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝¹ : Fintype V
inst✝ : DecidableEq V
x : V
⊢ neighborFinset ⊤ x = {x}ᶜ
Tactic:
ext y
State after:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝¹ : Fintype V
inst✝ : DecidableEq V
x y : V
⊢ y ∈ neighborFinset ⊤ x ↔ y ∈ {x}ᶜ

State before:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝¹ : Fintype V
inst✝ : DecidableEq V
x y : V
⊢ y ∈ neighborFinset ⊤ x ↔ y ∈ {x}ᶜ
Tactic:
rw [mem_neighborFinset, top_adj, Finset.mem_compl, mem_singleton, ne_comm]
State after:
no goals