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
rw : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber < 1 ↔ G = ⊥ ∧ Nonempty V
rw₁ : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ Nonempty V
rw₂ : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₃ : G.chromaticNumber ≤ (↑1 : ℕ∞) ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₄ : G.chromaticNumber ≤ (↑1 : ℕ∞) ∧ ¬G.chromaticNumber ≤ (↑0 : ℕ∞) ↔ G = ⊥ ∧ ¬IsEmpty V
rw₅ : G.Colorable 1 ∧ ¬G.chromaticNumber ≤ (↑0 : ℕ∞) ↔ G = ⊥ ∧ ¬IsEmpty V
⊢ G.chromaticNumber = 1 ↔ G = ⊥ ∧ Nonempty V
have rw₆ : G.Colorable 1 ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V
Tactic: rw [eq_iff_le_not_lt, Order.lt_one_iff_nonpos, ← not_isEmpty_iff, ← Nat.cast_one, ← Nat.cast_zero,
    chromaticNumber_le_iff_colorable, chromaticNumber_le_iff_colorable, colorable_one_iff,
    colorable_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
rw : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber < 1 ↔ G = ⊥ ∧ Nonempty V
rw₁ : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ Nonempty V
rw₂ : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₃ : G.chromaticNumber ≤ (↑1 : ℕ∞) ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₄ : G.chromaticNumber ≤ (↑1 : ℕ∞) ∧ ¬G.chromaticNumber ≤ (↑0 : ℕ∞) ↔ G = ⊥ ∧ ¬IsEmpty V
rw₅ : G.Colorable 1 ∧ ¬G.chromaticNumber ≤ (↑0 : ℕ∞) ↔ G = ⊥ ∧ ¬IsEmpty V
rw₆ : G.Colorable 1 ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V
⊢ G.chromaticNumber = 1 ↔ G = ⊥ ∧ Nonempty V
have rw₇ : G = ⊥ ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V
Tactic: rw [eq_iff_le_not_lt, Order.lt_one_iff_nonpos, ← not_isEmpty_iff, ← Nat.cast_one, ← Nat.cast_zero,
    chromaticNumber_le_iff_colorable, chromaticNumber_le_iff_colorable, colorable_one_iff,
    colorable_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
rw : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber < 1 ↔ G = ⊥ ∧ Nonempty V
rw₁ : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ Nonempty V
rw₂ : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₃ : G.chromaticNumber ≤ (↑1 : ℕ∞) ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₄ : G.chromaticNumber ≤ (↑1 : ℕ∞) ∧ ¬G.chromaticNumber ≤ (↑0 : ℕ∞) ↔ G = ⊥ ∧ ¬IsEmpty V
rw₅ : G.Colorable 1 ∧ ¬G.chromaticNumber ≤ (↑0 : ℕ∞) ↔ G = ⊥ ∧ ¬IsEmpty V
rw₆ : G.Colorable 1 ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₇ : G = ⊥ ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V
⊢ G.chromaticNumber = 1 ↔ G = ⊥ ∧ Nonempty V
have rw₈ : G = ⊥ ∧ ¬IsEmpty V ↔ G = ⊥ ∧ ¬IsEmpty V
Tactic: rw [eq_iff_le_not_lt, Order.lt_one_iff_nonpos, ← not_isEmpty_iff, ← Nat.cast_one, ← Nat.cast_zero,
    chromaticNumber_le_iff_colorable, chromaticNumber_le_iff_colorable, colorable_one_iff,
    colorable_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ 2 ≤ G.chromaticNumber ↔ G ≠ ⊥
have refine_1 : ∀ (h : 2 ≤ G.chromaticNumber), G ≠ ⊥
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
refine_1 : ∀ (h : 2 ≤ G.chromaticNumber), G ≠ ⊥
⊢ 2 ≤ G.chromaticNumber ↔ G ≠ ⊥
have refine_2 : ∀ (h : G ≠ ⊥), 2 ≤ G.chromaticNumber
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
h : 2 ≤ G.chromaticNumber
⊢ G ≠ ⊥
have refine_1 : ∀ (h : G = ⊥), G.chromaticNumber < 2
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
h : G = ⊥
⊢ G.chromaticNumber < 2
have pos : ∀ (h' : IsEmpty V), G.chromaticNumber < 2
Tactic: by_cases h' : IsEmpty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
h : G = ⊥
pos : ∀ (h' : IsEmpty V), G.chromaticNumber < 2
⊢ G.chromaticNumber < 2
have neg : ∀ (h' : ¬IsEmpty V), G.chromaticNumber < 2
Tactic: by_cases h' : IsEmpty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
h : G ≠ ⊥
⊢ 2 ≤ G.chromaticNumber
have refine_2 : ∀ (w w_1 : V) (h : G.Adj w w_1), 2 ≤ G.chromaticNumber
Tactic: obtain ⟨_, _, h⟩ := ne_bot_iff_exists_adj.mp h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
v w : V ⊕ W
⊢ (completeBipartiteGraph V W).Adj v w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) v) ((fun (v : V ⊕ W) ↦ v.isRight) w)
have inl : ∀ (val : V),
  (completeBipartiteGraph V W).Adj (Sum.inl val) w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
v w : V ⊕ W
inl :
  ∀ (val : V),
    (completeBipartiteGraph V W).Adj (Sum.inl val) w →
      Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)
⊢ (completeBipartiteGraph V W).Adj v w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) v) ((fun (v : V ⊕ W) ↦ v.isRight) w)
have inr : ∀ (val : W),
  (completeBipartiteGraph V W).Adj (Sum.inr val) w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val) w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)
