case mk
ι : Sort ?u.98474
𝕜 : Type ?u.98477
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
p : V × V
h : Adj G p.fst p.snd
⊢ ∀ {p_1 : V × V},
    Dart.edge { toProd := p, is_adj := h } = Quotient.mk (Sym2.Rel.setoid V) p_1 ↔
      { toProd := p, is_adj := h }.toProd = p_1 ∨ { toProd := p, is_adj := h }.toProd = Prod.swap p_1
ι : Sort ?u.98474
𝕜 : Type ?u.98477
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
⊢ ∀ {d : Dart G} {p : V × V}, Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) p ↔ d.toProd = p ∨ d.toProd = Prod.swap p
rintro ⟨p, h⟩
no goals
case mk
ι : Sort ?u.98474
𝕜 : Type ?u.98477
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
p : V × V
h : Adj G p.fst p.snd
⊢ ∀ {p_1 : V × V},
    Dart.edge { toProd := p, is_adj := h } = Quotient.mk (Sym2.Rel.setoid V) p_1 ↔
      { toProd := p, is_adj := h }.toProd = p_1 ∨ { toProd := p, is_adj := h }.toProd = Prod.swap p_1
apply Sym2.mk''_eq_mk''_iff