ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
⊢ H = SimpleGraph.singletonSubgraph G v
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
⊢ H = SimpleGraph.singletonSubgraph G v ↔ H.verts = {v}
refine' ⟨fun h ↦ by rw [h, singletonSubgraph_verts], fun h ↦ _⟩
case verts.h
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝ : V
⊢ x✝ ∈ H.verts ↔ x✝ ∈ (SimpleGraph.singletonSubgraph G v).verts

case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ Subgraph.Adj H x✝¹ x✝ ↔ Subgraph.Adj (SimpleGraph.singletonSubgraph G v) x✝¹ x✝
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
⊢ H = SimpleGraph.singletonSubgraph G v
ext
no goals
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H = SimpleGraph.singletonSubgraph G v
⊢ H.verts = {v}
rw [h, singletonSubgraph_verts]
no goals
case verts.h
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝ : V
⊢ x✝ ∈ H.verts ↔ x✝ ∈ (SimpleGraph.singletonSubgraph G v).verts
rw [h, singletonSubgraph_verts]
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ ¬Subgraph.Adj H x✝¹ x✝
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ Subgraph.Adj H x✝¹ x✝ ↔ Subgraph.Adj (SimpleGraph.singletonSubgraph G v) x✝¹ x✝
simp only [Prop.bot_eq_false, singletonSubgraph_Adj, Pi.bot_apply, iff_false_iff]
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
⊢ False
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ ¬Subgraph.Adj H x✝¹ x✝
intro ha
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
⊢ False
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
⊢ False
have ha1 := ha.fst_mem
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
ha2 : x✝ ∈ H.verts
⊢ False
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
⊢ False
have ha2 := ha.snd_mem
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
ha1 : x✝¹ = v
ha2 : x✝ = v
⊢ False
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
ha1 : x✝¹ ∈ H.verts
ha2 : x✝ ∈ H.verts
⊢ False
rw [h, Set.mem_singleton_iff] at ha1 ha2
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
x✝ : V
ha : Subgraph.Adj H x✝ x✝
h : H.verts = {x✝}
⊢ False
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
v : V
h : H.verts = {v}
x✝¹ x✝ : V
ha : Subgraph.Adj H x✝¹ x✝
ha1 : x✝¹ = v
ha2 : x✝ = v
⊢ False
subst_vars
no goals
case Adj.h.h.a
ι : Sort ?u.216099
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
H : Subgraph G
x✝ : V
ha : Subgraph.Adj H x✝ x✝
h : H.verts = {x✝}
⊢ False
exact ha.ne rfl