awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
hc : G.Colorable n
⊢ Colorable.{u_3} (V := β) (SimpleGraph.map (⇑f : (a : V) → β) G) n
have obtain : ∀ (C : G.Coloring (Fin n)), Colorable.{u_3} (V := β) (SimpleGraph.map (⇑f : (a : V) → β) G) n
Tactic: obtain ⟨C⟩ := hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
C : G.Coloring (Fin n)
⊢ Colorable.{u_3} (V := β) (SimpleGraph.map (⇑f : (a : V) → β) G) n
have map_rel' : ∀ {a b : β},
  Adj (SimpleGraph.map (⇑f : (a : V) → β) G) a b →
    Adj (V := Fin n) (completeGraph (Fin n))
      (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) a)
      (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) b)
Tactic: use extend f C (const β default)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
C : G.Coloring (Fin n)
a b : β
⊢ Adj (SimpleGraph.map (⇑f : (a : V) → β) G) a b →
    Adj (V := Fin n) (completeGraph (Fin n))
      (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) a)
      (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) b)
have map_rel' : a ≠ b →
  ∀ (w w_1 : V) (hadj : G.Adj w w_1) (ha : (f : (a : V) → β) w = a) (hb : (f : (a : V) → β) w_1 = b),
    Adj (V := Fin n) (completeGraph (Fin n))
      (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) a)
      (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) b)
Tactic: ⟨_, _, _, hadj, ha, hb⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
C : G.Coloring (Fin n)
a b : β
left : a ≠ b
w w_1 : V
hadj : G.Adj w w_1
ha : (f : (a : V) → β) w = a
hb : (f : (a : V) → β) w_1 = b
⊢ Adj (V := Fin n) (completeGraph (Fin n))
    (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) a)
    (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) b)
have map_rel' : Adj (V := Fin n) (completeGraph (Fin n) : SimpleGraph (Fin n)) ((C : (a : V) → Fin n) w : Fin n)
  ((C : (a : V) → Fin n) w_1 : Fin n)
Tactic: rw [← ha, f.injective.extend_apply, ← hb, f.injective.extend_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
hG : G.Colorable n
f : ι → V
hf : Pairwise fun (i j : ι) ↦ G.Adj (f i) (f j)
⊢ Nat.card ι ≤ n
have obtain : ∀ (C : G.Coloring (Fin n)), Nat.card ι ≤ n
Tactic: obtain ⟨C⟩ := hG
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber = ⨅ (n : (↑{m : ℕ | G.Colorable m} : Type)), (↑(↑n : ℕ) : ℕ∞)
have rw : Eq (α := ℕ∞) (⨅ n ∈ setOf G.Colorable, (↑n : ℕ∞)) (⨅ (n : (↑{m : ℕ | G.Colorable m} : Type)), (↑(↑n : ℕ) : ℕ∞))
Tactic: rw [chromaticNumber, iInf_subtype]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
rw : Eq (α := ℕ∞) (⨅ n ∈ setOf G.Colorable, (↑n : ℕ∞)) (⨅ (n : (↑{m : ℕ | G.Colorable m} : Type)), (↑(↑n : ℕ) : ℕ∞))
⊢ G.chromaticNumber = ⨅ (n : (↑{m : ℕ | G.Colorable m} : Type)), (↑(↑n : ℕ) : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (⨅ n ∈ setOf G.Colorable, (↑n : ℕ∞))
  (⨅ (i : ℕ),
    ⨅ (h : Membership.mem (γ := Set ℕ) {m : ℕ | G.Colorable m} i),
      (↑(↑(Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | G.Colorable m} x) i h) : ℕ) : ℕ∞))
Tactic: rw [chromaticNumber, iInf_subtype]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ G.chromaticNumber = (↑(sInf {n' : ℕ | G.Colorable n'}) : ℕ∞)
have rw : Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}
Tactic: rw [ENat.coe_sInf, chromaticNumber]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α_1 : Type u_2
β_1 : Type u_3
C_1 : G.Coloring α_1
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring α
⊢ (G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α)
      ((G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β) C) =
    C
have h : ∀ (v : V),
  Eq.{u_4 + 1} (α := α)
    ((((G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α)
              ((G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β) C) :
            G.Coloring α) :
          (a : V) → α)
        v :
      α)
    ((C : (a : V) → α) v : α)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α_1 : Type u_2
