case intro
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Colorable G (chromaticNumber G)
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
⊢ Colorable G (chromaticNumber G)
cases nonempty_fintype V
no goals
case intro
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Colorable G (chromaticNumber G)
exact colorable_chromaticNumber G.colorable_of_fintype