[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
⊢ filter (fun d => d.fst = v) univ = image (dartOfNeighborSet G v) univ
[PROOFSTEP]
ext d
[GOAL]
case a
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
d : Dart G
⊢ d ∈ filter (fun d => d.fst = v) univ ↔ d ∈ image (dartOfNeighborSet G v) univ
[PROOFSTEP]
simp only [mem_image, true_and_iff, mem_filter, SetCoe.exists, mem_univ, exists_prop_of_true]
[GOAL]
case a
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
d : Dart G
⊢ d.fst = v ↔ ∃ x h, dartOfNeighborSet G v { val := x, property := h } = d
[PROOFSTEP]
constructor
[GOAL]
case a.mp
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
d : Dart G
⊢ d.fst = v → ∃ x h, dartOfNeighborSet G v { val := x, property := h } = d
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mp
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
⊢ ∃ x h, dartOfNeighborSet G d.fst { val := x, property := h } = d
[PROOFSTEP]
exact ⟨_, d.is_adj, by ext <;> rfl⟩
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
⊢ dartOfNeighborSet G d.fst { val := d.snd, property := (_ : Adj G d.fst d.snd) } = d
[PROOFSTEP]
ext
[GOAL]
case h.h₁
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
⊢ (dartOfNeighborSet G d.fst { val := d.snd, property := (_ : Adj G d.fst d.snd) }).toProd.fst = d.fst
[PROOFSTEP]
rfl
[GOAL]
case h.h₂
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
⊢ (dartOfNeighborSet G d.fst { val := d.snd, property := (_ : Adj G d.fst d.snd) }).toProd.snd = d.snd
[PROOFSTEP]
rfl
[GOAL]
case a.mpr
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
d : Dart G
⊢ (∃ x h, dartOfNeighborSet G v { val := x, property := h } = d) → d.fst = v
[PROOFSTEP]
rintro ⟨e, he, rfl⟩
[GOAL]
case a.mpr.intro.intro
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v e : V
he : e ∈ neighborSet G v
⊢ (dartOfNeighborSet G v { val := e, property := he }).toProd.fst = v
[PROOFSTEP]
rfl
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
⊢ card (filter (fun d => d.fst = v) univ) = degree G v
[PROOFSTEP]
simpa only [dart_fst_fiber, Finset.card_univ, card_neighborSet_eq_degree] using
  card_image_of_injective univ (G.dartOfNeighborSet_injective v)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
⊢ Fintype.card (Dart G) = ∑ v : V, degree G v
[PROOFSTEP]
haveI := Classical.decEq V
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ Fintype.card (Dart G) = ∑ v : V, degree G v
[PROOFSTEP]
simp only [← card_univ, ← dart_fst_fiber_card_eq_degree]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ card univ = ∑ x : V, card (filter (fun d => d.fst = x) univ)
[PROOFSTEP]
exact card_eq_sum_card_fiberwise (by simp)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ ∀ (x : Dart G), x ∈ univ → x.fst ∈ univ
[PROOFSTEP]
simp
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d d' : Dart G
⊢ d' ∈ filter (fun d' => edge d' = edge d) univ ↔ d' ∈ {d, symm d}
[PROOFSTEP]
simpa using dart_edge_eq_iff d' d
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ edgeSet G
⊢ card (filter (fun d => Dart.edge d = e) univ) = 2
[PROOFSTEP]
refine' Sym2.ind (fun v w h => _) e h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
⊢ card (filter (fun d => Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (v, w)) univ) = 2
[PROOFSTEP]
let d : G.Dart := ⟨(v, w), h⟩
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ card (filter (fun d => Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (v, w)) univ) = 2
[PROOFSTEP]
convert congr_arg card d.edge_fiber
[GOAL]
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ 2 = card {d, Dart.symm d}
[PROOFSTEP]
rw [card_insert_of_not_mem, card_singleton]
[GOAL]
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ ¬d ∈ {Dart.symm d}
[PROOFSTEP]
rw [mem_singleton]
[GOAL]
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ ¬d = Dart.symm d
[PROOFSTEP]
exact d.symm_ne.symm
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
⊢ Fintype.card (Dart G) = 2 * card (edgeFinset G)
[PROOFSTEP]
rw [← card_univ]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
⊢ card univ = 2 * card (edgeFinset G)
[PROOFSTEP]
rw [@card_eq_sum_card_fiberwise _ _ _ Dart.edge _ G.edgeFinset fun d _h => by rw [mem_edgeFinset]; apply Dart.edge_mem]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
_h : d ∈ univ
⊢ Dart.edge d ∈ edgeFinset G
[PROOFSTEP]
rw [mem_edgeFinset]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
_h : d ∈ univ
⊢ Dart.edge d ∈ edgeSet G
[PROOFSTEP]
apply Dart.edge_mem
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
⊢ ∑ a in edgeFinset G, card (filter (fun x => Dart.edge x = a) univ) = 2 * card (edgeFinset G)
[PROOFSTEP]
rw [← mul_comm, sum_const_nat]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
⊢ ∀ (x : Sym2 V), x ∈ edgeFinset G → card (filter (fun x_1 => Dart.edge x_1 = x) univ) = 2
[PROOFSTEP]
intro e h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ edgeFinset G
⊢ card (filter (fun x => Dart.edge x = e) univ) = 2
[PROOFSTEP]
apply G.dart_edge_fiber_card e
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ edgeFinset G
⊢ e ∈ edgeSet G
[PROOFSTEP]
rwa [← mem_edgeFinset]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
[PROOFSTEP]
classical
have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges
simp only [ZMod.nat_cast_self, zero_mul, Nat.cast_mul] at h
rw [Nat.cast_sum, ← sum_filter_ne_zero] at h
rw [@sum_congr _ _ _ _ (fun v => (G.degree v : ZMod 2)) (fun _v => (1 : ZMod 2)) _ rfl] at h
· simp only [filter_congr, mul_one, nsmul_eq_mul, sum_const, Ne.def] at h
  rw [← ZMod.eq_zero_iff_even]
  convert h
  exact ZMod.ne_zero_iff_odd.symm
· intro v
  simp only [true_and_iff, mem_filter, mem_univ, Ne.def]
  rw [ZMod.eq_zero_iff_even, ZMod.eq_one_iff_odd, Nat.odd_iff_not_even, imp_self]
  trivial
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
[PROOFSTEP]
have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : (fun n => ↑n) (∑ v : V, degree G v) = (fun n => ↑n) (2 * card (edgeFinset G))
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
[PROOFSTEP]
simp only [ZMod.nat_cast_self, zero_mul, Nat.cast_mul] at h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(∑ v : V, degree G v) = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
[PROOFSTEP]
rw [Nat.cast_sum, ← sum_filter_ne_zero] at h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
[PROOFSTEP]
rw [@sum_congr _ _ _ _ (fun v => (G.degree v : ZMod 2)) (fun _v => (1 : ZMod 2)) _ rfl] at h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ _v in filter (fun x => ↑(degree G x) ≠ 0) univ, 1 = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
[PROOFSTEP]
simp only [filter_congr, mul_one, nsmul_eq_mul, sum_const, Ne.def] at h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ↑(card (filter (fun x => ¬↑(degree G x) = 0) univ)) = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
[PROOFSTEP]
rw [← ZMod.eq_zero_iff_even]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ↑(card (filter (fun x => ¬↑(degree G x) = 0) univ)) = 0
⊢ ↑(card (filter (fun v => Odd (degree G v)) univ)) = 0
[PROOFSTEP]
convert h
[GOAL]
case h.e'_2.h.e'_3.h.e'_2.h.e'_2.h.a
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ↑(card (filter (fun x => ¬↑(degree G x) = 0) univ)) = 0
x✝ : V
⊢ Odd (degree G x✝) ↔ ¬↑(degree G x✝) = 0
[PROOFSTEP]
exact ZMod.ne_zero_iff_odd.symm
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
⊢ ∀ (x : V), x ∈ filter (fun x => ↑(degree G x) ≠ 0) univ → ↑(degree G x) = 1
[PROOFSTEP]
intro v
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
v : V
⊢ v ∈ filter (fun x => ↑(degree G x) ≠ 0) univ → ↑(degree G v) = 1
[PROOFSTEP]
simp only [true_and_iff, mem_filter, mem_univ, Ne.def]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
v : V
⊢ ¬↑(degree G v) = 0 → ↑(degree G v) = 1
[PROOFSTEP]
rw [ZMod.eq_zero_iff_even, ZMod.eq_one_iff_odd, Nat.odd_iff_not_even, imp_self]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
v : V
⊢ True
[PROOFSTEP]
trivial
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
⊢ Odd (card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ))
[PROOFSTEP]
rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ Odd (card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ))
[PROOFSTEP]
have hk : 0 < k :=
  by
  have hh : (filter (fun v : V => Odd (G.degree v)) univ).Nonempty :=
    by
    use v
    simp only [true_and_iff, mem_filter, mem_univ]
    exact h
  rwa [← card_pos, hg, ← two_mul, zero_lt_mul_left] at hh
  exact zero_lt_two
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ 0 < k
[PROOFSTEP]
have hh : (filter (fun v : V => Odd (G.degree v)) univ).Nonempty :=
  by
  use v
  simp only [true_and_iff, mem_filter, mem_univ]
  exact h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ Finset.Nonempty (filter (fun v => Odd (degree G v)) univ)
