awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬(Odd v ↔ Even v)
have inl : ¬Odd v ↔ Even v
Tactic: apply Classical.not_iff.mpr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
have inr : ¬(Even u ↔ Odd u)
Tactic: rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h,
          ← Fin.even_iff_mod_of_even h, Fin.even_add_one_iff_odd]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(Even u ↔ Odd u)
have inr : ¬Even u ↔ Odd u
Tactic: apply Classical.not_iff.mpr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
⊢ ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
have inl : ∀ (huv : u - v = 1), ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
Tactic: cases hadj with
      | inl huv | inr huv =>
        rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h,
          ← Fin.even_iff_mod_of_even h, Fin.even_add_one_iff_odd]
        apply Classical.not_iff.mpr
        simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
inl : ∀ (huv : u - v = 1), ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
⊢ ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
have inr : ∀ (huv : v - u = 1), ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
Tactic: cases hadj with
      | inl huv | inr huv =>
        rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h,
          ← Fin.even_iff_mod_of_even h, Fin.even_add_one_iff_odd]
        apply Classical.not_iff.mpr
        simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
⊢ (cycleGraph n).chromaticNumber = 2
have hc : (cycleGraph n).Colorable (Fintype.card Bool)
Tactic: have hc := (cycleGraph.bicoloring_of_even n hEven).colorable
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).chromaticNumber = 2
have a : (cycleGraph n).chromaticNumber ≤ 2
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
a : (cycleGraph n).chromaticNumber ≤ 2
⊢ (cycleGraph n).chromaticNumber = 2
have a₁ : 2 ≤ (cycleGraph n).chromaticNumber
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ 2 ≤ (cycleGraph n).chromaticNumber
have hadj : (cycleGraph n).Adj ⟨0, sorry⟩ ⟨1, h⟩
Tactic: have hadj : (cycleGraph n).Adj ⟨0, Nat.zero_lt_of_lt h⟩ ⟨1, h⟩ := by
      simp [cycleGraph_adj', Fin.sub_val_of_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : Adj (cycleGraph (n + 2)) u v
⊢ (if (↑u : ℕ) = n + 2 - 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) ≠
    if (↑v : ℕ) = n + 2 - 1 then 2 else ⟨(↑v : ℕ) % 2, ⋯⟩
have hadj₁ : u - v = 1 ∨ v - u = 1
Tactic: simp only [cycleGraph_adj] at hadj
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
⊢ (if (↑u : ℕ) = n + 2 - 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) ≠
    if (↑v : ℕ) = n + 2 - 1 then 2 else ⟨(↑v : ℕ) % 2, ⋯⟩
have pos : ∀ (hu : (↑u : ℕ) = n + 2 - 1) (hv : (↑v : ℕ) = n + 2 - 1), Ne (α := Fin 3) 2 2
Tactic: split_ifs with hu hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
pos : ∀ (hu : (↑u : ℕ) = n + 2 - 1) (hv : (↑v : ℕ) = n + 2 - 1), Ne (α := Fin 3) 2 2
⊢ (if (↑u : ℕ) = n + 2 - 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) ≠
    if (↑v : ℕ) = n + 2 - 1 then 2 else ⟨(↑v : ℕ) % 2, ⋯⟩
have neg : ∀ (hu : (↑u : ℕ) = n + 2 - 1) (hv : ¬(↑v : ℕ) = n + 2 - 1), 2 ≠ (⟨(↑v : ℕ) % 2, sorry⟩ : Fin 3)
Tactic: split_ifs with hu hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
pos : ∀ (hu : (↑u : ℕ) = n + 2 - 1) (hv : (↑v : ℕ) = n + 2 - 1), Ne (α := Fin 3) 2 2
neg : ∀ (hu : (↑u : ℕ) = n + 2 - 1) (hv : ¬(↑v : ℕ) = n + 2 - 1), 2 ≠ (⟨(↑v : ℕ) % 2, ⋯⟩ : Fin 3)
⊢ (if (↑u : ℕ) = n + 2 - 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) ≠
    if (↑v : ℕ) = n + 2 - 1 then 2 else ⟨(↑v : ℕ) % 2, ⋯⟩
have pos₁ : ∀ (hu : ¬(↑u : ℕ) = n + 2 - 1), (↑v : ℕ) = n + 2 - 1 → (⟨(↑u : ℕ) % 2, sorry⟩ : Fin 3) ≠ 2
Tactic: split_ifs with hu hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
pos : ∀ (hu : (↑u : ℕ) = n + 2 - 1) (hv : (↑v : ℕ) = n + 2 - 1), Ne (α := Fin 3) 2 2
neg : ∀ (hu : (↑u : ℕ) = n + 2 - 1) (hv : ¬(↑v : ℕ) = n + 2 - 1), 2 ≠ (⟨(↑v : ℕ) % 2, ⋯⟩ : Fin 3)
pos₁ : ∀ (hu : ¬(↑u : ℕ) = n + 2 - 1), (↑v : ℕ) = n + 2 - 1 → (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3) ≠ 2
⊢ (if (↑u : ℕ) = n + 2 - 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) ≠
    if (↑v : ℕ) = n + 2 - 1 then 2 else ⟨(↑v : ℕ) % 2, ⋯⟩
have neg₁ : ∀ (hu : ¬(↑u : ℕ) = n + 2 - 1), ¬(↑v : ℕ) = n + 2 - 1 → (⟨(↑u : ℕ) % 2, sorry⟩ : Fin 3) ≠ ⟨(↑v : ℕ) % 2, sorry⟩
Tactic: split_ifs with hu hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : (↑u : ℕ) = n + 2 - 1
hv : ¬(↑v : ℕ) = n + 2 - 1
⊢ 2 ≠ (⟨(↑v : ℕ) % 2, ⋯⟩ : Fin 3)
have neg : (↑v : ℕ) % 2 < (↑2 : ℕ)
Tactic: refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val (?_))).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : (↑v : ℕ) = n + 2 - 1
⊢ (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3) ≠ 2
have pos : (↑u : ℕ) % 2 < (↑2 : ℕ)
Tactic: refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val ?_))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
⊢ (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3) ≠ ⟨(↑v : ℕ) % 2, ⋯⟩
have neg : ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
Tactic: simp only [ne_eq, Fin.ext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
⊢ (↑u : ℕ) + (↑1 : ℕ) < n + 2
have fin_omega : ∀ (h : LE.le (α := ℤ) (↑2 : ℤ) (↑(n + 2) : ℤ)), LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ)
Tactic: fin_omega
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
⊢ ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
have hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
Tactic: have hu' : u.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
⊢ (↑v : ℕ) + (↑1 : ℕ) < n + 2
have fin_omega : ∀ (h : LE.le (α := ℤ) (↑2 : ℤ) (↑(n + 2) : ℤ)) (hu' : LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ)),
  LT.lt (α := ℤ) (↑((↑v : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ)
Tactic: fin_omega
Cleared hypotheses: h, hu'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
⊢ ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
have hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
Tactic: have hv' : v.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : u - v = 1
⊢ ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
have neg : ¬(↑(v + 1) : ℕ) % 2 = (↑v : ℕ) % 2
Tactic: rw [← add_eq_of_eq_sub' huv.symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : u - v = 1
⊢ ¬(↑(v + 1) : ℕ) % 2 = (↑v : ℕ) % 2
have neg : ¬((↑v : ℕ) + 1) % 2 = (↑v : ℕ) % 2
Tactic: simp only [Fin.val_add_eq_of_add_lt hv', Fin.val_add_eq_of_add_lt hu', Fin.val_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : u - v = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (Even x ↔ Even y)
have simp : ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)
Tactic: simp [Nat.even_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : u - v = 1
⊢ ¬((↑v : ℕ) + 1) % 2 = (↑v : ℕ) % 2
have neg : ¬((Even (↑v : ℕ) ↔ Even (α := ℕ) 1) ↔ Even (↑v : ℕ))
Tactic: rw [show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,
            Nat.even_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : u - v = 1
⊢ ¬((Even (↑v : ℕ) ↔ Even (α := ℕ) 1) ↔ Even (↑v : ℕ))
have neg : ¬False
Tactic: simp only [Nat.not_even_one, iff_false, not_iff_self, iff_not_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : v - u = 1
⊢ ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
have neg : ¬(↑u : ℕ) % 2 = (↑(u + 1) : ℕ) % 2
Tactic: rw [← add_eq_of_eq_sub' huv.symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : v - u = 1
⊢ ¬(↑u : ℕ) % 2 = (↑(u + 1) : ℕ) % 2
have neg : ¬(↑u : ℕ) % 2 = ((↑u : ℕ) + 1) % 2
Tactic: simp only [Fin.val_add_eq_of_add_lt hv', Fin.val_add_eq_of_add_lt hu', Fin.val_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : v - u = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (Even x ↔ Even y)
have simp : ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)
Tactic: simp [Nat.even_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : v - u = 1
⊢ ¬(↑u : ℕ) % 2 = ((↑u : ℕ) + 1) % 2
have neg : ¬(Even (↑u : ℕ) ↔ (Even (↑u : ℕ) ↔ Even (α := ℕ) 1))
Tactic: rw [show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,
            Nat.even_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
huv : v - u = 1
⊢ ¬(Even (↑u : ℕ) ↔ (Even (↑u : ℕ) ↔ Even (α := ℕ) 1))
have neg : ¬False
Tactic: simp only [Nat.not_even_one, iff_false, not_iff_self, iff_not_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
⊢ ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
have neg : ∀ (huv : u - v = 1), ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
Tactic: cases hadj with
        | inl huv | inr huv =>
          rw [← add_eq_of_eq_sub' huv.symm]
          simp only [Fin.val_add_eq_of_add_lt hv', Fin.val_add_eq_of_add_lt hu', Fin.val_one]
          rw [show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,
            Nat.even_add]
          simp only [Nat.not_even_one, iff_false, not_iff_self, iff_not_self]
          exact id
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬(↑u : ℕ) = n + 2 - 1
h_1 : ¬(↑v : ℕ) = n + 2 - 1
hu' : (↑u : ℕ) + (↑1 : ℕ) < n + 2
hv' : (↑v : ℕ) + (↑1 : ℕ) < n + 2
neg : ∀ (huv : u - v = 1), ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
⊢ ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
have neg₁ : ∀ (huv : v - u = 1), ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
Tactic: cases hadj with
        | inl huv | inr huv =>
          rw [← add_eq_of_eq_sub' huv.symm]
          simp only [Fin.val_add_eq_of_add_lt hv', Fin.val_add_eq_of_add_lt hu', Fin.val_one]
          rw [show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,
            Nat.even_add]
          simp only [Nat.not_even_one, iff_false, not_iff_self, iff_not_self]
          exact id
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
⊢ (cycleGraph n).chromaticNumber = 3
have hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
Tactic: have hc := (cycleGraph.tricoloring n h).colorable
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ (cycleGraph n).chromaticNumber = 3
have a : (cycleGraph n).chromaticNumber ≤ 3
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
a : (cycleGraph n).chromaticNumber ≤ 3
⊢ (cycleGraph n).chromaticNumber = 3
have a₁ : 3 ≤ (cycleGraph n).chromaticNumber
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ n - 3 + 3 = n
have refine : ¬2 = n
Tactic: refine Nat.sub_add_cancel (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne h ?_))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
h2 : 2 = n
⊢ False
have hOdd₁ : Odd (α := ℕ) 2
Tactic: rw [← h2] at hOdd
Cleared hypotheses: hOdd, hc, h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ 3 ≤ (cycleGraph n).chromaticNumber
have hn3 : n - 3 + 3 = n
Tactic: have hn3 : n - 3 + 3 = n := by
      refine Nat.sub_add_cancel (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne h ?_))
      intro h2
      rw [← h2] at hOdd
      exact (Nat.not_odd_iff.mpr rfl) hOdd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
hn3 : n - 3 + 3 = n
w : Walk (V := Fin (n - 3 + 3)) (cycleGraph (n - 3 + 3)) 0 0 := cycleGraph.cycle (n - 3)
⊢ 3 ≤ (cycleGraph n).chromaticNumber
have hOdd' : Odd w.length
Tactic: have hOdd' : Odd w.length := by
      rw [cycleGraph.length_cycle, hn3]
      exact hOdd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
hn3 : n - 3 + 3 = n
w : Walk (V := Fin (n - 3 + 3)) (cycleGraph (n - 3 + 3)) 0 0 := cycleGraph.cycle (n - 3)
hOdd' : Odd w.length
⊢ 3 ≤ (cycleGraph n).chromaticNumber
have a : 3 ≤ chromaticNumber (V := Fin (n - 3 + 3)) (cycleGraph (n - 3 + 3))
Tactic: rw [← hn3]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), Even w.length
have simp_rw : G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
Tactic: simp_rw [← Nat.not_odd_iff_even]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
have mp : G.Colorable 2 → ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
mp : G.Colorable 2 → ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
have mpr : (∀ (u : α) (w : G.Walk u u), ¬Odd w.length) → G.Colorable 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u : α
w : G.Walk u u
ho : Odd w.length
⊢ False
have this : LE.le (α := ℕ∞) 3 (↑2 : ℕ∞)
Tactic: have := (w.three_le_chromaticNumber_of_odd_loop ho).trans h.chromaticNumber_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
⊢ G.Colorable 2
have mpr : ∀ (c : G.ConnectedComponent), c.toSimpleGraph.Colorable 2
Tactic: apply colorable_iff_forall_connectedComponents.2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
⊢ c.toSimpleGraph.Colorable 2
have mpr : ∀ (w : α) (hv : w ∈ c.supp), c.toSimpleGraph.Colorable 2
Tactic: obtain ⟨_, hv⟩ := c.nonempty_supp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w : α
hv : w ∈ c.supp
⊢ c.toSimpleGraph.Colorable 2
have map_rel' : ∀ {a b : ↥c},
  c.toSimpleGraph.Adj a b →
    Adj (V := Fin 2) (completeGraph (Fin 2))
      (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry)))
      (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry)))
Tactic: use fun a ↦ Fin.ofNat 2 (c.connected_toSimpleGraph ⟨_, hv⟩ a).some.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w : α
hv : w ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he :
  Eq (α := Fin 2) (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
    (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
⊢ False
have map_rel' : Odd
  (length (u := (c.toSimpleGraph_hom : (a : ↥c) → α) (Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv)) (v :=
    (c.toSimpleGraph_hom : (a : ↥c) → α) (Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv))
    (Walk.map c.toSimpleGraph_hom (append (concat (Nonempty.some sorry) hab) (reverse (Nonempty.some sorry)))))
Tactic: apply h _ <| (((c.connected_toSimpleGraph ⟨_, hv⟩ a).some.concat hab).append
                 (c.connected_toSimpleGraph ⟨_, hv⟩ b).some.reverse).map c.toSimpleGraph_hom
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w : α
hv : w ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he :
  Eq (α := Fin 2) (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
    (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
⊢ Odd
    (length (u := (c.toSimpleGraph_hom : (a : ↥c) → α) (Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv)) (v :=
      (c.toSimpleGraph_hom : (a : ↥c) → α) (Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv))
      (Walk.map c.toSimpleGraph_hom (append (concat (Nonempty.some ⋯) hab) (reverse (Nonempty.some ⋯)))))
have map_rel' : Odd
  (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry) +
      length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry) +
    1)
Tactic: rw [length_map, length_append, length_concat, length_reverse, add_right_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w : α
hv : w ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he :
  Eq (α := Fin 2) (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
    (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
⊢ length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯) % 2 =
    length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯) % 2
have simp_rw : (↑(↑(length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry)) : Fin 2) : ℕ) =
  (↑(↑(length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry)) : Fin 2) : ℕ)
Tactic: simp_rw [← Fin.val_natCast, ← Fin.ofNat_eq_cast, he]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w : α
hv : w ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he :
  Eq (α := Fin 2) (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
    (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
simp_rw :
  (↑(↑(length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)) : Fin 2) : ℕ) =
    (↑(↑(length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)) : Fin 2) : ℕ)
⊢ length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯) % 2 =
    length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯) % 2
have simp_rw₁ : (↑(Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry))) : ℕ) =
  (↑(Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry))) : ℕ)
Tactic: simp_rw [← Fin.val_natCast, ← Fin.ofNat_eq_cast, he]