ι : Sort ?u.72658
𝕜 : Type ?u.72661
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
e : Sym2 V
v : V
h : v ∈ e
he : Quotient.mk (Sym2.Rel.setoid V) (Sym2.Mem.other h, v) ∈ edgeSet G
⊢ Sym2.Mem.other h ≠ v
ι : Sort ?u.72658
𝕜 : Type ?u.72661
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
e : Sym2 V
he : e ∈ edgeSet G
v : V
h : v ∈ e
⊢ Sym2.Mem.other h ≠ v
erw [← Sym2.other_spec h, Sym2.eq_swap] at he
no goals
ι : Sort ?u.72658
𝕜 : Type ?u.72661
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
e : Sym2 V
v : V
h : v ∈ e
he : Quotient.mk (Sym2.Rel.setoid V) (Sym2.Mem.other h, v) ∈ edgeSet G
⊢ Sym2.Mem.other h ≠ v
exact G.ne_of_adj he