ι : Sort ?u.99591
𝕜 : Type ?u.99594
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
v : V
e₁ e₂ : ↑(neighborSet G v)
h' : (v, ↑e₁) = (v, ↑e₂)
⊢ ↑e₁ = ↑e₂
ι : Sort ?u.99591
𝕜 : Type ?u.99594
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
v : V
e₁ e₂ : ↑(neighborSet G v)
h : dartOfNeighborSet G v e₁ = dartOfNeighborSet G v e₂
⊢ ↑e₁ = ↑e₂
injection h with h'
no goals
ι : Sort ?u.99591
𝕜 : Type ?u.99594
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
v : V
e₁ e₂ : ↑(neighborSet G v)
h' : (v, ↑e₁) = (v, ↑e₂)
⊢ ↑e₁ = ↑e₂
convert congr_arg Prod.snd h'