V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
⊢ chromaticNumber ⊤ = 0
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
⊢ chromaticNumber ⊤ = 0
let n := (⊤ : SimpleGraph V).chromaticNumber
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : ¬chromaticNumber ⊤ = 0
⊢ False
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
⊢ chromaticNumber ⊤ = 0
by_contra hc
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ False
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : ¬chromaticNumber ⊤ = 0
⊢ False
replace hc := pos_iff_ne_zero.mpr hc
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ Nat.succ n ≤ n
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ False
apply Nat.not_succ_le_self n
case h.e'_3
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ Nat.succ n = chromaticNumber ⊤

V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ chromaticNumber ⊤ ≤ n
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ Nat.succ n ≤ n
convert_to (⊤ : SimpleGraph { m | m < n + 1 }).chromaticNumber ≤ _
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ ⊤ ↪g ⊤
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ chromaticNumber ⊤ ≤ n
refine' (colorable_of_chromaticNumber_pos hc).chromaticNumber_mono_of_embedding _
case f
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ ↑{m | m < n + 1} ↪ V
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ ⊤ ↪g ⊤
apply Embedding.completeGraph
no goals
case f
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ ↑{m | m < n + 1} ↪ V
exact (Function.Embedding.subtype _).trans (Infinite.natEmbedding V)
no goals
case h.e'_3
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ Nat.succ n = chromaticNumber ⊤
rw [SimpleGraph.chromaticNumber_top, Fintype.card_ofFinset,
    Finset.card_range, Nat.succ_eq_add_one]