[PROOFSTEP]
use v
[GOAL]
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ v ∈ filter (fun v => Odd (degree G v)) univ
[PROOFSTEP]
simp only [true_and_iff, mem_filter, mem_univ]
[GOAL]
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ Odd (degree G v)
[PROOFSTEP]
exact h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hh : Finset.Nonempty (filter (fun v => Odd (degree G v)) univ)
⊢ 0 < k
[PROOFSTEP]
rwa [← card_pos, hg, ← two_mul, zero_lt_mul_left] at hh
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hh : 0 < 2 * k
⊢ 0 < 2
[PROOFSTEP]
exact zero_lt_two
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
⊢ Odd (card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ))
[PROOFSTEP]
have hc : (fun w : V => w ≠ v ∧ Odd (G.degree w)) = fun w : V => Odd (G.degree w) ∧ w ≠ v :=
  by
  ext w
  rw [and_comm]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
⊢ (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
[PROOFSTEP]
ext w
[GOAL]
case h.a
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
w : V
⊢ w ≠ v ∧ Odd (degree G w) ↔ Odd (degree G w) ∧ w ≠ v
[PROOFSTEP]
rw [and_comm]
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ Odd (card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ))
[PROOFSTEP]
simp only [hc, filter_congr]
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ Odd (card (filter (fun w => Odd (degree G w) ∧ w ≠ v) univ))
[PROOFSTEP]
rw [← filter_filter, filter_ne', card_erase_of_mem]
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ Odd (card (filter (fun w => Odd (degree G w)) univ) - 1)
[PROOFSTEP]
refine' ⟨k - 1, tsub_eq_of_eq_add <| hg.trans _⟩
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ k + k = 2 * (k - 1) + 1 + 1
[PROOFSTEP]
rw [add_assoc, one_add_one_eq_two, ← Nat.mul_succ, ← two_mul]
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ 2 * k = 2 * Nat.succ (k - 1)
[PROOFSTEP]
congr
[GOAL]
case intro.e_a
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ k = Nat.succ (k - 1)
[PROOFSTEP]
exact (tsub_add_cancel_of_le <| Nat.succ_le_iff.2 hk).symm
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ v ∈ filter (fun w => Odd (degree G w)) univ
[PROOFSTEP]
simpa only [true_and_iff, mem_filter, mem_univ]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
[PROOFSTEP]
haveI := Classical.decEq V
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
[PROOFSTEP]
rcases G.odd_card_odd_degree_vertices_ne v h with ⟨k, hg⟩
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
[PROOFSTEP]
have hg' : (filter (fun w : V => w ≠ v ∧ Odd (G.degree w)) univ).card > 0 :=
  by
  rw [hg]
  apply Nat.succ_pos
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
⊢ card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
[PROOFSTEP]
rw [hg]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
⊢ 2 * k + 1 > 0
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
hg' : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
[PROOFSTEP]
rcases card_pos.mp hg' with ⟨w, hw⟩
[GOAL]
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
hg' : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
w : V
hw : w ∈ filter (fun w => w ≠ v ∧ Odd (degree G w)) univ
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
[PROOFSTEP]
simp only [true_and_iff, mem_filter, mem_univ, Ne.def] at hw
[GOAL]
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
hg' : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
w : V
hw : ¬w = v ∧ Odd (degree G w)
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
[PROOFSTEP]
exact ⟨w, hw⟩


[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype.card ↑(colorClasses C) ≤ Fintype.card α
[PROOFSTEP]
simp [colorClasses]
  -- porting note: brute force instance declaration `[Fintype (Setoid.classes (Setoid.ker C))]`
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype.card ↑(Setoid.classes (Setoid.ker ↑C)) ≤ Fintype.card α
[PROOFSTEP]
haveI : Fintype (Setoid.classes (Setoid.ker C)) := by assumption
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype ↑(Setoid.classes (Setoid.ker ↑C))
[PROOFSTEP]
assumption
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
this : Fintype ↑(Setoid.classes (Setoid.ker ↑C))
⊢ Fintype.card ↑(Setoid.classes (Setoid.ker ↑C)) ≤ Fintype.card α
[PROOFSTEP]
convert Setoid.card_classes_ker_le C
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype V
inst✝ : Fintype α
⊢ Fintype (Coloring G α)
[PROOFSTEP]
classical
change Fintype (RelHom G.Adj (⊤ : SimpleGraph α).Adj)
apply Fintype.ofInjective _ RelHom.coe_fn_injective
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype V
inst✝ : Fintype α
⊢ Fintype (Coloring G α)
[PROOFSTEP]
change Fintype (RelHom G.Adj (⊤ : SimpleGraph α).Adj)
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype V
inst✝ : Fintype α
⊢ Fintype (G.Adj →r ⊤.Adj)
[PROOFSTEP]
apply Fintype.ofInjective _ RelHom.coe_fn_injective
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
⊢ IsEmpty V
[PROOFSTEP]
constructor
[GOAL]
case false
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
⊢ V → False
[PROOFSTEP]
intro v
[GOAL]
case false
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
v : V
⊢ False
[PROOFSTEP]
obtain ⟨i, hi⟩ := h.some v
[GOAL]
case false.mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : Colorable G 0
v : V
i : ℕ
hi : i < 0
⊢ False
[PROOFSTEP]
exact Nat.not_lt_zero _ hi
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
⊢ Function.Injective fun C => Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C
[PROOFSTEP]
intro C C' h
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h :
  (fun C => Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C) C =
    (fun C => Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C) C'
⊢ C = C'
[PROOFSTEP]
dsimp only at h
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
⊢ C = C'
[PROOFSTEP]
ext v
[GOAL]
case h
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
v : V
⊢ ↑C v = ↑C' v
[PROOFSTEP]
apply (Embedding.completeGraph f).inj'
[GOAL]
case h.a
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
v : V
⊢ Function.Embedding.toFun (Embedding.completeGraph f).toEmbedding (↑C v) =
    Function.Embedding.toFun (Embedding.completeGraph f).toEmbedding (↑C' v)
[PROOFSTEP]
change ((Embedding.completeGraph f).toHom.comp C) v = _
[GOAL]
case h.a
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
v : V
⊢ ↑(Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C) v =
    Function.Embedding.toFun (Embedding.completeGraph f).toEmbedding (↑C' v)
[PROOFSTEP]
rw [h]
[GOAL]
case h.a
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ↪ β
C C' : Coloring G α
h : Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C = Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C'
v : V
⊢ ↑(Hom.comp (Embedding.toHom (Embedding.completeGraph f)) C') v =
    Function.Embedding.toFun (Embedding.completeGraph f).toEmbedding (↑C' v)
[PROOFSTEP]
rfl
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ≃ β
C : Coloring G α
⊢ ↑(recolorOfEmbedding G (Equiv.toEmbedding f.symm)) (↑(recolorOfEmbedding G (Equiv.toEmbedding f)) C) = C
[PROOFSTEP]
ext v
[GOAL]
case h
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ≃ β
C : Coloring G α
v : V
⊢ ↑(↑(recolorOfEmbedding G (Equiv.toEmbedding f.symm)) (↑(recolorOfEmbedding G (Equiv.toEmbedding f)) C)) v = ↑C v
[PROOFSTEP]
apply Equiv.symm_apply_apply
[GOAL]
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ≃ β
C : Coloring G β
⊢ ↑(recolorOfEmbedding G (Equiv.toEmbedding f)) (↑(recolorOfEmbedding G (Equiv.toEmbedding f.symm)) C) = C
[PROOFSTEP]
ext v
[GOAL]
case h
V : Type u
G : SimpleGraph V
α✝ : Type v
C✝ : Coloring G α✝
α : Type u_1
β : Type u_2
f : α ≃ β
C : Coloring G β
v : V
⊢ ↑(↑(recolorOfEmbedding G (Equiv.toEmbedding f)) (↑(recolorOfEmbedding G (Equiv.toEmbedding f.symm)) C)) v = ↑C v
[PROOFSTEP]
apply Equiv.apply_symm_apply
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n m : ℕ
h : n ≤ m
hc : Colorable G n
⊢ Fintype.card (Fin n) ≤ Fintype.card (Fin m)
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
⊢ Fintype.card α ≤ Fintype.card (Fin (Fintype.card α))
[PROOFSTEP]
simp
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype α
n : ℕ
hc : Colorable G n
hn : n ≤ Fintype.card α
⊢ Coloring G α
[PROOFSTEP]
rw [← Fintype.card_fin n] at hn
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype α
n : ℕ
hc : Colorable G n
hn : Fintype.card (Fin n) ≤ Fintype.card α
⊢ Coloring G α
[PROOFSTEP]
exact G.recolorOfCardLE hn hc.some
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
f : G ↪g G'
n : ℕ
h : Colorable G' n
⊢ n ≤ Fintype.card (Fin n)
[PROOFSTEP]
simp
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ Colorable G n ↔ ∃ C, ∀ (v : V), ↑C v < n
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ Colorable G n → ∃ C, ∀ (v : V), ↑C v < n
[PROOFSTEP]
rintro hc
[GOAL]
case mp
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ ∃ C, ∀ (v : V), ↑C v < n
[PROOFSTEP]
have C : G.Coloring (Fin n) := hc.toColoring (by simp)
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ n ≤ Fintype.card (Fin n)
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
let f := Embedding.completeGraph (@Fin.valEmbedding n)
[GOAL]
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
[PROOFSTEP]
use f.toHom.comp C
[GOAL]
case h
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
[PROOFSTEP]
intro v
[GOAL]
case h
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
[PROOFSTEP]
cases' C with color valid
[GOAL]
case h.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
[PROOFSTEP]
exact Fin.is_lt (color v)
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
⊢ (∃ C, ∀ (v : V), ↑C v < n) → Colorable G n
[PROOFSTEP]
rintro ⟨C, Cf⟩
[GOAL]
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
[PROOFSTEP]
refine' ⟨Coloring.mk _ _⟩
[GOAL]
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
[PROOFSTEP]
exact fun v => ⟨C v, Cf v⟩
[GOAL]
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) }
[PROOFSTEP]
rintro v w hvw
[GOAL]
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) }
[PROOFSTEP]
simp only [Fin.mk_eq_mk, Ne.def]
[GOAL]
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
[PROOFSTEP]
exact C.valid hvw
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ chromaticNumber G ≤ n
[PROOFSTEP]
rw [chromaticNumber]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ sInf {n | Colorable G n} ≤ n
[PROOFSTEP]
apply csInf_le chromaticNumber_bddBelow
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ n ∈ {n | Colorable G n}
[PROOFSTEP]
constructor
[GOAL]
case val
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ Coloring G (Fin n)
[PROOFSTEP]
exact Classical.choice hc
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
classical
dsimp only [chromaticNumber]
rw [Nat.sInf_def]
apply Nat.find_spec
exact colorable_set_nonempty_of_colorable hc
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
dsimp only [chromaticNumber]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (sInf {n | Colorable G n})
[PROOFSTEP]
rw [Nat.sInf_def]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Colorable G (Nat.find ?m.140369)
V : Type u G : SimpleGraph V α : Type v C : Coloring G α m : ℕ hc : Colorable G m ⊢ Set.Nonempty {n | Colorable G n}
[PROOFSTEP]
apply Nat.find_spec
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
m : ℕ
hc : Colorable G m
⊢ Set.Nonempty {n | Colorable G n}
[PROOFSTEP]
exact colorable_set_nonempty_of_colorable hc
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
cases nonempty_fintype V
[GOAL]
case intro
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
exact colorable_chromaticNumber G.colorable_of_fintype
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ chromaticNumber G ≤ 1
[PROOFSTEP]
rw [chromaticNumber]
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ sInf {n | Colorable G n} ≤ 1
[PROOFSTEP]
apply csInf_le chromaticNumber_bddBelow
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ 1 ∈ {n | Colorable G n}
[PROOFSTEP]
constructor
[GOAL]
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ Coloring G (Fin 1)
[PROOFSTEP]
refine' Coloring.mk (fun _ => 0) _
[GOAL]
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ ∀ {v w : V}, Adj G v w → (fun x => 0) v ≠ (fun x => 0) w
[PROOFSTEP]
intro v w
[GOAL]
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ Adj G v w → (fun x => 0) v ≠ (fun x => 0) w
[PROOFSTEP]
rw [Subsingleton.elim v w]
[GOAL]
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ Adj G w w → (fun x => 0) w ≠ (fun x => 0) w
[PROOFSTEP]
simp
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ chromaticNumber G = 0
[PROOFSTEP]
rw [← nonpos_iff_eq_zero]
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ chromaticNumber G ≤ 0
[PROOFSTEP]
apply csInf_le chromaticNumber_bddBelow
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ 0 ∈ {n | Colorable G n}
[PROOFSTEP]
apply colorable_of_isEmpty
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
h : chromaticNumber G = 0
⊢ IsEmpty V
[PROOFSTEP]
have h' := G.colorable_chromaticNumber_of_fintype
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
h : chromaticNumber G = 0
h' : Colorable G (chromaticNumber G)
⊢ IsEmpty V
[PROOFSTEP]
rw [h] at h'
[GOAL]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Finite V
h : chromaticNumber G = 0
h' : Colorable G 0
⊢ IsEmpty V
[PROOFSTEP]
exact G.isEmpty_of_colorable_zero h'
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
⊢ 0 < chromaticNumber G
[PROOFSTEP]
apply le_csInf (colorable_set_nonempty_of_colorable hc)
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
⊢ ∀ (b : ℕ), b ∈ {n | Colorable G n} → Nat.succ 0 ≤ b
[PROOFSTEP]
intro m hm
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
⊢ Nat.succ 0 ≤ m
[PROOFSTEP]
by_contra h'
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : ¬Nat.succ 0 ≤ m
⊢ False
[PROOFSTEP]
simp only [not_le] at h'
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
⊢ False
[PROOFSTEP]
obtain ⟨i, hi⟩ := hm.some (Classical.arbitrary V)
[GOAL]
case mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
⊢ False
[PROOFSTEP]
have h₁ : i < 0 := lt_of_lt_of_le hi (Nat.le_of_lt_succ h')
[GOAL]
case mk
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
n : ℕ
hc : Colorable G n
m : ℕ
hm : m ∈ {n | Colorable G n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
h₁ : i < 0
⊢ False
[PROOFSTEP]
exact Nat.not_lt_zero _ h₁
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h : 0 < chromaticNumber G
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
obtain ⟨h, hn⟩ := Nat.nonempty_of_pos_sInf h
[GOAL]
case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
h✝ : 0 < chromaticNumber G
h : ℕ
hn : h ∈ {n | Colorable G n}
⊢ Colorable G (chromaticNumber G)
[PROOFSTEP]
exact colorable_chromaticNumber hn
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ chromaticNumber G ≤ chromaticNumber G'
[PROOFSTEP]
apply csInf_le chromaticNumber_bddBelow
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ chromaticNumber G' ∈ {n | Colorable G n}
[PROOFSTEP]
apply h
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ Colorable G' (chromaticNumber G')
[PROOFSTEP]
apply colorable_chromaticNumber hc
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
⊢ chromaticNumber G = Fintype.card α
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
⊢ chromaticNumber G ≤ Fintype.card α
[PROOFSTEP]
apply chromaticNumber_le_card C
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
⊢ Fintype.card α ≤ chromaticNumber G
[PROOFSTEP]
by_contra hc
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc : ¬Fintype.card α ≤ chromaticNumber G
⊢ False
[PROOFSTEP]
rw [not_le] at hc
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc : chromaticNumber G < Fintype.card α
⊢ False
[PROOFSTEP]
obtain ⟨n, cn, hc⟩ := exists_lt_of_csInf_lt (colorable_set_nonempty_of_colorable C.to_colorable) hc
[GOAL]
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : n < Fintype.card α
⊢ False
[PROOFSTEP]
rw [← Fintype.card_fin n] at hc
[GOAL]
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
⊢ False
[PROOFSTEP]
have f := (Function.Embedding.nonempty_of_card_le (le_of_lt hc)).some
[GOAL]
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
⊢ False
[PROOFSTEP]
have C' := cn.some
[GOAL]
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
h : ∀ (C' : Coloring G α), Function.Surjective ↑C'
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
⊢ False
[PROOFSTEP]
specialize h (G.recolorOfEmbedding f C')
[GOAL]
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
h : Function.Surjective ↑(↑(recolorOfEmbedding G f) C')
⊢ False
[PROOFSTEP]
have h1 : Function.Surjective f := Function.Surjective.of_comp h
[GOAL]
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
h : Function.Surjective ↑(↑(recolorOfEmbedding G f) C')
h1 : Function.Surjective ↑f
⊢ False
[PROOFSTEP]
have h2 := Fintype.card_le_of_surjective _ h1
[GOAL]
case a.intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype α
C : Coloring G α
hc✝ : chromaticNumber G < Fintype.card α
n : ℕ
cn : n ∈ {n | Colorable G n}
hc : Fintype.card (Fin n) < Fintype.card α
f : Fin n ↪ α
C' : Coloring G (Fin n)
h : Function.Surjective ↑(↑(recolorOfEmbedding G f) C')
h1 : Function.Surjective ↑f
h2 : Fintype.card α ≤ Fintype.card (Fin n)
⊢ False
[PROOFSTEP]
exact Nat.lt_le_antisymm hc h2
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
⊢ chromaticNumber ⊥ = 1
[PROOFSTEP]
let C : (⊥ : SimpleGraph V).Coloring (Fin 1) := Coloring.mk (fun _ => 0) fun {v w} h => False.elim h
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ chromaticNumber ⊥ = 1
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ chromaticNumber ⊥ ≤ 1
[PROOFSTEP]
exact chromaticNumber_le_card C
[GOAL]
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ 1 ≤ chromaticNumber ⊥
[PROOFSTEP]
exact chromaticNumber_pos C.to_colorable
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype V
⊢ chromaticNumber ⊤ = Fintype.card V
[PROOFSTEP]
apply chromaticNumber_eq_card_of_forall_surj (selfColoring _)
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype V
⊢ ∀ (C' : Coloring ⊤ V), Function.Surjective ↑C'
[PROOFSTEP]
intro C
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
⊢ Function.Surjective ↑C
[PROOFSTEP]
rw [← Finite.injective_iff_surjective]
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
⊢ Function.Injective ↑C
[PROOFSTEP]
intro v w
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
⊢ ↑C v = ↑C w → v = w
[PROOFSTEP]
contrapose
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
⊢ ¬v = w → ¬↑C v = ↑C w
[PROOFSTEP]
intro h
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
h : ¬v = w
⊢ ¬↑C v = ↑C w
[PROOFSTEP]
exact C.valid h
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
⊢ chromaticNumber ⊤ = 0
[PROOFSTEP]
let n := (⊤ : SimpleGraph V).chromaticNumber
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
⊢ chromaticNumber ⊤ = 0
[PROOFSTEP]
by_contra hc
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : ¬chromaticNumber ⊤ = 0
⊢ False
[PROOFSTEP]
replace hc := pos_iff_ne_zero.mpr hc
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ False
[PROOFSTEP]
apply Nat.not_succ_le_self n
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ Nat.succ n ≤ n
[PROOFSTEP]
convert_to (⊤ : SimpleGraph {m | m < n + 1}).chromaticNumber ≤ _
[GOAL]
case h.e'_3
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ Nat.succ n = chromaticNumber ⊤
[PROOFSTEP]
rw [SimpleGraph.chromaticNumber_top, Fintype.card_ofFinset, Finset.card_range, Nat.succ_eq_add_one]
[GOAL]
case convert_2
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ chromaticNumber ⊤ ≤ n
[PROOFSTEP]
refine' (colorable_of_chromaticNumber_pos hc).chromaticNumber_mono_of_embedding _
[GOAL]
case convert_2
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ ⊤ ↪g ⊤
[PROOFSTEP]
apply Embedding.completeGraph
[GOAL]
case convert_2.f
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
inst✝ : Infinite V
n : ℕ := chromaticNumber ⊤
hc : 0 < chromaticNumber ⊤
⊢ ↑{m | m < n + 1} ↪ V
[PROOFSTEP]
exact (Function.Embedding.subtype _).trans (Infinite.natEmbedding V)
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
⊢ ∀ {v w : V ⊕ W}, Adj (completeBipartiteGraph V W) v w → (fun v => Sum.isRight v) v ≠ (fun v => Sum.isRight v) w
[PROOFSTEP]
intro v w
[GOAL]
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
v w : V ⊕ W
⊢ Adj (completeBipartiteGraph V W) v w → (fun v => Sum.isRight v) v ≠ (fun v => Sum.isRight v) w
[PROOFSTEP]
cases v
[GOAL]
case inl
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
w : V ⊕ W
val✝ : V
⊢ Adj (completeBipartiteGraph V W) (Sum.inl val✝) w →
    (fun v => Sum.isRight v) (Sum.inl val✝) ≠ (fun v => Sum.isRight v) w
[PROOFSTEP]
cases w
[GOAL]
case inr
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
w : V ⊕ W
val✝ : W
⊢ Adj (completeBipartiteGraph V W) (Sum.inr val✝) w →
    (fun v => Sum.isRight v) (Sum.inr val✝) ≠ (fun v => Sum.isRight v) w
[PROOFSTEP]
cases w
[GOAL]
case inl.inl
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
val✝¹ val✝ : V
⊢ Adj (completeBipartiteGraph V W) (Sum.inl val✝¹) (Sum.inl val✝) →
    (fun v => Sum.isRight v) (Sum.inl val✝¹) ≠ (fun v => Sum.isRight v) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case inl.inr
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
val✝¹ : V
val✝ : W
⊢ Adj (completeBipartiteGraph V W) (Sum.inl val✝¹) (Sum.inr val✝) →
    (fun v => Sum.isRight v) (Sum.inl val✝¹) ≠ (fun v => Sum.isRight v) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
case inr.inl
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
val✝¹ : W
val✝ : V
⊢ Adj (completeBipartiteGraph V W) (Sum.inr val✝¹) (Sum.inl val✝) →
    (fun v => Sum.isRight v) (Sum.inr val✝¹) ≠ (fun v => Sum.isRight v) (Sum.inl val✝)
[PROOFSTEP]
simp
[GOAL]
case inr.inr
V✝ : Type u
G : SimpleGraph V✝
α : Type v
C : Coloring G α
V : Type u_1
W : Type u_2
val✝¹ val✝ : W
⊢ Adj (completeBipartiteGraph V W) (Sum.inr val✝¹) (Sum.inr val✝) →
    (fun v => Sum.isRight v) (Sum.inr val✝¹) ≠ (fun v => Sum.isRight v) (Sum.inr val✝)
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
apply chromaticNumber_eq_card_of_forall_surj (CompleteBipartiteGraph.bicoloring V W)
[GOAL]
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'
[PROOFSTEP]
intro C b
[GOAL]
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
[PROOFSTEP]
have v := Classical.arbitrary V
[GOAL]
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
[PROOFSTEP]
have w := Classical.arbitrary W
[GOAL]
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
[PROOFSTEP]
have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
have hn := C.valid h
[GOAL]
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
[PROOFSTEP]
by_cases he : C (Sum.inl v) = b
[GOAL]
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
[PROOFSTEP]
exact ⟨_, he⟩
[GOAL]
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
[PROOFSTEP]
by_cases he' : C (Sum.inr w) = b
[GOAL]
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
[PROOFSTEP]
exact ⟨_, he'⟩
[GOAL]
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
[PROOFSTEP]
exfalso
[GOAL]
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
[PROOFSTEP]
cases b
[GOAL]
case neg.h.false
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
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) = false
he' : ¬↑C (Sum.inr w) = false
⊢ False
[PROOFSTEP]
simp only [Bool.eq_true_eq_not_eq_false, Bool.eq_false_eq_not_eq_true] at he he'
[GOAL]
case neg.h.true
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
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) = true
he' : ¬↑C (Sum.inr w) = true
⊢ False
[PROOFSTEP]
simp only [Bool.eq_true_eq_not_eq_false, Bool.eq_false_eq_not_eq_true] at he he'
[GOAL]
case neg.h.false
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
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) = true
he' : ↑C (Sum.inr w) = true
⊢ False
[PROOFSTEP]
rw [he, he'] at hn
[GOAL]
case neg.h.true
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
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) = false
he' : ↑C (Sum.inr w) = false
⊢ False
[PROOFSTEP]
rw [he, he'] at hn
[GOAL]
case neg.h.false
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
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : true ≠ true
he : ↑C (Sum.inl v) = true
he' : ↑C (Sum.inr w) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg.h.true
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
v : V
w : W
h : Adj (completeBipartiteGraph V W) (Sum.inl v) (Sum.inr w)
hn : false ≠ false
he : ↑C (Sum.inl v) = false
he' : ↑C (Sum.inr w) = false
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : IsClique G ↑s
inst✝ : Fintype α
C : Coloring G α
⊢ Finset.card s ≤ Fintype.card α
[PROOFSTEP]
rw [isClique_iff_induce_eq] at h
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
⊢ Finset.card s ≤ Fintype.card α
[PROOFSTEP]
have f : G.induce ↑s ↪g G := Embedding.comap (Function.Embedding.subtype fun x => x ∈ ↑s) G
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : induce (↑s) G ↪g G
⊢ Finset.card s ≤ Fintype.card α
[PROOFSTEP]
rw [h] at f
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : ⊤ ↪g G
⊢ Finset.card s ≤ Fintype.card α
[PROOFSTEP]
convert Fintype.card_le_of_injective _ (C.comp f.toHom).injective_of_top_hom using 1
[GOAL]
case h.e'_3
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : ⊤ ↪g G
⊢ Finset.card s = Fintype.card ↑↑s
[PROOFSTEP]
simp
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
s : Finset V
h : IsClique G ↑s
n : ℕ
hc : Colorable G n
⊢ Finset.card s ≤ n
[PROOFSTEP]
convert h.card_le_of_coloring hc.some
[GOAL]
case h.e'_4
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
s : Finset V
h : IsClique G ↑s
n : ℕ
hc : Colorable G n
⊢ n = Fintype.card (Fin n)
[PROOFSTEP]
simp
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Finite V
s : Finset V
h : IsClique G ↑s
⊢ Finset.card s ≤ chromaticNumber G
[PROOFSTEP]
cases nonempty_fintype V
[GOAL]
case intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Finite V
s : Finset V
h : IsClique G ↑s
val✝ : Fintype V
⊢ Finset.card s ≤ chromaticNumber G
[PROOFSTEP]
exact h.card_le_of_colorable G.colorable_chromaticNumber_of_fintype
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n m : ℕ
hc : Colorable G n
hm : n < m
⊢ CliqueFree G m
[PROOFSTEP]
by_contra h
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n m : ℕ
hc : Colorable G n
hm : n < m
h : ¬CliqueFree G m
⊢ False
[PROOFSTEP]
simp only [CliqueFree, isNClique_iff, not_forall, Classical.not_not] at h
[GOAL]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n m : ℕ
hc : Colorable G n
hm : n < m
h : ∃ x, IsClique G ↑x ∧ Finset.card x = m
⊢ False
[PROOFSTEP]
obtain ⟨s, h, rfl⟩ := h
[GOAL]
case intro.intro
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
s : Finset V
h : IsClique G ↑s
hm : n < Finset.card s
⊢ False
[PROOFSTEP]
exact Nat.lt_le_antisymm hm (h.card_le_of_colorable hc)