∀ {V : Type u_1} [inst : Fintype V] {W : Type u_2} [inst_1 : Fintype W] [inst_2 : DecidableEq W] (f : V ↪ W)
  (G : SimpleGraph V) [inst_3 : DecidableRel G.Adj],
  (SimpleGraph.map (⇑f) G).edgeFinset = Finset.map f.sym2Map G.edgeFinset