ι : Sort ?u.11825
𝕜 : Type ?u.11828
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a c u v w : V
e : Sym2 V
h : Adj G a a
⊢ False
ι : Sort ?u.11825
𝕜 : Type ?u.11828
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 : Adj G a b
⊢ a ≠ b
rintro rfl
no goals
ι : Sort ?u.11825
𝕜 : Type ?u.11828
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a c u v w : V
e : Sym2 V
h : Adj G a a
⊢ False
exact G.irrefl h