-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem eq_singletonSubgraph_iff_verts_eq (H : G.Subgraph) {v : V} :
    H = G.singletonSubgraph v ↔ H.verts = {v}

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
⊢ H = G.singletonSubgraph v ↔ H.verts = {v}

Tactic:
refine ⟨fun h ↦ by rw [h, singletonSubgraph_verts], fun h ↦ ?_⟩

Result:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
⊢ H = G.singletonSubgraph v

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ ¬H.Adj x✝¹ x✝

Tactic:
intro ha

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H = G.singletonSubgraph v
⊢ H.verts = {v}

Tactic:
rw [h, singletonSubgraph_verts]

Result:
no goals

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
ha1 : x✝¹ = v
ha2 : x✝ = v
⊢ False

Tactic:
subst_vars

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
x✝ : V
ha : H.Adj x✝ x✝
h : H.verts = {x✝}
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
⊢ H = G.singletonSubgraph v

Tactic:
ext

Result:
case verts.h
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝ : V
⊢ x✝ ∈ H.verts ↔ x✝ ∈ (G.singletonSubgraph v).verts

case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ ↔ (G.singletonSubgraph v).Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ ↔ (G.singletonSubgraph v).Adj x✝¹ x✝

Tactic:
simp only [Prop.bot_eq_false, singletonSubgraph_adj, Pi.bot_apply, iff_false]

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ ¬H.Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
⊢ False

Tactic:
have ha1 := ha.fst_mem

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
⊢ False

Proof state:
case verts.h
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝ : V
⊢ x✝ ∈ H.verts ↔ x✝ ∈ (G.singletonSubgraph v).verts

Tactic:
rw [h, singletonSubgraph_verts]

Result:
no goals

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
ha2 : x✝ ∈ H.verts
⊢ False

Tactic:
rw [h, Set.mem_singleton_iff] at ha1 ha2

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
ha1 : x✝¹ = v
ha2 : x✝ = v
⊢ False

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
⊢ False

Tactic:
have ha2 := ha.snd_mem

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : H.Adj x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
ha2 : x✝ ∈ H.verts
⊢ False

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H : G.Subgraph
x✝ : V
ha : H.Adj x✝ x✝
h : H.verts = {x✝}
⊢ False

Tactic:
exact ha.ne rfl

Result:
no goals