case mk.mk
ι : Sort ?u.97949
𝕜 : Type ?u.97952
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
hp : Adj G p.fst p.snd
q : V × V
hq : Adj G q.fst q.snd
⊢ Dart.edge { toProd := p, is_adj := hp } = Dart.edge { toProd := q, is_adj := hq } ↔
    { toProd := p, is_adj := hp } = { toProd := q, is_adj := hq } ∨
      { toProd := p, is_adj := hp } = Dart.symm { toProd := q, is_adj := hq }
ι : Sort ?u.97949
𝕜 : Type ?u.97952
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₁ d₂ : Dart G), Dart.edge d₁ = Dart.edge d₂ ↔ d₁ = d₂ ∨ d₁ = Dart.symm d₂
rintro ⟨p, hp⟩ ⟨q, hq⟩
no goals
case mk.mk
ι : Sort ?u.97949
𝕜 : Type ?u.97952
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
hp : Adj G p.fst p.snd
q : V × V
hq : Adj G q.fst q.snd
⊢ Dart.edge { toProd := p, is_adj := hp } = Dart.edge { toProd := q, is_adj := hq } ↔
    { toProd := p, is_adj := hp } = { toProd := q, is_adj := hq } ∨
      { toProd := p, is_adj := hp } = Dart.symm { toProd := q, is_adj := hq }
simp [Sym2.mk''_eq_mk''_iff, -Quotient.eq]