SimpleGraph.Dart.ext

theorem SimpleGraph.Dart.ext : ∀ {V : Type u_1} {G : SimpleGraph V} (d₁ d₂ : G.Dart), d₁.toProd = d₂.toProd → d₁ = d₂

This theorem states that for any simple graph `G` with vertices of type `V`, if we have two 'darts' (directed edges) `d₁` and `d₂` such that their pair of vertices (obtained using `toProd`) are equal, then the two darts themselves are equal. In essence, two darts are considered identical if they are directed from the same vertex to another same vertex, regardless of their internal representation.

More concisely: In a simple graph, two darts with equal source-target vertex pairs are equal.