Theorem: Finset.singleton_inter_nonempty (Untitled/Graphs/to_mathlib.lean)

State before:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ ({a} ∩ X).Nonempty → a ∈ X
Tactic:
simp [nonempty_iff_ne_empty]
State after:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ ¬{a} ∩ X = ∅ → a ∈ X

State before:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ ¬{a} ∩ X = ∅ → a ∈ X
Tactic:
contrapose!
State after:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ a ∉ X → {a} ∩ X = ∅

State before:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
⊢ a ∉ X → {a} ∩ X = ∅
Tactic:
exact singleton_inter_of_not_mem
State after:
no goals

State before:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
h : a ∈ X
⊢ ({a} ∩ X).Nonempty
Tactic:
use a
State after:
case h
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
h : a ∈ X
⊢ a ∈ {a} ∩ X

State before:
case h
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
a : V
X : Finset V
h : a ∈ X
⊢ a ∈ {a} ∩ X
Tactic:
simp [h]
State after:
no goals