V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ ∀ (C' : Coloring (completeBipartiteGraph V W) Bool), Function.Surjective ↑C'
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ SimpleGraph.chromaticNumber (completeBipartiteGraph V W) = 2
apply chromaticNumber_eq_card_of_forall_surj (CompleteBipartiteGraph.bicoloring V W)
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
⊢ ∃ a, ↑C a = b
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ ∀ (C' : Coloring (completeBipartiteGraph V W) Bool), Function.Surjective ↑C'
intro C b
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
⊢ ∃ a, ↑C a = b
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
⊢ ∃ a, ↑C a = b
have v := Classical.arbitrary V
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
⊢ ∃ a, ↑C a = b
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
⊢ ∃ a, ↑C a = b
have w := Classical.arbitrary W
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
⊢ ∃ a, ↑C a = b
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
⊢ ∃ a, ↑C a = b
have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
⊢ ∃ a, ↑C a = b
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
⊢ ∃ a, ↑C a = b
have hn := C.valid h
case pos
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ↑C (Sum.inl v) = b
⊢ ∃ a, ↑C a = b

case neg
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
⊢ ∃ a, ↑C a = b
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
⊢ ∃ a, ↑C a = b
by_cases he : C (Sum.inl v) = b
no goals
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
⊢ Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
simp
no goals
case pos
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ↑C (Sum.inl v) = b
⊢ ∃ a, ↑C a = b
exact ⟨_, he⟩
case pos
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
he' : ↑C (Sum.inr w) = b
⊢ ∃ a, ↑C a = b

case neg
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
he' : ¬↑C (Sum.inr w) = b
⊢ ∃ a, ↑C a = b
case neg
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
⊢ ∃ a, ↑C a = b
by_cases he' : C (Sum.inr w) = b
no goals
case pos
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
he' : ↑C (Sum.inr w) = b
⊢ ∃ a, ↑C a = b
exact ⟨_, he'⟩
case neg.h
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
he' : ¬↑C (Sum.inr w) = b
⊢ False
case neg
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
he' : ¬↑C (Sum.inr w) = b
⊢ ∃ a, ↑C a = b
exfalso
no goals
case neg.h
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C✝ : Coloring G α
V : Type u_1
W : Type u_2
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : Coloring (completeBipartiteGraph V W) Bool
b : Bool
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : ↑C (Sum.inl v) ≠ ↑C (Sum.inr w)
he : ¬↑C (Sum.inl v) = b
he' : ¬↑C (Sum.inr w) = b
⊢ False
cases b <;>
  simp only [Bool.eq_true_eq_not_eq_false, Bool.eq_false_eq_not_eq_true] at he he' <;>
    rw [he, he'] at hn <;>
  contradiction