refine' ⟨⟨⟨⟨isEmptyElim, isEmptyElim, isEmptyElim, isEmptyElim⟩, fun {a} ↦ isEmptyElim a⟩⟩,
  fun H' e ↦ Subgraph.ext _ _ _ $ funext₂ fun 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 β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
⊢ Nonempty (⊥ ≃g ⊥) ∧ ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = ⊥
case h.e'_2.h.e'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
H' : H.Subgraph
e : ⊥ ≃g H'.coe
⊢ H'.verts = ⊥.verts

case h.e'_2.h.e'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ H'.Adj a b = ⊥.Adj a b