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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ ¬v ∈ nbhdRes G v A
Tactic:
rw [mem_res_nbhd_iff]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ ¬(v ∈ A ∧ v ∈ neighborFinset G v)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ ¬(v ∈ A ∧ v ∈ neighborFinset G v)
Tactic:
push_neg
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ v ∈ A → ¬v ∈ neighborFinset G v

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ v ∈ A → ¬v ∈ neighborFinset G v
Tactic:
intro _
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
_✝ : v ∈ A
⊢ ¬v ∈ neighborFinset G v

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
_✝ : v ∈ A
⊢ ¬v ∈ neighborFinset G v
Tactic:
exact G.not_mem_nbhd v
State after:
no goals