β_1 : Type u_3
C_1 : G.Coloring α_1
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring β
⊢ (G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β)
      ((G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α) C) =
    C
have h : ∀ (v : V),
  Eq.{u_5 + 1} (α := β)
    ((((G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β)
              ((G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α) C) :
            G.Coloring β) :
          (a : V) → β)
        v :
      β)
    ((C : (a : V) → β) v : β)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n_1 : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Fintype α
n : ℕ
hc : G.Colorable n
hn : n ≤ card α
⊢ G.Coloring α
have hn₁ : card (Fin n) ≤ card α
Tactic: rw [← Fintype.card_fin n] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n ↔ ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n
have mp : G.Colorable n → ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
mp : G.Colorable n → ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n
⊢ G.Colorable n ↔ ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n
have mpr : (∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n) → G.Colorable n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n
have mp : ∀ (C : G.Coloring (Fin n)), ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n
Tactic: have C : G.Coloring (Fin n) := hc.toColoring (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : Embedding (V := Fin n) (completeGraph (Fin n)) (completeGraph ℕ) := Embedding.completeGraph Fin.valEmbedding
⊢ ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n
have h : ∀ (v : V), (f.toHom.comp C : (a : V) → ℕ) v < n
Tactic: use f.toHom.comp C
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), (C : (a : V) → ℕ) v < n
⊢ G.Colorable n
have mpr : V → Fin n
Tactic: refine ⟨Coloring.mk ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), (C : (a : V) → ℕ) v < n
mpr : V → Fin n
⊢ G.Colorable n
have mpr₁ : ∀ {v w : V}, G.Adj v w → (⟨(C : (a : V) → ℕ) v, sorry⟩ : Fin n) ≠ ⟨(C : (a : V) → ℕ) w, sorry⟩
Tactic: refine ⟨Coloring.mk ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), (C : (a : V) → ℕ) v < n
v w : V
hvw : G.Adj v w
⊢ (⟨(C : (a : V) → ℕ) v, ⋯⟩ : Fin n) ≠ ⟨(C : (a : V) → ℕ) w, ⋯⟩
have mpr : ¬Eq (α := ℕ) ((C : (a : V) → ℕ) v : ℕ) ((C : (a : V) → ℕ) w : ℕ)
Tactic: simp only [Fin.mk_eq_mk, Ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ G.chromaticNumber ≤ (↑n : ℕ∞)
have rw : LE.le (α := ℕ∞) (↑(sInf {n' : ℕ | G.Colorable n'}) : ℕ∞) (↑n : ℕ∞)
Tactic: rw [hc.chromaticNumber_eq_sInf]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ LE.le (α := ℕ∞) (↑(sInf {n' : ℕ | G.Colorable n'}) : ℕ∞) (↑n : ℕ∞)
have norm_cast : sInf {n' : ℕ | G.Colorable n'} ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ sInf {n' : ℕ | G.Colorable n'} ≤ n
have apply : Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} n
Tactic: apply csInf_le chromaticNumber_bddBelow
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ (↑n : ℕ∞) ↔ G.Colorable n
have refine : ∀ (h : G.chromaticNumber ≤ (↑n : ℕ∞)), G.Colorable n
Tactic: refine ⟨fun h ↦ ?_, Colorable.chromaticNumber_le⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ (↑n : ℕ∞)
⊢ G.Colorable n
have this : G.chromaticNumber ≠ ⊤
Tactic: have : G.chromaticNumber ≠ ⊤ := (trans h (WithTop.coe_lt_top n)).ne
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ (↑n : ℕ∞)
this : G.chromaticNumber ≠ ⊤
⊢ G.Colorable n
have this₁ : ∃ (n : ℕ), G.Colorable n
Tactic: rw [chromaticNumber_ne_top_iff_exists] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ (↑n : ℕ∞)
this : ∃ (n : ℕ), G.Colorable n
⊢ G.Colorable n
have obtain : ∀ (m : ℕ) (hm : G.Colorable m), G.Colorable n
Tactic: obtain ⟨m, hm⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ (↑n : ℕ∞)
m : ℕ
hm : G.Colorable m
⊢ G.Colorable n
have rw : ∀ (h : sInf {n' : ℕ | G.Colorable n'} ≤ n) (m : ℕ) (hm : G.Colorable m), G.Colorable n
Tactic: rw [hm.chromaticNumber_eq_sInf, Nat.cast_le] at h
Cleared hypotheses: h, m, hm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' : ℕ | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
⊢ G.Colorable n
have this : Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} (sInf {n' : ℕ | G.Colorable n'})
Tactic: have := Nat.sInf_mem (⟨m, hm⟩ : {n' | G.Colorable n'}.Nonempty)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
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 n
have this₁ : G.Colorable (sInf {n' : ℕ | G.Colorable n'})
Tactic: rw [Set.mem_setOf_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
have rw : G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ ¬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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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
⊢ G.chromaticNumber = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
have rw₁ : G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ G.chromaticNumber ↔
  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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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
⊢ G.chromaticNumber = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
have rw₂ : G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ (↑n : ℕ∞) < G.chromaticNumber ↔
  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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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
⊢ G.chromaticNumber = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
have rw₃ : G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ ¬G.chromaticNumber ≤ (↑n : ℕ∞) ↔
  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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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
⊢ G.chromaticNumber = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
have rw₄ : G.chromaticNumber ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ ¬G.Colorable n ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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
⊢ G.chromaticNumber = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
have rw₅ : G.chromaticNumber ≤ (↑(n + 1) : ℕ∞) ∧ ¬G.Colorable n ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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
⊢ G.chromaticNumber = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
have rw₆ : G.Colorable (n + 1) ∧ ¬G.Colorable n ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable G.chromaticNumber.toNat
have rw : G.Colorable
  (ENat.toNat (↑(Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} n) sorry) : ℕ∞))
