ι : Sort ?u.409745
𝕜 : Type ?u.409748
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
f✝ : G →g G'
f : ⊤ →g G'
v w : V
h : ↑f v = ↑f w
⊢ v = w
ι : Sort ?u.409745
𝕜 : Type ?u.409748
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
f✝ : G →g G'
f : ⊤ →g G'
⊢ Injective ↑f
intro v w h
ι : Sort ?u.409745
𝕜 : Type ?u.409748
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
f✝ : G →g G'
f : ⊤ →g G'
v w : V
h : v ≠ w
⊢ ↑f v ≠ ↑f w
ι : Sort ?u.409745
𝕜 : Type ?u.409748
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
f✝ : G →g G'
f : ⊤ →g G'
v w : V
h : ↑f v = ↑f w
⊢ v = w
contrapose! h
no goals
ι : Sort ?u.409745
𝕜 : Type ?u.409748
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
f✝ : G →g G'
f : ⊤ →g G'
v w : V
h : v ≠ w
⊢ ↑f v ≠ ↑f w
exact G'.ne_of_adj (map_adj _ ((top_adj _ _).mpr h))