awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ (↑n : ℕ∞)
⊢ G.chromaticNumber ≠ ⊤

Tactic:
have : G.chromaticNumber ≠ ⊤ := (trans h (WithTop.coe_lt_top n)).ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ (↑n : ℕ∞)
this : G.chromaticNumber ≠ ⊤
⊢ ∃ (n : ℕ), G.Colorable n

Tactic:
rw [chromaticNumber_ne_top_iff_exists] at this

Premises used: SimpleGraph.chromaticNumber_ne_top_iff_exists
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ (↑n : ℕ∞)
this : ∃ (n : ℕ), G.Colorable n
obtain : ∀ (m : ℕ) (hm : G.Colorable m), G.Colorable n
⊢ G.Colorable n

Tactic:
obtain ⟨m, hm⟩ := this
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ (↑n : ℕ∞)
m : ℕ
hm : G.Colorable m
rw : ∀ (h : sInf {n' : ℕ | G.Colorable n'} ≤ n) (m : ℕ) (hm : G.Colorable m), G.Colorable n
⊢ G.Colorable n

Tactic:
rw [hm.chromaticNumber_eq_sInf, Nat.cast_le] at h

Premises used: SimpleGraph.Colorable.chromaticNumber_eq_sInf, Nat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' : ℕ | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
⊢ Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} (sInf {n' : ℕ | G.Colorable n'})

Tactic:
have := Nat.sInf_mem (⟨m, hm⟩ : {n' | G.Colorable n'}.Nonempty)
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' : ℕ | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} (sInf {n' : ℕ | G.Colorable n'})
⊢ G.Colorable (sInf {n' : ℕ | G.Colorable n'})

Tactic:
rw [Set.mem_setOf_eq] at this

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' : ℕ | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : G.Colorable (sInf {n' : ℕ | G.Colorable n'})
⊢ G.Colorable n

Tactic:
this.mono h

Premises used: SimpleGraph.Colorable.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' : ℕ | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : G.Colorable (sInf {n' : ℕ | G.Colorable n'})
⊢ G.Colorable n

Tactic:
exact this.mono h

Premises used: SimpleGraph.Colorable.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
rw :
  G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ ¬G.chromaticNumber < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    G.Colorable (n + 1) ∧ ¬G.Colorable n
rw₁ :
  G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ G.chromaticNumber ↔
    G.Colorable (n + 1) ∧ ¬G.Colorable n
rw₂ :
  G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ (↑n : ℕ∞) < G.chromaticNumber ↔
    G.Colorable (n + 1) ∧ ¬G.Colorable n
rw₃ :
  G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ ¬G.chromaticNumber ≤ (↑n : ℕ∞) ↔
    G.Colorable (n + 1) ∧ ¬G.Colorable n
rw₄ : G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ ¬G.Colorable n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
rw₅ : G.chromaticNumber ≤ (↑(n + 1) : ℕ∞) ∧ ¬G.Colorable n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
rw₆ rw₇ : G.Colorable (n + 1) ∧ ¬G.Colorable n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
⊢ G.chromaticNumber = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n

Tactic:
rw [eq_iff_le_not_lt, not_lt, ENat.add_one_le_iff (ENat.coe_ne_top n), ← not_le,
    chromaticNumber_le_iff_colorable, ← Nat.cast_add_one, chromaticNumber_le_iff_colorable]

Premises used: not_le, ENat.add_one_le_iff, SimpleGraph.chromaticNumber_le_iff_colorable, not_lt, eq_iff_le_not_lt, ENat.coe_ne_top, Nat.cast_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
rw :
  G.Colorable
    (ENat.toNat (↑(Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} n) ⋯) : ℕ∞))
rw₁ : Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]

Premises used: SimpleGraph.Colorable.chromaticNumber_eq_sInf, Nat.sInf_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable
    (ENat.toNat (↑(Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} n) ⋯) : ℕ∞))

Tactic:
apply Nat.find_spec

Premises used: Nat.find_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}

Tactic:
colorable_set_nonempty_of_colorable hc

Premises used: SimpleGraph.colorable_set_nonempty_of_colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}

Tactic:
exact colorable_set_nonempty_of_colorable hc

Premises used: SimpleGraph.colorable_set_nonempty_of_colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
rw : G.Colorable (ENat.toNat (↑(sInf {n' : ℕ | G.Colorable n'}) : ℕ∞))
rw₁ :
  G.Colorable
    (ENat.toNat (↑(Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} n) ⋯) : ℕ∞))
rw₂ : Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}
rw₃ :
  G.Colorable
    (ENat.toNat (↑(Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} n) ⋯) : ℕ∞))
rw₄ : Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}
rw₅ :
  G.Colorable
    (ENat.toNat (↑(Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} n) ⋯) : ℕ∞))
rw₆ rw₇ : Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
classical
  rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]
  · apply Nat.find_spec
  · exact colorable_set_nonempty_of_colorable hc

Premises used: SimpleGraph.Colorable.chromaticNumber_eq_sInf, Nat.sInf_def, SimpleGraph.colorable_set_nonempty_of_colorable, Nat.find_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
intro : ∀ (val : Fintype V), G.Colorable G.chromaticNumber.toNat
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
cases nonempty_fintype V

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
colorable_chromaticNumber G.colorable_of_fintype

Premises used: SimpleGraph.colorable_chromaticNumber, SimpleGraph.colorable_of_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
exact colorable_chromaticNumber G.colorable_of_fintype

Premises used: SimpleGraph.colorable_chromaticNumber, SimpleGraph.colorable_of_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
rw : G.Colorable 1
⊢ G.chromaticNumber ≤ 1

Tactic:
rw [← Nat.cast_one, chromaticNumber_le_iff_colorable]

Premises used: SimpleGraph.chromaticNumber_le_iff_colorable, Nat.cast_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
⊢ G.Colorable 1

Tactic:
⟨Coloring.mk (fun _ => 0) ?_⟩

Premises used: SimpleGraph.Coloring.mk, Nonempty.intro, SimpleGraph.Colorable, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
refine : ∀ {v w : V}, G.Adj v w → Ne (α := Fin 1) ((fun (x : V) ↦ (0 : Fin 1)) v) ((fun (x : V) ↦ (0 : Fin 1)) w)
⊢ G.Colorable 1

Tactic:
refine ⟨Coloring.mk (fun _ => 0) ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
v w : V
refl : G.Adj v v → Ne (α := Fin 1) ((fun (x : V) ↦ (0 : Fin 1)) v) ((fun (x : V) ↦ (0 : Fin 1)) v)
⊢ G.Adj v w → Ne (α := Fin 1) ((fun (x : V) ↦ (0 : Fin 1)) v) ((fun (x : V) ↦ (0 : Fin 1)) w)

Tactic:
cases Subsingleton.elim v w

Premises used: Subsingleton.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
v : V
⊢ G.Adj v v → Ne (α := Fin 1) ((fun (x : V) ↦ (0 : Fin 1)) v) ((fun (x : V) ↦ (0 : Fin 1)) v)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
rw : LT.lt (α := ℕ) 0 (sInf {n' : ℕ | G.Colorable n'})
⊢ 0 < G.chromaticNumber

Tactic:
rw [hc.chromaticNumber_eq_sInf, Nat.cast_pos]

Premises used: Nat.cast_pos, SimpleGraph.Colorable.chromaticNumber_eq_sInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
apply : ∀ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} b → Nat.succ 0 ≤ b
⊢ LT.lt (α := ℕ) 0 (sInf {n' : ℕ | G.Colorable n'})

Tactic:
apply le_csInf (colorable_set_nonempty_of_colorable hc)

Premises used: le_csInf, SimpleGraph.colorable_set_nonempty_of_colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} m
by_contra : ∀ (h' : ¬Nat.succ 0 ≤ m), False
⊢ Nat.succ 0 ≤ m

Tactic:
by_contra h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} m
h' : ¬Nat.succ 0 ≤ m
⊢ m < Nat.succ 0

Tactic:
simp only [not_le] at h'

Premises used: not_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} m
h' : m < Nat.succ 0
obtain : ∀ (i : ℕ) (hi : i < m), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := hm.some (Classical.arbitrary V)

Premises used: Nonempty.some, Classical.arbitrary, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} m
h' : m < Nat.succ 0
i : ℕ
hi : i < m
⊢ i < 0

