case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Finite V
s : Finset V
h : IsClique G ↑s
val✝ : Fintype V
⊢ Finset.card s ≤ chromaticNumber G
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Finite V
s : Finset V
h : IsClique G ↑s
⊢ Finset.card s ≤ chromaticNumber G
cases nonempty_fintype V
no goals
case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Finite V
s : Finset V
h : IsClique G ↑s
val✝ : Fintype V
⊢ Finset.card s ≤ chromaticNumber G
exact h.card_le_of_colorable G.colorable_chromaticNumber_of_fintype