simp only [eq_singleton_iff_unique_mem, mem_filter, mem_univ, Subgraph.coe_bot, true_and_iff,
  Nonempty.forall]
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 β
⊢ filter (fun H' => Nonempty (⊥ ≃g H'.coe)) univ =
    {{ verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }}
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 β
⊢ Nonempty (⊥ ≃g { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }.coe) ∧
    ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }