case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h✝ : 0 < chromaticNumber G
h : ℕ
hn : h ∈ {n | Colorable G n}
⊢ Colorable G (chromaticNumber G)
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : 0 < chromaticNumber G
⊢ Colorable G (chromaticNumber G)
obtain ⟨h, hn⟩ := Nat.nonempty_of_pos_sInf h
no goals
case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h✝ : 0 < chromaticNumber G
h : ℕ
hn : h ∈ {n | Colorable G n}
⊢ Colorable G (chromaticNumber G)
exact colorable_chromaticNumber hn