rw [edgeSet_coe, Set.image_preimage_eq_iff]
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
⊢ Sym2.map Subtype.val '' G'.coe.edgeSet = G'.edgeSet
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
⊢ G'.edgeSet ⊆ Set.range (Sym2.map Subtype.val)