exact fun ⟨f⟩ ↦ Set.Nonempty.image _ ⟨_, f.map_mem_edgeSet_iff.2 he⟩
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : H.Subgraph
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Nonempty (G ≃g H'.coe) → (Sym2.map Subtype.val '' H'.coe.edgeSet).Nonempty
no goals