-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
lemma card_le_chromaticNumber_iff_forall_surjective [Fintype α] :
    card α ≤ G.chromaticNumber ↔ ∀ C : G.Coloring α, Surjective C

Proof state:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
⊢ ∃ a, C a = i

Tactic:
by_contra! hi

Result:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
⊢ card (Fin i) ≤ card α

Tactic:
simpa using h.le

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
D : G.Coloring { a // a ≠ i } := { toFun := fun v => ⟨C v, ⋯⟩, map_rel' := ⋯ }
⊢ card { a // a ≠ i } = card (Fin (card α - 1))

Tactic:
simp [Nat.pred_eq_sub_one]

Result:
no goals

Proof state:
case refine_2.intro
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
hC : Surjective (⇑⋯.some ∘ ⇑C)
⊢ False

Tactic:
simpa [h.not_le] using Fintype.card_le_of_surjective _ hC.of_comp

Result:
no goals

Proof state:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
⊢ Surjective ⇑C

Tactic:
intro i

Result:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
⊢ ∃ a, C a = i

Proof state:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
D : G.Coloring { a // a ≠ i } := { toFun := fun v => ⟨C v, ⋯⟩, map_rel' := ⋯ }
⊢ False

Tactic:
classical
exact Nat.not_mem_of_lt_sInf ((Nat.sub_one_lt_of_lt <| card_pos_iff.2 ⟨i⟩).trans_le h)
  ⟨G.recolorOfEquiv (equivOfCardEq <| by simp [Nat.pred_eq_sub_one]) D⟩

Result:
no goals

Proof state:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
D : G.Coloring { a // a ≠ i } := { toFun := fun v => ⟨C v, ⋯⟩, map_rel' := ⋯ }
⊢ False

Tactic:
exact Nat.not_mem_of_lt_sInf ((Nat.sub_one_lt_of_lt <| card_pos_iff.2 ⟨i⟩).trans_le h)
  ⟨G.recolorOfEquiv (equivOfCardEq <| by simp [Nat.pred_eq_sub_one]) D⟩

Result:
no goals

Proof state:
case refine_2.intro
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
⊢ ∃ C, ¬Surjective ⇑C

Tactic:
refine ⟨G.recolorOfCardLE (by simpa using h.le) C, fun hC ↦ ?_⟩

Result:
case refine_2.intro
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
hC : Surjective ⇑((G.recolorOfCardLE ⋯) C)
⊢ False

Proof state:
case refine_2
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : ∀ (C : G.Coloring α), Surjective ⇑C
⊢ ∀ (i : ℕ), G.Colorable i → card α ≤ i

Tactic:
rintro i ⟨C⟩

Result:
case refine_2.intro
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : ∀ (C : G.Coloring α), Surjective ⇑C
i : ℕ
C : G.Coloring (Fin i)
⊢ card α ≤ i

Proof state:
case refine_2
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : ∀ (C : G.Coloring α), Surjective ⇑C
⊢ ↑(card α) ≤ G.chromaticNumber

Tactic:
simp only [chromaticNumber, Set.mem_setOf_eq, le_iInf_iff, Nat.cast_le, exists_prop]

Result:
case refine_2
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : ∀ (C : G.Coloring α), Surjective ⇑C
⊢ ∀ (i : ℕ), G.Colorable i → card α ≤ i

Proof state:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : ↑(card α) ≤ G.chromaticNumber
C : G.Coloring α
⊢ Surjective ⇑C

Tactic:
rw [C.colorable.chromaticNumber_eq_sInf, Nat.cast_le] at h

Result:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
⊢ Surjective ⇑C

Proof state:
case refine_2.intro
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
hC : Surjective ⇑((G.recolorOfCardLE ⋯) C)
⊢ False

Tactic:
dsimp at hC

Result:
case refine_2.intro
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
hC : Surjective (⇑⋯.some ∘ ⇑C)
⊢ False

Proof state:
case refine_2.intro
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : ∀ (C : G.Coloring α), Surjective ⇑C
i : ℕ
C : G.Coloring (Fin i)
⊢ card α ≤ i

Tactic:
contrapose! h

Result:
case refine_2.intro
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
⊢ ∃ C, ¬Surjective ⇑C

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
⊢ ↑(card α) ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring α), Surjective ⇑C

Tactic:
refine ⟨fun h C ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : ↑(card α) ≤ G.chromaticNumber
C : G.Coloring α
⊢ Surjective ⇑C

case refine_2
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
h : ∀ (C : G.Coloring α), Surjective ⇑C
⊢ ↑(card α) ≤ G.chromaticNumber