case mk.mk
ι : Sort ?u.98622
𝕜 : Type ?u.98625
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
a b : V
h : Adj G (a, b).fst (a, b).snd
u v : V
⊢ Dart.edge { toProd := (a, b), is_adj := h } = Quotient.mk (Sym2.Rel.setoid V) (u, v) ↔
    { toProd := (a, b), is_adj := h }.toProd.fst = u ∧ { toProd := (a, b), is_adj := h }.toProd.snd = v ∨
      { toProd := (a, b), is_adj := h }.toProd.fst = v ∧ { toProd := (a, b), is_adj := h }.toProd.snd = u
ι : Sort ?u.98622
𝕜 : Type ?u.98625
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} {u v : V},
    Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (u, v) ↔ d.fst = u ∧ d.snd = v ∨ d.fst = v ∧ d.snd = u
rintro ⟨⟨a, b⟩, h⟩ u v
case mk.mk
ι : Sort ?u.98622
𝕜 : Type ?u.98625
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
a b : V
h : Adj G (a, b).fst (a, b).snd
u v : V
⊢ { toProd := (a, b), is_adj := h }.toProd = (u, v) ∨ { toProd := (a, b), is_adj := h }.toProd = Prod.swap (u, v) ↔
    { toProd := (a, b), is_adj := h }.toProd.fst = u ∧ { toProd := (a, b), is_adj := h }.toProd.snd = v ∨
      { toProd := (a, b), is_adj := h }.toProd.fst = v ∧ { toProd := (a, b), is_adj := h }.toProd.snd = u
case mk.mk
ι : Sort ?u.98622
𝕜 : Type ?u.98625
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
a b : V
h : Adj G (a, b).fst (a, b).snd
u v : V
⊢ Dart.edge { toProd := (a, b), is_adj := h } = Quotient.mk (Sym2.Rel.setoid V) (u, v) ↔
    { toProd := (a, b), is_adj := h }.toProd.fst = u ∧ { toProd := (a, b), is_adj := h }.toProd.snd = v ∨
      { toProd := (a, b), is_adj := h }.toProd.fst = v ∧ { toProd := (a, b), is_adj := h }.toProd.snd = u
rw [dart_edge_eq_mk'_iff]
no goals
case mk.mk
ι : Sort ?u.98622
𝕜 : Type ?u.98625
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
a b : V
h : Adj G (a, b).fst (a, b).snd
u v : V
⊢ { toProd := (a, b), is_adj := h }.toProd = (u, v) ∨ { toProd := (a, b), is_adj := h }.toProd = Prod.swap (u, v) ↔
    { toProd := (a, b), is_adj := h }.toProd.fst = u ∧ { toProd := (a, b), is_adj := h }.toProd.snd = v ∨
      { toProd := (a, b), is_adj := h }.toProd.fst = v ∧ { toProd := (a, b), is_adj := h }.toProd.snd = u
simp