no goals
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (chromaticNumber G)
classical
dsimp only [chromaticNumber]
rw [Nat.sInf_def]
apply Nat.find_spec
exact colorable_set_nonempty_of_colorable hc
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (sInf {n | Colorable G n})
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (chromaticNumber G)
dsimp only [chromaticNumber]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (Nat.find ?m.133011)

V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Set.Nonempty {n | Colorable G n}
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (sInf {n | Colorable G n})
rw [Nat.sInf_def]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Set.Nonempty {n | Colorable G n}
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (Nat.find ?m.133011)

V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Set.Nonempty {n | Colorable G n}
apply Nat.find_spec
no goals
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Set.Nonempty {n | Colorable G n}
exact colorable_set_nonempty_of_colorable hc