-- Mathlib/Combinatorics/SimpleGraph/Partition.lean
theorem partitionable_iff_colorable {n : ℕ} : G.Partitionable n ↔ G.Colorable n

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
⊢ h.toFinset.card ≤ Fintype.card (Fin n)

Tactic:
have : Fintype C.colorClasses := C.colorClasses_finite.fintype

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype ↑C.colorClasses
⊢ h.toFinset.card ≤ Fintype.card (Fin n)

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n ↔ G.Colorable n

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n → G.Colorable n

case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → G.Partitionable n

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype ↑C.colorClasses
⊢ h.toFinset.card ≤ Fintype.card (Fin n)

Tactic:
rw [h.card_toFinset]

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype ↑C.colorClasses
⊢ Fintype.card ↑C.colorClasses ≤ Fintype.card (Fin n)

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.toPartition.parts.Finite
⊢ h.toFinset.card ≤ Fintype.card (Fin n)

Tactic:
change Set.Finite (Coloring.colorClasses C) at h

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
⊢ h.toFinset.card ≤ Fintype.card (Fin n)

Proof state:
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset.card ≤ n
this : Fintype ↑P.parts
⊢ G.Colorable n

Tactic:
rw [Set.Finite.card_toFinset hf] at hc

Result:
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
this : Fintype ↑P.parts
hc : Fintype.card ↑P.parts ≤ n
⊢ G.Colorable n

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype ↑C.colorClasses
⊢ Fintype.card ↑C.colorClasses ≤ Fintype.card (Fin n)

Tactic:
exact C.card_colorClasses_le

Result:
no goals

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ G.Partitionable n

Tactic:
refine ⟨C.toPartition, C.colorClasses_finite, le_trans ?_ (Fintype.card_fin n).le⟩

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ ⋯.toFinset.card ≤ Fintype.card (Fin n)

Proof state:
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
this : Fintype ↑P.parts
hc : Fintype.card ↑P.parts ≤ n
⊢ G.Colorable n

Tactic:
apply P.colorable.mono hc

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n → G.Colorable n

Tactic:
rintro ⟨P, hf, hc⟩

Result:
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset.card ≤ n
⊢ G.Colorable n

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ ⋯.toFinset.card ≤ Fintype.card (Fin n)

Tactic:
generalize_proofs h

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.toPartition.parts.Finite
⊢ h.toFinset.card ≤ Fintype.card (Fin n)

Proof state:
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset.card ≤ n
⊢ G.Colorable n

Tactic:
have : Fintype P.parts := hf.fintype

Result:
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset.card ≤ n
this : Fintype ↑P.parts
⊢ G.Colorable n

Proof state:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → G.Partitionable n

Tactic:
rintro ⟨C⟩

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ G.Partitionable n