case intro
ι : Sort ?u.150205
𝕜 : Type ?u.150208
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
inst✝ : DecidableEq V
v : V
e : Sym2 V
he : e ∈ edgeSet G
hv : v ∈ e
⊢ otherVertexOfIncident G (_ : e ∈ edgeSet G ∧ v ∈ e) ∈ neighborSet G v
ι : Sort ?u.150205
𝕜 : Type ?u.150208
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
inst✝ : DecidableEq V
v : V
e : Sym2 V
h : e ∈ incidenceSet G v
⊢ otherVertexOfIncident G h ∈ neighborSet G v
cases' h with he hv
no goals
case intro
ι : Sort ?u.150205
𝕜 : Type ?u.150208
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
inst✝ : DecidableEq V
v : V
e : Sym2 V
he : e ∈ edgeSet G
hv : v ∈ e
⊢ otherVertexOfIncident G (_ : e ∈ edgeSet G ∧ v ∈ e) ∈ neighborSet G v
rwa [← Sym2.other_spec' hv, mem_edgeSet] at he