case h.e'_4
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
s : Finset V
h : IsClique G ↑s
n : ℕ
hc : Colorable G n
⊢ n = Fintype.card (Fin n)
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
s : Finset V
h : IsClique G ↑s
n : ℕ
hc : Colorable G n
⊢ Finset.card s ≤ n
convert h.card_le_of_coloring hc.some
no goals
case h.e'_4
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
s : Finset V
h : IsClique G ↑s
n : ℕ
hc : Colorable G n
⊢ n = Fintype.card (Fin n)
simp