case false
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
⊢ V → False
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
⊢ IsEmpty V
constructor
case false
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
v : V
⊢ False
case false
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
⊢ V → False
intro v
case false.mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
v : V
i : ℕ
hi : i < 0
⊢ False
case false
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
v : V
⊢ False
obtain ⟨i, hi⟩ := h.some v
no goals
case false.mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
v : V
i : ℕ
hi : i < 0
⊢ False
exact Nat.not_lt_zero _ hi