no goals
ι : Sort ?u.101184
𝕜 : Type ?u.101187
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
h : a ≠ b
ha : e ∈ incidenceSet G a
hb : e ∈ incidenceSet G b
⊢ Adj G a b
rwa [← mk'_mem_incidenceSet_left_iff, ←
  Set.mem_singleton_iff.1 <| G.incidenceSet_inter_incidenceSet_subset h ⟨ha, hb⟩]