no goals
ι : Sort ?u.72136
𝕜 : Type ?u.72139
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
G₁ G₂ : SimpleGraph V
⊢ Adj G a b ↔ ∃ e, ↑e = Quotient.mk (Sym2.Rel.setoid V) (a, b)
simp only [mem_edgeSet, exists_prop, SetCoe.exists, exists_eq_right, Subtype.coe_mk]