Tactic: rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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) ⋯) : ℕ∞))
⊢ G.Colorable G.chromaticNumber.toNat
have rw₁ : Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}
Tactic: rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable G.chromaticNumber.toNat
have rw : G.Colorable (ENat.toNat (↑(sInf {n' : ℕ | G.Colorable n'}) : ℕ∞))
Tactic: classical
  rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]
  · apply Nat.find_spec
  · exact colorable_set_nonempty_of_colorable hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
rw : G.Colorable (ENat.toNat (↑(sInf {n' : ℕ | G.Colorable n'}) : ℕ∞))
⊢ G.Colorable G.chromaticNumber.toNat
have rw₁ : G.Colorable
  (ENat.toNat (↑(Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {n' : ℕ | G.Colorable n'} n) sorry) : ℕ∞))
Tactic: classical
  rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]
  · apply Nat.find_spec
  · exact colorable_set_nonempty_of_colorable hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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) ⋯) : ℕ∞))
⊢ G.Colorable G.chromaticNumber.toNat
have rw₂ : Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}
Tactic: classical
  rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]
  · apply Nat.find_spec
  · exact colorable_set_nonempty_of_colorable hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
⊢ G.Colorable G.chromaticNumber.toNat
have intro : ∀ (val : Fintype V), G.Colorable G.chromaticNumber.toNat
Tactic: cases nonempty_fintype V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
⊢ G.chromaticNumber ≤ 1
have rw : G.Colorable 1
Tactic: rw [← Nat.cast_one, chromaticNumber_le_iff_colorable]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
⊢ G.Colorable 1
have 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)
Tactic: refine ⟨Coloring.mk (fun _ => 0) ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
v w : V
⊢ G.Adj v w → Ne (α := Fin 1) ((fun (x : V) ↦ (0 : Fin 1)) v) ((fun (x : V) ↦ (0 : Fin 1)) w)
have refl : G.Adj v v → Ne (α := Fin 1) ((fun (x : V) ↦ (0 : Fin 1)) v) ((fun (x : V) ↦ (0 : Fin 1)) v)
Tactic: cases Subsingleton.elim v w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < G.chromaticNumber
have rw : LT.lt (α := ℕ) 0 (sInf {n' : ℕ | G.Colorable n'})
Tactic: rw [hc.chromaticNumber_eq_sInf, Nat.cast_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ LT.lt (α := ℕ) 0 (sInf {n' : ℕ | G.Colorable n'})
have apply : ∀ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} b → Nat.succ 0 ≤ b
Tactic: apply le_csInf (colorable_set_nonempty_of_colorable hc)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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
⊢ Nat.succ 0 ≤ m
have by_contra : ∀ (h' : ¬Nat.succ 0 ≤ m), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
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
⊢ False
have h'₁ : m < Nat.succ 0
Tactic: simp only [not_le] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
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
⊢ False
have obtain : ∀ (i : ℕ) (hi : i < m), False
Tactic: obtain ⟨i, hi⟩ := hm.some (Classical.arbitrary V)