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

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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
⊢ x ∈ nbhdRes G v A → x ∈ 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 α
x : α
⊢ x ∈ A ∧ x ∈ neighborFinset G v → x ∈ A

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

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