V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
⊢ ∀ (b : ℕ), b ∈ {n | Colorable G n} → Nat.succ 0 ≤ b
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
⊢ 0 < chromaticNumber G
apply le_csInf (colorable_set_nonempty_of_colorable hc)
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
⊢ Nat.succ 0 ≤ m
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
⊢ ∀ (b : ℕ), b ∈ {n | Colorable G n} → Nat.succ 0 ≤ b
intro m hm
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : ¬Nat.succ 0 ≤ m
⊢ False
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
⊢ Nat.succ 0 ≤ m
by_contra h'
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
⊢ False
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : ¬Nat.succ 0 ≤ m
⊢ False
simp only [not_le, Nat.lt_one_iff] at h'
case mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
⊢ False
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
⊢ False
obtain ⟨i, hi⟩ := hm.some (Classical.arbitrary V)
case mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
h₁ : i < 0
⊢ False
case mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
⊢ False
have h₁: i < 0 := lt_of_lt_of_le hi (Nat.le_of_lt_succ h')
no goals
case mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
h₁ : i < 0
⊢ False
exact Nat.not_lt_zero _ h₁