case verts.h
ι : Sort ?u.260819
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝ : V
⊢ x✝ ∈ (induce G' G'.verts).verts ↔ x✝ ∈ G'.verts

case Adj.h.h.a
ι : Sort ?u.260819
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
⊢ Adj (induce G' G'.verts) x✝¹ x✝ ↔ Adj G' x✝¹ x✝
ι : Sort ?u.260819
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
⊢ induce G' G'.verts = G'
ext
no goals
case verts.h
ι : Sort ?u.260819
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝ : V
⊢ x✝ ∈ (induce G' G'.verts).verts ↔ x✝ ∈ G'.verts
simp
case Adj.h.h.a.mpr
ι : Sort ?u.260819
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
⊢ Adj G' x✝¹ x✝ → x✝¹ ∈ G'.verts ∧ x✝ ∈ G'.verts
case Adj.h.h.a
ι : Sort ?u.260819
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
⊢ Adj (induce G' G'.verts) x✝¹ x✝ ↔ Adj G' x✝¹ x✝
constructor <;>
  simp (config := { contextual := true }) only [induce_Adj, imp_true_iff, and_true_iff]
no goals
case Adj.h.h.a.mpr
ι : Sort ?u.260819
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
⊢ Adj G' x✝¹ x✝ → x✝¹ ∈ G'.verts ∧ x✝ ∈ G'.verts
exact fun ha ↦ ⟨G'.edge_vert ha, G'.edge_vert ha.symm⟩