Tactic:
have h₁ : i < 0 := lt_of_lt_of_le hi (Nat.le_of_lt_succ h')
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} m
h' : m < Nat.succ 0
i : ℕ
hi : i < m
h₁ : i < 0
⊢ False

Tactic:
Nat.not_lt_zero _ h₁

Premises used: Nat.not_lt_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} m
h' : m < Nat.succ 0
i : ℕ
hi : i < m
h₁ : i < 0
⊢ False

Tactic:
exact Nat.not_lt_zero _ h₁

Premises used: Nat.not_lt_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h : G.chromaticNumber ≠ ⊤
⊢ ∃ (n : ℕ), G.Colorable n

Tactic:
rw [chromaticNumber_ne_top_iff_exists] at h

Premises used: SimpleGraph.chromaticNumber_ne_top_iff_exists
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h : ∃ (n : ℕ), G.Colorable n
obtain : ∀ (n : ℕ) (hn : G.Colorable n), G.Colorable G.chromaticNumber.toNat
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
obtain ⟨n, hn⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hn : G.Colorable n
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
colorable_chromaticNumber hn

Premises used: SimpleGraph.colorable_chromaticNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hn : G.Colorable n
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
exact colorable_chromaticNumber hn

Premises used: SimpleGraph.colorable_chromaticNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
n : ℕ
hc : G'.Colorable n
⊢ G.Colorable n

Tactic:
⟨hc.some.comp (.ofLE h)⟩

Premises used: Nonempty.some, Nonempty.intro, SimpleGraph.Hom.ofLE, SimpleGraph.Colorable, SimpleGraph.Hom.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
simp : ∀ (i : ℕ) (i_1 : G'.Colorable i), LE.le (α := ℕ∞) (⨅ (n : ℕ), ⨅ (_ : G.Colorable n), (↑n : ℕ∞)) (↑i : ℕ∞)
⊢ LE.le (α := ℕ∞) (⨅ n ∈ setOf G.Colorable, (↑n : ℕ∞)) (⨅ n ∈ setOf G'.Colorable, (↑n : ℕ∞))

Tactic:
simp only [Set.mem_setOf_eq, le_iInf_iff]

Premises used: le_iInf_iff, Set.mem_setOf_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
⊢ G.Colorable m

Tactic:
have := h _ hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
this : G.Colorable m
⊢ G.chromaticNumber ≤ (↑m : ℕ∞)

Tactic:
rw [← chromaticNumber_le_iff_colorable] at this

Premises used: SimpleGraph.chromaticNumber_le_iff_colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
this : G.chromaticNumber ≤ (↑m : ℕ∞)
⊢ LE.le (α := ℕ∞) (⨅ (n : ℕ), ⨅ (_ : G.Colorable n), (↑n : ℕ∞)) (↑m : ℕ∞)

Tactic:
this

Premises used: Set.Mem, setOf, SimpleGraph.Colorable, SimpleGraph.chromaticNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
m : ℕ
hc : G'.Colorable m
this : G.chromaticNumber ≤ (↑m : ℕ∞)
⊢ LE.le (α := ℕ∞) (⨅ (n : ℕ), ⨅ (_ : G.Colorable n), (↑n : ℕ∞)) (↑m : ℕ∞)

Tactic:
exact this
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
⊢ G.chromaticNumber ≤ G'.chromaticNumber

Tactic:
chromaticNumber_le_of_forall_imp fun _ => Colorable.mono_left h

Premises used: SimpleGraph.chromaticNumber_le_of_forall_imp, SimpleGraph.Colorable.mono_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
f : G →g G'
⊢ G.chromaticNumber ≤ G'.chromaticNumber

Tactic:
chromaticNumber_le_of_forall_imp fun _ => Colorable.of_hom f

Premises used: SimpleGraph.Colorable.of_hom, SimpleGraph.chromaticNumber_le_of_forall_imp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
⊢ (↑(card α) : ℕ∞) ≤ G.chromaticNumber ↔
    ∀ (C : G.Coloring α), Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)

Tactic:
⟨fun h C ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
refine_1 :
  ∀ (h : (↑(card α) : ℕ∞) ≤ G.chromaticNumber) (C : G.Coloring α),
    Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)
