[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v : V
⊢ partOfVertex P v ∈ P.parts
[PROOFSTEP]
obtain ⟨h, -⟩ := (P.isPartition.2 v).choose_spec.1
[GOAL]
case intro
V : Type u
G : SimpleGraph V
P : Partition G
v : V
h : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts
⊢ partOfVertex P v ∈ P.parts
[PROOFSTEP]
exact h
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v : V
⊢ v ∈ partOfVertex P v
[PROOFSTEP]
obtain ⟨⟨h1, h2⟩, _h3⟩ := (P.isPartition.2 v).choose_spec
[GOAL]
case intro.intro
V : Type u
G : SimpleGraph V
P : Partition G
v : V
_h3 : ∀ (y : Set V), (fun b => ∃! x, v ∈ b) y → y = Exists.choose (_ : ∃! b x, v ∈ b)
h1 : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts
h2 :
  (fun x => v ∈ Exists.choose (_ : ∃! b x, v ∈ b)) h1 ∧
    ∀ (y : Exists.choose (_ : ∃! b x, v ∈ b) ∈ P.parts), (fun x => v ∈ Exists.choose (_ : ∃! b x, v ∈ b)) y → y = h1
⊢ v ∈ partOfVertex P v
[PROOFSTEP]
exact h2.1
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
⊢ partOfVertex P v ≠ partOfVertex P w
[PROOFSTEP]
intro hn
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
⊢ False
[PROOFSTEP]
have hw := P.mem_partOfVertex w
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
hw : w ∈ partOfVertex P w
⊢ False
[PROOFSTEP]
rw [← hn] at hw 
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v w : V
h : Adj G v w
hn : partOfVertex P v = partOfVertex P w
hw : w ∈ partOfVertex P v
⊢ False
[PROOFSTEP]
exact P.independent _ (P.partOfVertex_mem v) (P.mem_partOfVertex v) hw (G.ne_of_adj h) h
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v✝ w✝ : V
hvw : Adj G v✝ w✝
⊢ (fun v => { val := partOfVertex P v, property := (_ : partOfVertex P v ∈ P.parts) }) v✝ ≠
    (fun v => { val := partOfVertex P v, property := (_ : partOfVertex P v ∈ P.parts) }) w✝
[PROOFSTEP]
rw [Ne.def, Subtype.mk_eq_mk]
[GOAL]
V : Type u
G : SimpleGraph V
P : Partition G
v✝ w✝ : V
hvw : Adj G v✝ w✝
⊢ ¬partOfVertex P v✝ = partOfVertex P w✝
[PROOFSTEP]
exact P.partOfVertex_ne_of_adj hvw
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
⊢ ∀ (s : Set V), s ∈ colorClasses C → IsAntichain G.Adj s
[PROOFSTEP]
rintro s ⟨c, rfl⟩
[GOAL]
case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
c : V
⊢ IsAntichain G.Adj {x | Setoid.Rel (Setoid.ker ↑C) x c}
[PROOFSTEP]
apply C.color_classes_independent
[GOAL]
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Partitionable G n ↔ Colorable G n
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Partitionable G n → Colorable G n
[PROOFSTEP]
rintro ⟨P, hf, hc⟩
[GOAL]
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
hc : Finset.card (Set.Finite.toFinset hf) ≤ n
⊢ Colorable G n
[PROOFSTEP]
have : Fintype P.parts := hf.fintype
[GOAL]
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
hc : Finset.card (Set.Finite.toFinset hf) ≤ n
this : Fintype ↑P.parts
⊢ Colorable G n
[PROOFSTEP]
rw [Set.Finite.card_toFinset hf] at hc 
[GOAL]
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
this : Fintype ↑P.parts
hc : Fintype.card ↑P.parts ≤ n
⊢ Colorable G n
[PROOFSTEP]
apply P.to_colorable.mono hc
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Colorable G n → Partitionable G n
[PROOFSTEP]
rintro ⟨C⟩
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
⊢ Partitionable G n
[PROOFSTEP]
refine' ⟨C.toPartition, C.colorClasses_finite, le_trans _ (Fintype.card_fin n).le⟩
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
⊢ Finset.card (Set.Finite.toFinset (_ : Set.Finite (Coloring.colorClasses C))) ≤ Fintype.card (Fin n)
[PROOFSTEP]
generalize_proofs h
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
⊢ Finset.card (Set.Finite.toFinset h) ≤ Fintype.card (Fin n)
[PROOFSTEP]
haveI : Fintype C.colorClasses := C.colorClasses_finite.fintype
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
this : Fintype ↑(Coloring.colorClasses C)
⊢ Finset.card (Set.Finite.toFinset h) ≤ Fintype.card (Fin n)
[PROOFSTEP]
rw [h.card_toFinset]
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
this : Fintype ↑(Coloring.colorClasses C)
⊢ Fintype.card ↑(Coloring.colorClasses C) ≤ Fintype.card (Fin n)
[PROOFSTEP]
exact C.card_colorClasses_le
