V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
h : chromaticNumber G = 0
h' : Colorable G (chromaticNumber G)
⊢ IsEmpty V
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
h : chromaticNumber G = 0
⊢ IsEmpty V
have h' := G.colorable_chromaticNumber_of_fintype
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
h : chromaticNumber G = 0
h' : Colorable G 0
⊢ IsEmpty V
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
h : chromaticNumber G = 0
h' : Colorable G (chromaticNumber G)
⊢ IsEmpty V
rw [h] at h'
no goals
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
h : chromaticNumber G = 0
h' : Colorable G 0
⊢ IsEmpty V
exact G.isEmpty_of_colorable_zero h'