case verts.h
ι : Sort ?u.233581
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
x✝ : ↑G'.verts
⊢ x✝ ∈ (Subgraph.restrict (Subgraph.coeSubgraph G'')).verts ↔ x✝ ∈ G''.verts

case Adj.h.h.a
ι : Sort ?u.233581
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
x✝¹ x✝ : ↑G'.verts
⊢ Adj (Subgraph.restrict (Subgraph.coeSubgraph G'')) x✝¹ x✝ ↔ Adj G'' x✝¹ x✝
ι : Sort ?u.233581
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
⊢ Subgraph.restrict (Subgraph.coeSubgraph G'') = G''
ext
no goals
case verts.h
ι : Sort ?u.233581
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
x✝ : ↑G'.verts
⊢ x✝ ∈ (Subgraph.restrict (Subgraph.coeSubgraph G'')).verts ↔ x✝ ∈ G''.verts
simp
case Adj.h.h.a
ι : Sort ?u.233581
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
x✝¹ x✝ : ↑G'.verts
⊢ Adj G'' x✝¹ x✝ → Adj G' ↑x✝¹ ↑x✝
case Adj.h.h.a
ι : Sort ?u.233581
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
x✝¹ x✝ : ↑G'.verts
⊢ Adj (Subgraph.restrict (Subgraph.coeSubgraph G'')) x✝¹ x✝ ↔ Adj G'' x✝¹ x✝
simp only [Relation.Map, comap_Adj, coe_Adj, Subtype.coe_prop, hom_apply, map_Adj,
  SetCoe.exists, Subtype.coe_mk, exists_and_right, exists_eq_right_right, Subtype.coe_eta,
  exists_true_left, exists_eq_right, and_iff_right_iff_imp]
no goals
case Adj.h.h.a
ι : Sort ?u.233581
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
G'' : Subgraph (Subgraph.coe G')
x✝¹ x✝ : ↑G'.verts
⊢ Adj G'' x✝¹ x✝ → Adj G' ↑x✝¹ ↑x✝
apply G''.adj_sub