Theorem: SimpleGraph.not_mem_nbhd (Turan4/NbhdRes.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ ¬v ∈ neighborFinset G v
Tactic:
rw [mem_neighborFinset]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ ¬Adj G v v

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ ¬Adj G v v
Tactic:
exact G.loopless v
State after:
no goals