no goals
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d d' : Dart G
⊢ d' ∈ filter (fun d' => edge d' = edge d) univ ↔ d' ∈ {d, symm d}
simpa using dart_edge_eq_iff d' d