have inl : ∀ (val_1 : V),
  (completeBipartiteGraph V W).Adj (Sum.inl val) (Sum.inl val_1) →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val_1))
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val : V
inl :
  ∀ (val_1 : V),
    (completeBipartiteGraph V W).Adj (Sum.inl val) (Sum.inl val_1) →
      Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val_1))
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val) w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)
have inl₁ : ∀ (val_1 : W),
  (completeBipartiteGraph V W).Adj (Sum.inl val) (Sum.inr val_1) →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val_1))
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val) w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)
have inr : ∀ (val_1 : V),
  (completeBipartiteGraph V W).Adj (Sum.inr val) (Sum.inl val_1) →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val_1))
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val : W
inr :
  ∀ (val_1 : V),
    (completeBipartiteGraph V W).Adj (Sum.inr val) (Sum.inl val_1) →
      Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val_1))
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val) w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)
have inr₁ : ∀ (val_1 : W),
  (completeBipartiteGraph V W).Adj (Sum.inr val) (Sum.inr val_1) →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val_1))
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
⊢ (completeBipartiteGraph V W).chromaticNumber = 2
have rw : ∀ (C : (completeBipartiteGraph V W).Coloring (Fin 2)), Surjective (α := V ⊕ W) (β := Fin 2) (⇑C : (a : V ⊕ W) → Fin 2)
Tactic: rw [← Nat.cast_two, chromaticNumber_eq_iff_forall_surjective
    (by simpa using (CompleteBipartiteGraph.bicoloring V W).colorable)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
have have : ∀ (v : V), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
Tactic: have v := Classical.arbitrary V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
have have : ∀ (w : W), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
Tactic: have w := Classical.arbitrary W
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
Tactic: have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
have pos : ∀ (he : (C : (a : V ⊕ W) → Fin 2) (Sum.inl v) = b), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
Tactic: by_cases he : C (Sum.inl v) = b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
pos : ∀ (he : (C : (a : V ⊕ W) → Fin 2) (Sum.inl v) = b), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
have neg : ∀ (he : ¬(C : (a : V ⊕ W) → Fin 2) (Sum.inl v) = b), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
Tactic: by_cases he : C (Sum.inl v) = b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬(C : (a : V ⊕ W) → Fin 2) (Sum.inl v) = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
have pos : ∀ (he' : (C : (a : V ⊕ W) → Fin 2) (Sum.inr w) = b), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
Tactic: by_cases he' : C (Sum.inr w) = b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬(C : (a : V ⊕ W) → Fin 2) (Sum.inl v) = b
pos : ∀ (he' : (C : (a : V ⊕ W) → Fin 2) (Sum.inr w) = b), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
have neg : ∀ (he' : ¬(C : (a : V ⊕ W) → Fin 2) (Sum.inr w) = b), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
Tactic: by_cases he' : C (Sum.inr w) = b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ (↑G.cliqueNum : ℕ∞) ≤ G.chromaticNumber
have have : ∀ (s : Finset V) (hs : G.IsNClique G.cliqueNum s), (↑G.cliqueNum : ℕ∞) ≤ G.chromaticNumber
Tactic: have ⟨s, hs⟩ := G.exists_isNClique_cliqueNum
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
⊢ G.CliqueFree m
have by_contra : ∀ (h : ¬G.CliqueFree m), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ¬G.CliqueFree m
⊢ False
have h₁ : ∃ (x : Finset V), G.IsClique (↑x : Set V) ∧ x.card = m
Tactic: simp only [CliqueFree, isNClique_iff, not_forall, Classical.not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ∃ (x : Finset V), G.IsClique (↑x : Set V) ∧ x.card = m
⊢ False
have obtain : ∀ (s : Finset V) (h : G.IsClique (↑s : Set V)) (hm : n < s.card), False
Tactic: obtain ⟨s, h, rfl⟩ := h
Cleared hypotheses: m, hm, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
⊢ G.CliqueFree n
have hne : G.chromaticNumber ≠ ⊤
Tactic: have hne : G.chromaticNumber ≠ ⊤ := hc.ne_top
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : G.chromaticNumber ≠ ⊤
⊢ G.CliqueFree n
have obtain : ∀ (m : ℕ) (hc' : G.Colorable m), G.CliqueFree n
Tactic: obtain ⟨m, hc'⟩ := chromaticNumber_ne_top_iff_exists.mp hne
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
⊢ G.CliqueFree n
have this : G.Colorable G.chromaticNumber.toNat
Tactic: have := colorable_chromaticNumber hc'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.CliqueFree n
have refine : G.chromaticNumber.toNat < n
Tactic: refine this.cliqueFree ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n
have rw : ∀ (hne : (↑G.chromaticNumber.toNat : ℕ∞) = G.chromaticNumber) (m : ℕ) (hc' : G.Colorable m)
  (this : G.Colorable G.chromaticNumber.toNat), G.chromaticNumber.toNat < n
Tactic: rw [← ENat.coe_toNat_eq_self] at hne
Cleared hypotheses: hne, m, hc', this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : (↑G.chromaticNumber.toNat : ℕ∞) = G.chromaticNumber
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n
have rw : ∀ (hc : LT.lt (α := ℕ∞) (↑G.chromaticNumber.toNat : ℕ∞) (↑n : ℕ∞))
  (hne : (↑G.chromaticNumber.toNat : ℕ∞) = G.chromaticNumber) (m : ℕ) (hc' : G.Colorable m)
  (this : G.Colorable G.chromaticNumber.toNat), G.chromaticNumber.toNat < n
Tactic: rw [← hne] at hc
Cleared hypotheses: hc, hne, m, hc', this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
s : Finset V
h : G.IsClique (↑s : Set V)
hc : card α ≤ s.card
C : G.Coloring α
a : α
h_1 : Membership.mem (γ := Set α) Set.univ a
⊢ Membership.mem (γ := Set α) ((⇑C : (a : V) → α) '' (↑s : Set V)) a
have obtain : ∀ (w : (↑(↑s : Set V) : Type u))
  (hx : (Hom.comp C (Embedding.toHom (Embedding.induce (↑s : Set V))) : (a : (↑(↑s : Set V) : Type u)) → α) w = a),
  Membership.mem (γ := Set α) ((⇑C : (a : V) → α) '' (↑s : Set V)) a
Tactic: obtain ⟨_, hx⟩ := card_le_chromaticNumber_iff_forall_surjective.mp
                    (by simp_all [isClique_iff_induce_eq]) (C.comp (Embedding.induce s).toHom) _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
ι : Type u_4
V : ι → Type u_5
inst : Fintype ι
f : (i : ι) → V i
⊢ (completeMultipartiteGraph V).chromaticNumber = (↑(card ι) : ℕ∞)
have apply : (↑(card ι) : ℕ∞) ≤ (completeMultipartiteGraph V).chromaticNumber
Tactic: apply le_antisymm (colorable V).chromaticNumber_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
ι : Type u_4
V : ι → Type u_5
inst : Fintype ι
f : (i : ι) → V i
⊢ (↑(card ι) : ℕ∞) ≤ (completeMultipartiteGraph V).chromaticNumber
have by_contra! : ∀ (h : (completeMultipartiteGraph V).chromaticNumber < (↑(card ι) : ℕ∞)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
⊢ (completeMultipartiteGraph V).Colorable (n + 1 - 1)
have succ : ∀ (this : Fintype ι), (completeMultipartiteGraph V).Colorable (n + 1 - 1)
Tactic: have : Fintype ι := fintypeOfNotInfinite
    fun hinf ↦ not_cliqueFree_of_infinite V f hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
this : Fintype ι
⊢ (completeMultipartiteGraph V).Colorable (n + 1 - 1)
have succ : card ι ≤ n + 1 - 1
Tactic: apply (coloring V).colorable.mono
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
this : Fintype ι
⊢ card ι ≤ n + 1 - 1
have this₁ : ¬(completeMultipartiteGraph V).CliqueFree (card ι)
Tactic: have := not_cliqueFree_of_le_card V f le_rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
this_1 : Fintype ι
this : ¬(completeMultipartiteGraph V).CliqueFree (card ι)
⊢ card ι ≤ n + 1 - 1
have succ : ∀ (this : n + 1 - 1 < card ι), (completeMultipartiteGraph V).CliqueFree (card ι)
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
n : ℕ
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
hc : (completeMultipartiteGraph V).CliqueFree n
⊢ (completeMultipartiteGraph V).Colorable (n - 1)
have zero : ∀ (hc : (completeMultipartiteGraph V).CliqueFree 0), (completeMultipartiteGraph V).Colorable (HSub.hSub (α := ℕ) 0 1)
Tactic: cases n with
  | zero => exact absurd hc not_cliqueFree_zero
  | succ n =>
  have : Fintype ι := fintypeOfNotInfinite
    fun hinf ↦ not_cliqueFree_of_infinite V f hc
  apply (coloring V).colorable.mono
  have := not_cliqueFree_of_le_card V f le_rfl
  contrapose! this
  exact hc.mono this
Cleared hypotheses: n, hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
n : ℕ
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
hc : (completeMultipartiteGraph V).CliqueFree n
zero :
  ∀ (hc : (completeMultipartiteGraph V).CliqueFree 0), (completeMultipartiteGraph V).Colorable (HSub.hSub (α := ℕ) 0 1)
⊢ (completeMultipartiteGraph V).Colorable (n - 1)
have succ : ∀ (n : ℕ) (hc : (completeMultipartiteGraph V).CliqueFree (n + 1)), (completeMultipartiteGraph V).Colorable (n + 1 - 1)
Tactic: cases n with
  | zero => exact absurd hc not_cliqueFree_zero
  | succ n =>
  have : Fintype ι := fintypeOfNotInfinite
    fun hinf ↦ not_cliqueFree_of_infinite V f hc
  apply (coloring V).colorable.mono
  have := not_cliqueFree_of_le_card V f le_rfl
  contrapose! this
  exact hc.mono this
Cleared hypotheses: n, hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
W : Type u_4
H : SimpleGraph W
nhc : ¬H.Colorable n
hc : G.Colorable n
⊢ H.Free G
have contrapose : ∀ (hc' : H ⊑ G), H.Colorable n
Tactic: contrapose nhc with hc'
Cleared hypotheses: nhc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
x y : α
h' : ¬G.Adj x y
⊢ ¬G.Adj y x
have rwa : ∀ (h' : ¬G.Adj y x), ¬G.Adj y x
Tactic: rwa [adj_comm] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α},
    Adj.{u} (V := (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x })
        (completeMultipartiteGraph fun (c : Quotient h.setoid) ↦ { x : α // (h.setoid : α → α → Prop) c.out x })
        (({
              toFun := fun (x : α) ↦
                Sigma.mk (β := fun (i : Quotient h.setoid) ↦ { x : α // (h.setoid : α → α → Prop) i.out x }) ⟦x⟧
                  (Subtype.mk (p := fun (x_1 : α) ↦ (h.setoid : α → α → Prop) ⟦x⟧.out x_1) x ⋯),
              invFun := fun (x : (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x }) ↦
                match (motive := (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x } → α) x with
                | ⟨fst, x⟩ => (↑x : α),
              left_inv := ⋯, right_inv := ⋯ :
              α ≃ (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x } } :
            (a : α) → (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x })
          a)
        (({
              toFun := fun (x : α) ↦
                Sigma.mk (β := fun (i : Quotient h.setoid) ↦ { x : α // (h.setoid : α → α → Prop) i.out x }) ⟦x⟧
                  (Subtype.mk (p := fun (x_1 : α) ↦ (h.setoid : α → α → Prop) ⟦x⟧.out x_1) x ⋯),
              invFun := fun (x : (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x }) ↦
                match (motive := (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x } → α) x with
                | ⟨fst, x⟩ => (↑x : α),
              left_inv := ⋯, right_inv := ⋯ :
              α ≃ (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x } } :
            (a : α) → (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x })
          b) ↔
      G.Adj a b
have simp_rw : ∀ {a b : α}, ¬(h.setoid : α → α → Prop) a b ↔ G.Adj a b
Tactic: simp_rw [Equiv.coe_fn_mk, comap_adj, top_adj, ne_eq, Quotient.eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
a b : α
⊢ ¬¬G.Adj a b ↔ G.Adj a b
have rw : G.Adj a b ↔ G.Adj a b
Tactic: rw [not_not]