case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
⊢ chromaticNumber G ≤ Fintype.card α

case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
⊢ Fintype.card α ≤ chromaticNumber G
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
⊢ chromaticNumber G = Fintype.card α
apply le_antisymm
no goals
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
⊢ chromaticNumber G ≤ Fintype.card α
apply chromaticNumber_le_card C
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc : ¬Fintype.card α ≤ chromaticNumber G
⊢ False
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
⊢ Fintype.card α ≤ chromaticNumber G
by_contra hc
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc : chromaticNumber G < Fintype.card α
⊢ False
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc : ¬Fintype.card α ≤ chromaticNumber G
⊢ False
rw [not_le] at hc
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : n < Fintype.card α
⊢ False
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc : chromaticNumber G < Fintype.card α
⊢ False
obtain ⟨n, cn, hc⟩ :=
  exists_lt_of_csInf_lt (colorable_set_nonempty_of_colorable C.to_colorable) hc
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
⊢ False
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : n < Fintype.card α
⊢ False
rw [← Fintype.card_fin n] at hc
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
⊢ False
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
⊢ False
have f := (Function.Embedding.nonempty_of_card_le (le_of_lt hc)).some
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
⊢ False
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
⊢ False
have C' := cn.some
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
h : Function.Surjective ↑(↑(recolorOfEmbedding G f) C')
⊢ False
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
⊢ False
specialize h (G.recolorOfEmbedding f C')
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
h : Function.Surjective ↑(↑(recolorOfEmbedding G f) C')
h1 : Function.Surjective ↑f
⊢ False
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
h : Function.Surjective ↑(↑(recolorOfEmbedding G f) C')
⊢ False
have h1 : Function.Surjective f := Function.Surjective.of_comp h
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
h : Function.Surjective ↑(↑(recolorOfEmbedding G f) C')
h1 : Function.Surjective ↑f
h2 : Fintype.card α ≤ Fintype.card (Fin n)
⊢ False
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
h : Function.Surjective ↑(↑(recolorOfEmbedding G f) C')
h1 : Function.Surjective ↑f
⊢ False
have h2 := Fintype.card_le_of_surjective _ h1
no goals
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
h : Function.Surjective ↑(↑(recolorOfEmbedding G f) C')
h1 : Function.Surjective ↑f
h2 : Fintype.card α ≤ Fintype.card (Fin n)
⊢ False
exact Nat.lt_le_antisymm hc h2