simpa [Set.eq_empty_iff_forall_not_mem, filter_eq_empty_iff, ‹IsEmpty α›] using
  e.toEquiv.symm.isEmpty_congr
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
no goals