[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype.card ↑(colorClasses C) ≤ Fintype.card α
[PROOFSTEP]
simp [colorClasses]
  -- porting note: brute force instance declaration `[Fintype (Setoid.classes (Setoid.ker C))]`
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype.card ↑(Setoid.classes (Setoid.ker ↑C)) ≤ Fintype.card α
[PROOFSTEP]
haveI : Fintype (Setoid.classes (Setoid.ker C)) := by assumption
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype ↑(Setoid.classes (Setoid.ker ↑C))
[PROOFSTEP]
assumption
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
this : Fintype ↑(Setoid.classes (Setoid.ker ↑C))
⊢ Fintype.card ↑(Setoid.classes (Setoid.ker ↑C)) ≤ Fintype.card α
[PROOFSTEP]
convert Setoid.card_classes_ker_le C
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype V
inst✝ : Fintype α
⊢ Fintype (Coloring G α)
[PROOFSTEP]
classical
change Fintype (RelHom G.Adj (⊤ : SimpleGraph α).Adj)
apply Fintype.ofInjective _ RelHom.coe_fn_injective
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype V
inst✝ : Fintype α
⊢ Fintype (Coloring G α)
[PROOFSTEP]
change Fintype (RelHom G.Adj (⊤ : SimpleGraph α).Adj)
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype V
inst✝ : Fintype α
⊢ Fintype (G.Adj →r ⊤.Adj)
[PROOFSTEP]
apply Fintype.ofInjective _ RelHom.coe_fn_injective
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
⊢ IsEmpty V
[PROOFSTEP]
constructor
[GOAL]
case false
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
⊢ V → False
[PROOFSTEP]
intro v
[GOAL]
case false
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
v : V
⊢ False
[PROOFSTEP]
obtain ⟨i, hi⟩ := h.some v
[GOAL]
case false.mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
v : V
i : ℕ
hi : i < 0
⊢ False
[PROOFSTEP]
exact Nat.not_lt_zero _ hi
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
⊢ Function.Injective fun C => Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C
[PROOFSTEP]
intro C C' h
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h :
  (fun C => Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C) C =
    (fun C => Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C) C'
⊢ C = C'
[PROOFSTEP]
dsimp only at h 
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
⊢ C = C'
[PROOFSTEP]
ext v
[GOAL]
case h
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
v : V
⊢ ↑C v = ↑C' v
[PROOFSTEP]
apply (Embedding.completeGraph f).inj'
[GOAL]
case h.a
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
v : V
⊢ Function.Embedding.toFun (Embedding.completeGraph f).toEmbedding (↑C v) =
    Function.Embedding.toFun (Embedding.completeGraph f).toEmbedding (↑C' v)
[PROOFSTEP]
change ((Embedding.completeGraph f).toHom.comp C) v = _
[GOAL]
case h.a
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
v : V
⊢ ↑(Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C) v =
    Function.Embedding.toFun (Embedding.completeGraph f).toEmbedding (↑C' v)
[PROOFSTEP]
rw [h]
[GOAL]
case h.a
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
v : V
⊢ ↑(Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C') v =
    Function.Embedding.toFun (Embedding.completeGraph f).toEmbedding (↑C' v)
[PROOFSTEP]
rfl
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ≃ β
C : Coloring G α
⊢ ↑(recolorOfEmbedding G (Equiv.toEmbedding f.symm)) (↑(recolorOfEmbedding G (Equiv.toEmbedding f)) C) = C
[PROOFSTEP]
ext v
[GOAL]
case h
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ≃ β
C : Coloring G α
v : V
⊢ ↑(↑(recolorOfEmbedding G (Equiv.toEmbedding f.symm)) (↑(recolorOfEmbedding G (Equiv.toEmbedding f)) C)) v = ↑C v
[PROOFSTEP]
apply Equiv.symm_apply_apply
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ≃ β
C : Coloring G β
⊢ ↑(recolorOfEmbedding G (Equiv.toEmbedding f)) (↑(recolorOfEmbedding G (Equiv.toEmbedding f.symm)) C) = C
[PROOFSTEP]
ext v
[GOAL]
case h
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ≃ β
C : Coloring G β
v : V
⊢ ↑(↑(recolorOfEmbedding G (Equiv.toEmbedding f)) (↑(recolorOfEmbedding G (Equiv.toEmbedding f.symm)) C)) v = ↑C v
[PROOFSTEP]
apply Equiv.apply_symm_apply
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n m : ℕ
h : n ≤ m
hc : Colorable G n
⊢ Fintype.card (Fin n) ≤ Fintype.card (Fin m)
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
⊢ Fintype.card α ≤ Fintype.card (Fin (Fintype.card α))
[PROOFSTEP]
simp
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype α
n : ℕ
hc : Colorable G n
hn : n ≤ Fintype.card α
⊢ Coloring G α
[PROOFSTEP]
rw [← Fintype.card_fin n] at hn 
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype α
n : ℕ
hc : Colorable G n
hn : Fintype.card (Fin n) ≤ Fintype.card α
⊢ Coloring G α
[PROOFSTEP]
exact G.recolorOfCardLE hn hc.some
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
f : G ↪g G'
n : ℕ
h : Colorable G' n
⊢ n ≤ Fintype.card (Fin n)
[PROOFSTEP]
simp
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ Colorable G n ↔ ∃ C, ∀ (v : V), ↑C v < n
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ Colorable G n → ∃ C, ∀ (v : V), ↑C v < n
[PROOFSTEP]
rintro hc
[GOAL]
case mp
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ ∃ C, ∀ (v : V), ↑C v < n
[PROOFSTEP]
have C : G.Coloring (Fin n) := hc.toColoring (by simp)
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ n ≤ Fintype.card (Fin n)
[PROOFSTEP]
simp
[GOAL]
case mp
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
n : ℕ
hc : Colorable G n
C : Coloring G (Fin n)
⊢ ∃ C, ∀ (v : V), ↑C v < n
[PROOFSTEP]
let f := Embedding.completeGraph (@Fin.valEmbedding n)
[GOAL]
case mp
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
n : ℕ
hc : Colorable G n
C : Coloring G (Fin n)
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
⊢ ∃ C, ∀ (v : V), ↑C v < n
[PROOFSTEP]
use f.toHom.comp C
[GOAL]
case h
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
n : ℕ
hc : Colorable G n
C : Coloring G (Fin n)
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
⊢ ∀ (v : V), ↑(Hom.comp (Embedding.toHom f) C) v < n
[PROOFSTEP]
intro v
[GOAL]
case h
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
n : ℕ
hc : Colorable G n
C : Coloring G (Fin n)
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
v : V
⊢ ↑(Hom.comp (Embedding.toHom f) C) v < n
[PROOFSTEP]
cases' C with color valid
[GOAL]
case h.mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
v : V
color : V → Fin n
valid : ∀ {a b : V}, Adj G a b → Adj ⊤ (color a) (color b)
⊢ ↑(Hom.comp (Embedding.toHom f) { toFun := color, map_rel' := valid }) v < n
[PROOFSTEP]
exact Fin.is_lt (color v)
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ (∃ C, ∀ (v : V), ↑C v < n) → Colorable G n
[PROOFSTEP]
rintro ⟨C, Cf⟩
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
n : ℕ
C : Coloring G ℕ
Cf : ∀ (v : V), ↑C v < n
⊢ Colorable G n
[PROOFSTEP]
refine' ⟨Coloring.mk _ _⟩
[GOAL]
case mpr.intro.refine'_1
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
n : ℕ
C : Coloring G ℕ
Cf : ∀ (v : V), ↑C v < n
⊢ V → Fin n
[PROOFSTEP]
exact fun v => ⟨C v, Cf v⟩
[GOAL]
case mpr.intro.refine'_2
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
n : ℕ
C : Coloring G ℕ
Cf : ∀ (v : V), ↑C v < n
⊢ ∀ {v w : V}, Adj G v w → { val := ↑C v, isLt := (_ : ↑C v < n) } ≠ { val := ↑C w, isLt := (_ : ↑C w < n) }
[PROOFSTEP]
rintro v w hvw
[GOAL]
case mpr.intro.refine'_2
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
n : ℕ
C : Coloring G ℕ
Cf : ∀ (v : V), ↑C v < n
v w : V
hvw : Adj G v w
⊢ { val := ↑C v, isLt := (_ : ↑C v < n) } ≠ { val := ↑C w, isLt := (_ : ↑C w < n) }
[PROOFSTEP]
simp only [Fin.mk_eq_mk, Ne.def]
[GOAL]
case mpr.intro.refine'_2
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
n : ℕ
C : Coloring G ℕ
Cf : ∀ (v : V), ↑C v < n
v w : V
hvw : Adj G v w
⊢ ¬↑C v = ↑C w
[PROOFSTEP]
exact C.valid hvw
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ chromaticNumber G ≤ n
[PROOFSTEP]
rw [chromaticNumber]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ sInf {n | Colorable G n} ≤ n
[PROOFSTEP]
apply csInf_le chromaticNumber_bddBelow
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ n ∈ {n | Colorable G n}
[PROOFSTEP]
constructor
[GOAL]
case val
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ Coloring G (Fin n)
[PROOFSTEP]
exact Classical.choice hc
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
classical
dsimp only [chromaticNumber]
rw [Nat.sInf_def]
apply Nat.find_spec
exact colorable_set_nonempty_of_colorable hc
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
dsimp only [chromaticNumber]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (sInf {n | Colorable G n})
[PROOFSTEP]
rw [Nat.sInf_def]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (Nat.find ?m.140369)
V : Type u G : SimpleGraph V α : Type v C : Coloring G α m : ℕ hc : Colorable G m ⊢ Set.Nonempty {n | Colorable G n}
[PROOFSTEP]
apply Nat.find_spec
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Set.Nonempty {n | Colorable G n}
[PROOFSTEP]
exact colorable_set_nonempty_of_colorable hc
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
cases nonempty_fintype V
[GOAL]
case intro
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
exact colorable_chromaticNumber G.colorable_of_fintype
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ chromaticNumber G ≤ 1
[PROOFSTEP]
rw [chromaticNumber]
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ sInf {n | Colorable G n} ≤ 1
[PROOFSTEP]
apply csInf_le chromaticNumber_bddBelow
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ 1 ∈ {n | Colorable G n}
[PROOFSTEP]
constructor
[GOAL]
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ Coloring G (Fin 1)
[PROOFSTEP]
refine' Coloring.mk (fun _ => 0) _
[GOAL]
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ ∀ {v w : V}, Adj G v w → (fun x => 0) v ≠ (fun x => 0) w
[PROOFSTEP]
intro v w
[GOAL]
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ Adj G v w → (fun x => 0) v ≠ (fun x => 0) w
[PROOFSTEP]
rw [Subsingleton.elim v w]
[GOAL]
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ Adj G w w → (fun x => 0) w ≠ (fun x => 0) w
[PROOFSTEP]
simp
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ chromaticNumber G = 0
[PROOFSTEP]
rw [← nonpos_iff_eq_zero]
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ chromaticNumber G ≤ 0
[PROOFSTEP]
apply csInf_le chromaticNumber_bddBelow
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ 0 ∈ {n | Colorable G n}
[PROOFSTEP]
apply colorable_of_isEmpty
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
h : chromaticNumber G = 0
⊢ IsEmpty V
[PROOFSTEP]
have h' := G.colorable_chromaticNumber_of_fintype
[GOAL]
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
[PROOFSTEP]
rw [h] at h' 
[GOAL]
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
[PROOFSTEP]
exact G.isEmpty_of_colorable_zero h'
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
⊢ 0 < chromaticNumber G
[PROOFSTEP]
apply le_csInf (colorable_set_nonempty_of_colorable hc)
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
⊢ ∀ (b : ℕ), b ∈ {n | Colorable G n} → Nat.succ 0 ≤ b
[PROOFSTEP]
intro m hm
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
⊢ Nat.succ 0 ≤ m
[PROOFSTEP]
by_contra h'
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : ¬Nat.succ 0 ≤ m
⊢ False
[PROOFSTEP]
simp only [not_le] at h' 
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
⊢ False
[PROOFSTEP]
obtain ⟨i, hi⟩ := hm.some (Classical.arbitrary V)
[GOAL]
case mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
⊢ False
[PROOFSTEP]
have h₁ : i < 0 := lt_of_lt_of_le hi (Nat.le_of_lt_succ h')
[GOAL]
case mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
h₁ : i < 0
⊢ False
[PROOFSTEP]
exact Nat.not_lt_zero _ h₁
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : 0 < chromaticNumber G
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
obtain ⟨h, hn⟩ := Nat.nonempty_of_pos_sInf h
[GOAL]
case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h✝ : 0 < chromaticNumber G
h : ℕ
hn : h ∈ {n | Colorable G n}
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
exact colorable_chromaticNumber hn
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ chromaticNumber G ≤ chromaticNumber G'
[PROOFSTEP]
apply csInf_le chromaticNumber_bddBelow
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ chromaticNumber G' ∈ {n | Colorable G n}
[PROOFSTEP]
apply h
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ Colorable G' (chromaticNumber G')
[PROOFSTEP]
apply colorable_chromaticNumber hc
[GOAL]
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 α
[PROOFSTEP]
apply le_antisymm
[GOAL]
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 α
[PROOFSTEP]
apply chromaticNumber_le_card C
[GOAL]
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
[PROOFSTEP]
by_contra hc
[GOAL]
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
[PROOFSTEP]
rw [not_le] at hc 
[GOAL]
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
[PROOFSTEP]
obtain ⟨n, cn, hc⟩ := exists_lt_of_csInf_lt (colorable_set_nonempty_of_colorable C.to_colorable) hc
[GOAL]
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
[PROOFSTEP]
rw [← Fintype.card_fin n] at hc 
[GOAL]
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
[PROOFSTEP]
have f := (Function.Embedding.nonempty_of_card_le (le_of_lt hc)).some
[GOAL]
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
[PROOFSTEP]
have C' := cn.some
[GOAL]
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
[PROOFSTEP]
specialize h (G.recolorOfEmbedding f C')
[GOAL]
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
[PROOFSTEP]
have h1 : Function.Surjective f := Function.Surjective.of_comp h
[GOAL]
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
[PROOFSTEP]
have h2 := Fintype.card_le_of_surjective _ h1
[GOAL]
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
[PROOFSTEP]
exact Nat.lt_le_antisymm hc h2
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
⊢ chromaticNumber ⊥ = 1
[PROOFSTEP]
let C : (⊥ : SimpleGraph V).Coloring (Fin 1) := Coloring.mk (fun _ => 0) fun {v w} h => False.elim h
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ chromaticNumber ⊥ = 1
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ chromaticNumber ⊥ ≤ 1
[PROOFSTEP]
exact chromaticNumber_le_card C
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ 1 ≤ chromaticNumber ⊥
[PROOFSTEP]
exact chromaticNumber_pos C.to_colorable
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype V
⊢ chromaticNumber ⊤ = Fintype.card V
[PROOFSTEP]
apply chromaticNumber_eq_card_of_forall_surj (selfColoring _)
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype V
⊢ ∀ (C' : Coloring ⊤ V), Function.Surjective ↑C'
[PROOFSTEP]
intro C
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
⊢ Function.Surjective ↑C
[PROOFSTEP]
rw [← Finite.injective_iff_surjective]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
⊢ Function.Injective ↑C
[PROOFSTEP]
intro v w
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
⊢ ↑C v = ↑C w → v = w
[PROOFSTEP]
contrapose
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
⊢ ¬v = w → ¬↑C v = ↑C w
[PROOFSTEP]
intro h
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
h : ¬v = w
⊢ ¬↑C v = ↑C w
[PROOFSTEP]
exact C.valid h
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
⊢ chromaticNumber ⊤ = 0
[PROOFSTEP]
let n := (⊤ : SimpleGraph V).chromaticNumber
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
⊢ chromaticNumber ⊤ = 0
[PROOFSTEP]
by_contra hc
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : ¬chromaticNumber ⊤ = 0
⊢ False
[PROOFSTEP]
replace hc := pos_iff_ne_zero.mpr hc
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ False
[PROOFSTEP]
apply Nat.not_succ_le_self n
[GOAL]
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
[PROOFSTEP]
convert_to (⊤ : SimpleGraph {m | m < n + 1}).chromaticNumber ≤ _
[GOAL]
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 ⊤
[PROOFSTEP]
rw [SimpleGraph.chromaticNumber_top, Fintype.card_ofFinset, Finset.card_range, Nat.succ_eq_add_one]
[GOAL]
case convert_2
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
[PROOFSTEP]
refine' (colorable_of_chromaticNumber_pos hc).chromaticNumber_mono_of_embedding _
[GOAL]
case convert_2
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ ⊤ ↪g ⊤
[PROOFSTEP]
apply Embedding.completeGraph
[GOAL]
case convert_2.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
[PROOFSTEP]
exact (Function.Embedding.subtype _).trans (Infinite.natEmbedding V)
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
⊢ ∀ {v w : V ⊕ W}, Adj (completeBipartiteGraph V W) v w → (fun v => Sum.isRight v) v ≠ (fun v => Sum.isRight v) w
[PROOFSTEP]
intro v w
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
v w : V ⊕ W
⊢ Adj (completeBipartiteGraph V W) v w → (fun v => Sum.isRight v) v ≠ (fun v => Sum.isRight v) w
[PROOFSTEP]
cases v
[GOAL]
case inl
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
w : V ⊕ W
val✝ : V
⊢ Adj (completeBipartiteGraph V W) (Sum.inl val✝) w →
    (fun v => Sum.isRight v) (Sum.inl val✝) ≠ (fun v => Sum.isRight v) w
[PROOFSTEP]
cases w
[GOAL]
case inr
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
w : V ⊕ W
val✝ : W
⊢ Adj (completeBipartiteGraph V W) (Sum.inr val✝) w →
    (fun v => Sum.isRight v) (Sum.inr val✝) ≠ (fun v => Sum.isRight v) w
[PROOFSTEP]
cases w
[GOAL]
case inl.inl
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
val✝¹ val✝ : V
⊢ Adj (completeBipartiteGraph V W) (Sum.inl val✝¹) (Sum.inl val✝) →
    (fun v => Sum.isRight v) (Sum.inl val✝¹) ≠ (fun v => Sum.isRight v) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case inl.inr
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
val✝¹ : V
val✝ : W
⊢ Adj (completeBipartiteGraph V W) (Sum.inl val✝¹) (Sum.inr val✝) →
    (fun v => Sum.isRight v) (Sum.inl val✝¹) ≠ (fun v => Sum.isRight v) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
case inr.inl
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
val✝¹ : W
val✝ : V
⊢ Adj (completeBipartiteGraph V W) (Sum.inr val✝¹) (Sum.inl val✝) →
    (fun v => Sum.isRight v) (Sum.inr val✝¹) ≠ (fun v => Sum.isRight v) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case inr.inr
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
val✝¹ val✝ : W
⊢ Adj (completeBipartiteGraph V W) (Sum.inr val✝¹) (Sum.inr val✝) →
    (fun v => Sum.isRight v) (Sum.inr val✝¹) ≠ (fun v => Sum.isRight v) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ SimpleGraph.chromaticNumber (completeBipartiteGraph V W) = 2
[PROOFSTEP]
apply chromaticNumber_eq_card_of_forall_surj (CompleteBipartiteGraph.bicoloring V W)
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ ∀ (C' : Coloring (completeBipartiteGraph V W) Bool), Function.Surjective ↑C'
[PROOFSTEP]
intro C b
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
⊢ ∃ a, ↑C a = b
[PROOFSTEP]
have v := Classical.arbitrary V
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
⊢ ∃ a, ↑C a = b
[PROOFSTEP]
have w := Classical.arbitrary W
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
⊢ ∃ a, ↑C a = b
[PROOFSTEP]
have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
⊢ Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
[PROOFSTEP]
simp
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
⊢ ∃ a, ↑C a = b
[PROOFSTEP]
have hn := C.valid h
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
⊢ ∃ a, ↑C a = b
[PROOFSTEP]
by_cases he : C (Sum.inl v) = b
[GOAL]
case pos
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ↑C (Sum.inl v) = b
⊢ ∃ a, ↑C a = b
[PROOFSTEP]
exact ⟨_, he⟩
[GOAL]
case neg
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
⊢ ∃ a, ↑C a = b
[PROOFSTEP]
by_cases he' : C (Sum.inr w) = b
[GOAL]
case pos
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
he' : ↑C (Sum.inr w) = b
⊢ ∃ a, ↑C a = b
[PROOFSTEP]
exact ⟨_, he'⟩
[GOAL]
case neg
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
he' : ¬↑C (Sum.inr w) = b
⊢ ∃ a, ↑C a = b
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
he' : ¬↑C (Sum.inr w) = b
⊢ False
[PROOFSTEP]
cases b
[GOAL]
case neg.h.false
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = false
he' : ¬↑C (Sum.inr w) = false
⊢ False
[PROOFSTEP]
simp only [Bool.eq_true_eq_not_eq_false, Bool.eq_false_eq_not_eq_true] at he he' 
[GOAL]
case neg.h.true
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = true
he' : ¬↑C (Sum.inr w) = true
⊢ False
[PROOFSTEP]
simp only [Bool.eq_true_eq_not_eq_false, Bool.eq_false_eq_not_eq_true] at he he' 
[GOAL]
case neg.h.false
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ↑C (Sum.inl v) = true
he' : ↑C (Sum.inr w) = true
⊢ False
[PROOFSTEP]
rw [he, he'] at hn 
[GOAL]
case neg.h.true
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ↑C (Sum.inl v) = false
he' : ↑C (Sum.inr w) = false
⊢ False
[PROOFSTEP]
rw [he, he'] at hn 
[GOAL]
case neg.h.false
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : true ≠ true
he : ↑C (Sum.inl v) = true
he' : ↑C (Sum.inr w) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg.h.true
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : false ≠ false
he : ↑C (Sum.inl v) = false
he' : ↑C (Sum.inr w) = false
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : IsClique G ↑s
inst✝ : Fintype α
C : Coloring G α
⊢ Finset.card s ≤ Fintype.card α
[PROOFSTEP]
rw [isClique_iff_induce_eq] at h 
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
⊢ Finset.card s ≤ Fintype.card α
[PROOFSTEP]
have f : G.induce ↑s ↪g G := Embedding.comap (Function.Embedding.subtype fun x => x ∈ ↑s) G
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : induce (↑s) G ↪g G
⊢ Finset.card s ≤ Fintype.card α
[PROOFSTEP]
rw [h] at f 
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : ⊤ ↪g G
⊢ Finset.card s ≤ Fintype.card α
[PROOFSTEP]
convert Fintype.card_le_of_injective _ (C.comp f.toHom).injective_of_top_hom using 1
[GOAL]
case h.e'_3
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : ⊤ ↪g G
⊢ Finset.card s = Fintype.card ↑↑s
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
convert h.card_le_of_coloring hc.some
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Finite V
s : Finset V
h : IsClique G ↑s
⊢ Finset.card s ≤ chromaticNumber G
[PROOFSTEP]
cases nonempty_fintype V
[GOAL]
case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Finite V
s : Finset V
h : IsClique G ↑s
val✝ : Fintype V
⊢ Finset.card s ≤ chromaticNumber G
[PROOFSTEP]
exact h.card_le_of_colorable G.colorable_chromaticNumber_of_fintype
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n m : ℕ
hc : Colorable G n
hm : n < m
⊢ CliqueFree G m
[PROOFSTEP]
by_contra h
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n m : ℕ
hc : Colorable G n
hm : n < m
h : ¬CliqueFree G m
⊢ False
[PROOFSTEP]
simp only [CliqueFree, isNClique_iff, not_forall, Classical.not_not] at h 
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n m : ℕ
hc : Colorable G n
hm : n < m
h : ∃ x, IsClique G ↑x ∧ Finset.card x = m
⊢ False
[PROOFSTEP]
obtain ⟨s, h, rfl⟩ := h
[GOAL]
case intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
s : Finset V
h : IsClique G ↑s
hm : n < Finset.card s
⊢ False
[PROOFSTEP]
exact Nat.lt_le_antisymm hm (h.card_le_of_colorable hc)