refine_2 :
  ∀ (h : ∀ (C : G.Coloring α), Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)),
    (↑(card α) : ℕ∞) ≤ G.chromaticNumber
⊢ (↑(card α) : ℕ∞) ≤ G.chromaticNumber ↔
    ∀ (C : G.Coloring α), Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)

Tactic:
refine ⟨fun h C ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
h : (↑(card α) : ℕ∞) ≤ G.chromaticNumber
C : G.Coloring α
refine_1 :
  ∀ (h : card α ≤ sInf {n' : ℕ | G.Colorable n'}) (C : G.Coloring α),
    Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)
⊢ Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)

Tactic:
rw [C.colorable.chromaticNumber_eq_sInf, Nat.cast_le] at h

Premises used: SimpleGraph.Colorable.chromaticNumber_eq_sInf, Nat.cast_le, SimpleGraph.Coloring.colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
h : card α ≤ sInf {n' : ℕ | G.Colorable n'}
C : G.Coloring α
i : α
refine_1 : ∀ (hi : ∀ (a : V), (C : (a : V) → α) a ≠ i), False
⊢ ∃ (a : V), (C : (a : V) → α) a = i

Tactic:
by_contra! hi
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
h : card α ≤ sInf {n' : ℕ | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), (C : (a : V) → α) a ≠ i
D : Coloring.{u, u_2} G { a : α // a ≠ i } :=
  RelHom.mk (r := G.Adj) (s := Adj (completeGraph { a : α // a ≠ i }))
    (fun (v : V) ↦ Subtype.mk (p := fun (a : α) ↦ a ≠ i) ((C : (a : V) → α) v) ⋯) ⋯
⊢ card.{u_2} { a : α // a ≠ i } = card (Fin (card α - 1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
h : card α ≤ sInf {n' : ℕ | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), (C : (a : V) → α) a ≠ i
D : Coloring.{u, u_2} G { a : α // a ≠ i } :=
  RelHom.mk (r := G.Adj) (s := Adj (completeGraph { a : α // a ≠ i }))
    (fun (v : V) ↦ Subtype.mk (p := fun (a : α) ↦ a ≠ i) ((C : (a : V) → α) v) ⋯) ⋯
⊢ False

Tactic:
exact Nat.notMem_of_lt_sInf ((Nat.sub_one_lt_of_lt <| card_pos_iff.2 ⟨i⟩).trans_le h)
      ⟨G.recolorOfEquiv (equivOfCardEq <| by simp) D⟩

Premises used: Nat.sub_one_lt_of_lt, Iff.mpr, Nat.notMem_of_lt_sInf, Nonempty.intro, LT.lt.trans_le, SimpleGraph.recolorOfEquiv, DFunLike.coe, Fintype.card_pos_iff, Fintype.equivOfCardEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
h : card α ≤ sInf {n' : ℕ | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), (C : (a : V) → α) a ≠ i
D : Coloring.{u, u_2} G { a : α // a ≠ i } :=
  RelHom.mk (r := G.Adj) (s := Adj (completeGraph { a : α // a ≠ i }))
    (fun (v : V) ↦ Subtype.mk (p := fun (a : α) ↦ a ≠ i) ((C : (a : V) → α) v) ⋯) ⋯
⊢ False

Tactic:
classical
    exact Nat.notMem_of_lt_sInf ((Nat.sub_one_lt_of_lt <| card_pos_iff.2 ⟨i⟩).trans_le h)
      ⟨G.recolorOfEquiv (equivOfCardEq <| by simp) D⟩

Premises used: Nat.sub_one_lt_of_lt, Iff.mpr, Nat.notMem_of_lt_sInf, Nonempty.intro, LT.lt.trans_le, SimpleGraph.recolorOfEquiv, DFunLike.coe, Fintype.card_pos_iff, Fintype.equivOfCardEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
h : ∀ (C : G.Coloring α), Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)
refine_2 : ∀ (i : ℕ) (i_1 : G.Colorable i), card α ≤ i
⊢ (↑(card α) : ℕ∞) ≤ G.chromaticNumber

Tactic:
simp only [chromaticNumber, Set.mem_setOf_eq, le_iInf_iff, Nat.cast_le]

Premises used: le_iInf_iff, Set.mem_setOf_eq, Nat.cast_le, SimpleGraph.chromaticNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
h : ∀ (C : G.Coloring α), Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)
i : ℕ
C : G.Coloring (Fin i)
refine_2 : ∀ (h : i < card α), ∃ (C : G.Coloring α), ¬Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)
⊢ card α ≤ i

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
⊢ card (Fin i) ≤ card α

Tactic:
simpa using h.le

Premises used: LT.lt.le
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
refine_2 :
  ∀
    (hC :
      Surjective.{u + 1, u_2 + 1} (α := V) (β := α)
        (⇑((G.recolorOfCardLE ⋯ : (a : G.Coloring (Fin i)) → G.Coloring α) C : G.Coloring α) : (a : V) → α)),
    False
⊢ ∃ (C : G.Coloring α), ¬Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)

Tactic:
refine ⟨G.recolorOfCardLE (by simpa using h.le) C, fun hC ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
hC : Surjective (α := V) (β := α) (comp (β := Fin i) (⇑⋯.some : (a : Fin i) → α) (⇑C : (a : V) → Fin i))
⊢ False

Tactic:
simpa [h.not_ge] using Fintype.card_le_of_surjective _ hC.of_comp

Premises used: Function.Surjective.of_comp, LT.lt.not_ge, Fintype.card_le_of_surjective
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (↑n : ℕ∞) ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Surjective (α := V) (β := Fin n) (⇑C : (a : V) → Fin n)

Tactic:
simp [← card_le_chromaticNumber_iff_forall_surjective]

Premises used: SimpleGraph.card_le_chromaticNumber_iff_forall_surjective
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
hG : G.Colorable (card α)
rw :
  (↑(card α) : ℕ∞) ≤ G.chromaticNumber ↔
    ∀ (C : G.Coloring α), Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)
rw₁ rw₂ :
  (∀ (C : G.Coloring α), Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)) ↔
    ∀ (C : G.Coloring α), Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)
⊢ G.chromaticNumber = (↑(card α) : ℕ∞) ↔
    ∀ (C : G.Coloring α), Surjective.{u + 1, u_2 + 1} (α := V) (β := α) (⇑C : (a : V) → α)

Tactic:
rw [← hG.chromaticNumber_le.ge_iff_eq, card_le_chromaticNumber_iff_forall_surjective]

Premises used: SimpleGraph.card_le_chromaticNumber_iff_forall_surjective, SimpleGraph.Colorable.chromaticNumber_le, LE.le.ge_iff_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hG : G.Colorable n
rw : (↑n : ℕ∞) ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Surjective (α := V) (β := Fin n) (⇑C : (a : V) → Fin n)
rw₁ rw₂ :
  (∀ (C : G.Coloring (Fin n)), Surjective (α := V) (β := Fin n) (⇑C : (a : V) → Fin n)) ↔
    ∀ (C : G.Coloring (Fin n)), Surjective (α := V) (β := Fin n) (⇑C : (a : V) → Fin n)
⊢ G.chromaticNumber = (↑n : ℕ∞) ↔ ∀ (C : G.Coloring (Fin n)), Surjective (α := V) (β := Fin n) (⇑C : (a : V) → Fin n)

Tactic:
rw [← hG.chromaticNumber_le.ge_iff_eq, le_chromaticNumber_iff_forall_surjective]

Premises used: SimpleGraph.le_chromaticNumber_iff_forall_surjective, SimpleGraph.Colorable.chromaticNumber_le, LE.le.ge_iff_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
inst : Nonempty V
⊢ Colorable.{u} (V := V) ⊥ 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
inst : Fintype V
rw : ∀ (C : Coloring (V := V) ⊤ V), Surjective (α := V) (β := V) (⇑C : (a : V) → V)
⊢ chromaticNumber.{u} (V := V) ⊤ = (↑(card V) : ℕ∞)

Tactic:
rw [chromaticNumber_eq_card_iff_forall_surjective (selfColoring _).colorable]

Premises used: SimpleGraph.selfColoring, SimpleGraph.Coloring.colorable, SimpleGraph.chromaticNumber_eq_card_iff_forall_surjective