-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem colorable_iff_exists_bdd_nat_coloring (n : ℕ) :
    G.Colorable n ↔ ∃ C : G.Coloring ℕ, ∀ v, C v < n

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ G.Colorable n

Tactic:
refine ⟨Coloring.mk ?_ ?_⟩

Result:
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ V → Fin n

case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ ∀ {v w : V}, G.Adj v w → ?mpr.intro.refine_1 v ≠ ?mpr.intro.refine_1 w

Proof state:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (∃ C, ∀ (v : V), C v < n) → G.Colorable n

Tactic:
rintro ⟨C, Cf⟩

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ G.Colorable n

Proof state:
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ V → Fin n

Tactic:
exact fun v => ⟨C v, Cf v⟩

Result:
no goals

Proof state:
case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
v w : V
hvw : G.Adj v w
⊢ ⟨C v, ⋯⟩ ≠ ⟨C w, ⋯⟩

Tactic:
simp only [Fin.mk_eq_mk, Ne]

Result:
case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
v w : V
hvw : G.Adj v w
⊢ ¬C v = C w

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ n ≤ card (Fin n)

Tactic:
simp

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ ∃ C, ∀ (v : V), C v < n

Tactic:
have C : G.Coloring (Fin n) := hc.toColoring (by simp)

Result:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
⊢ ∃ C, ∀ (v : V), C v < n

Proof state:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
⊢ ∃ C, ∀ (v : V), C v < n

Tactic:
let f := Embedding.completeGraph (@Fin.valEmbedding n)

Result:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
⊢ ∃ C, ∀ (v : V), C v < n

Proof state:
case h
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
v : V
⊢ (f.toHom.comp C) v < n

Tactic:
exact Fin.is_lt (C.1 v)

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
⊢ ∃ C, ∀ (v : V), C v < n

Tactic:
use f.toHom.comp C

Result:
case h
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
⊢ ∀ (v : V), (f.toHom.comp C) v < n

Proof state:
case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
v w : V
hvw : G.Adj v w
⊢ ¬C v = C w

Tactic:
exact C.valid hvw

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → ∃ C, ∀ (v : V), C v < n

Tactic:
rintro hc

Result:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ ∃ C, ∀ (v : V), C v < n

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n ↔ ∃ C, ∀ (v : V), C v < n

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → ∃ C, ∀ (v : V), C v < n

case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (∃ C, ∀ (v : V), C v < n) → G.Colorable n

Proof state:
case h
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
⊢ ∀ (v : V), (f.toHom.comp C) v < n

Tactic:
intro v

Result:
case h
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : ⊤ ↪g ⊤ := Embedding.completeGraph Fin.valEmbedding
v : V
⊢ (f.toHom.comp C) v < n

Proof state:
case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ ∀ {v w : V}, G.Adj v w → ⟨C v, ⋯⟩ ≠ ⟨C w, ⋯⟩

Tactic:
rintro v w hvw

Result:
case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
v w : V
hvw : G.Adj v w
⊢ ⟨C v, ⋯⟩ ≠ ⟨C w, ⋯⟩