case mk
ι : Sort ?u.94190
𝕜 : Type ?u.94193
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
toProd✝ : V × V
is_adj✝ : Adj G toProd✝.fst toProd✝.snd
⊢ { toProd := toProd✝, is_adj := is_adj✝ } = d₂ ↔ { toProd := toProd✝, is_adj := is_adj✝ }.toProd = d₂.toProd
ι : Sort ?u.94190
𝕜 : Type ?u.94193
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
⊢ d₁ = d₂ ↔ d₁.toProd = d₂.toProd
cases d₁
case mk.mk
ι : Sort ?u.94190
𝕜 : Type ?u.94193
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
toProd✝¹ : V × V
is_adj✝¹ : Adj G toProd✝¹.fst toProd✝¹.snd
toProd✝ : V × V
is_adj✝ : Adj G toProd✝.fst toProd✝.snd
⊢ { toProd := toProd✝¹, is_adj := is_adj✝¹ } = { toProd := toProd✝, is_adj := is_adj✝ } ↔
    { toProd := toProd✝¹, is_adj := is_adj✝¹ }.toProd = { toProd := toProd✝, is_adj := is_adj✝ }.toProd
case mk
ι : Sort ?u.94190
𝕜 : Type ?u.94193
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
toProd✝ : V × V
is_adj✝ : Adj G toProd✝.fst toProd✝.snd
⊢ { toProd := toProd✝, is_adj := is_adj✝ } = d₂ ↔ { toProd := toProd✝, is_adj := is_adj✝ }.toProd = d₂.toProd
cases d₂
no goals
case mk.mk
ι : Sort ?u.94190
𝕜 : Type ?u.94193
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
toProd✝¹ : V × V
is_adj✝¹ : Adj G toProd✝¹.fst toProd✝¹.snd
toProd✝ : V × V
is_adj✝ : Adj G toProd✝.fst toProd✝.snd
⊢ { toProd := toProd✝¹, is_adj := is_adj✝¹ } = { toProd := toProd✝, is_adj := is_adj✝ } ↔
    { toProd := toProd✝¹, is_adj := is_adj✝¹ }.toProd = { toProd := toProd✝, is_adj := is_adj✝ }.toProd
simp