-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem CompleteBipartiteGraph.chromaticNumber {V W : Type*} [Nonempty V] [Nonempty W] :
    (completeBipartiteGraph V W).chromaticNumber = 2

Proof state:
case neg
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
⊢ ∃ a, C a = b

Tactic:
by_cases he' : C (Sum.inr w) = b

Result:
case pos
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : C (Sum.inr w) = b
⊢ ∃ a, C a = b

case neg
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : ¬C (Sum.inr w) = b
⊢ ∃ a, C a = b

Proof state:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)

Tactic:
simp

Result:
no goals

Proof state:
case pos
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : C (Sum.inr w) = b
⊢ ∃ a, C a = b

Tactic:
exact ⟨_, he'⟩

Result:
no goals

Proof state:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ ∀ (C : (completeBipartiteGraph V W).Coloring (Fin 2)), Surjective ⇑C

Tactic:
intro C b

Result:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
⊢ ∃ a, C a = b

Proof state:
case neg
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : ¬C (Sum.inr w) = b
⊢ ∃ a, C a = b

Tactic:
simpa using two_lt_card_iff.2 ⟨_, _, _, C.valid h, he, he'⟩

Result:
no goals

Proof state:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
⊢ ∃ a, C a = b

Tactic:
have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp

Result:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
⊢ ∃ a, C a = b

Proof state:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ (completeBipartiteGraph V W).Colorable 2

Tactic:
simpa using (CompleteBipartiteGraph.bicoloring V W).colorable

Result:
no goals

Proof state:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
⊢ ∃ a, C a = b

Tactic:
have w := Classical.arbitrary W

Result:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
⊢ ∃ a, C a = b

Proof state:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ (completeBipartiteGraph V W).chromaticNumber = 2

Tactic:
rw [← Nat.cast_two, chromaticNumber_eq_iff_forall_surjective
  (by simpa using (CompleteBipartiteGraph.bicoloring V W).colorable)]

Result:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ ∀ (C : (completeBipartiteGraph V W).Coloring (Fin 2)), Surjective ⇑C

Proof state:
case pos
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : C (Sum.inl v) = b
⊢ ∃ a, C a = b

Tactic:
exact ⟨_, he⟩

Result:
no goals

Proof state:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
⊢ ∃ a, C a = b

Tactic:
have v := Classical.arbitrary V

Result:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
⊢ ∃ a, C a = b

Proof state:
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
⊢ ∃ a, C a = b

Tactic:
by_cases he : C (Sum.inl v) = b

Result:
case pos
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : C (Sum.inl v) = b
⊢ ∃ a, C a = b

case neg
V : Type u_3
W : Type u_4
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
⊢ ∃ a, C a = b