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

case mpr
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ (∃ C, ∀ (v : V), ↑C v < n) → Colorable G n
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ Colorable G n ↔ ∃ C, ∀ (v : V), ↑C v < n
constructor
case mp
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ ∃ C, ∀ (v : V), ↑C v < n
case mp
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ Colorable G n → ∃ C, ∀ (v : V), ↑C v < n
rintro hc
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
case mp
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ ∃ C, ∀ (v : V), ↑C v < n
have C : G.Coloring (Fin n) := hc.toColoring (by simp)
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
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
let f := Embedding.completeGraph (@Fin.valEmbedding n)
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
⊢ ∀ (v : V), ↑(Hom.comp (Embedding.toHom f) C) v < n
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
use f.toHom.comp C
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
v : V
⊢ ↑(Hom.comp (Embedding.toHom f) C) v < n
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
⊢ ∀ (v : V), ↑(Hom.comp (Embedding.toHom f) C) v < n
intro v
case mp.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
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
v : V
⊢ ↑(Hom.comp (Embedding.toHom f) C) v < n
cases' C with color valid
no goals
case mp.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
exact Fin.is_lt (color v)
no goals
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ n ≤ Fintype.card (Fin n)
simp
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
case mpr
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ (∃ C, ∀ (v : V), ↑C v < n) → Colorable G n
rintro ⟨C, Cf⟩
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

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 → ?mpr.intro.refine'_1 v ≠ ?mpr.intro.refine'_1 w
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
refine' ⟨Coloring.mk _ _⟩
no goals
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
exact fun v => ⟨C v, Cf v⟩
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) }
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) }
rintro v w hvw
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
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) }
simp only [Fin.mk_eq_mk, Ne.def]
no goals
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
exact C.valid hvw