ext a b
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
H : SimpleGraph β
H' : H.Subgraph
e : ⊥ ≃g H'.coe
⊢ H'.Adj = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.Adj
case h.e'_2.h.e'_2.h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
H : SimpleGraph β
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ H'.Adj a b ↔ { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.Adj a b