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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ¬nbhdRes G v A = ∅
⊢ ∃ w, w ∈ A ∧ Adj G v w
Tactic:
rw [nbhdRes] at hA
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ¬A ∩ neighborFinset G v = ∅
⊢ ∃ w, w ∈ A ∧ Adj G v w

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ¬A ∩ neighborFinset G v = ∅
⊢ ∃ w, w ∈ A ∧ Adj G v w
Tactic:
contrapose! hA
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
⊢ A ∩ neighborFinset G v = ∅

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
⊢ A ∩ neighborFinset G v = ∅
Tactic:
rw [eq_empty_iff_forall_not_mem]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
⊢ ∀ (x : α), ¬x ∈ A ∩ neighborFinset G v

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
⊢ ∀ (x : α), ¬x ∈ A ∩ neighborFinset G v
Tactic:
intro x hx
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∩ neighborFinset G v
⊢ False

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∩ neighborFinset G v
⊢ False
Tactic:
rw [mem_inter, mem_neighborFinset] at hx
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∧ Adj G v x
⊢ False

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∧ Adj G v x
⊢ False
Tactic:
exact hA x hx.1 hx.2
State after:
no goals