awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
rw : ¬Eq (α := Bool) ((c : (a : α) → Bool) u : Bool) ((c : (a : α) → Bool) v : Bool)
⊢ ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true

Tactic:
rw [← not_iff, ← Bool.eq_iff_iff]

Premises used: Bool.eq_iff_iff, not_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
⊢ ¬Eq (α := Bool) ((c : (a : α) → Bool) u : Bool) ((c : (a : α) → Bool) v : Bool)

Tactic:
c.valid h

Premises used: SimpleGraph.Coloring.valid
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
⊢ ¬Eq (α := Bool) ((c : (a : α) → Bool) u : Bool) ((c : (a : α) → Bool) v : Bool)

Tactic:
exact c.valid h

Premises used: SimpleGraph.Coloring.valid
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
⊢ ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true

Tactic:
have : ¬ c u = true ↔ c v = true := by
      rw [← not_iff, ← Bool.eq_iff_iff]
      exact c.valid h
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
nil :
  ∀ {u : α},
    Even (Walk.length.{u_1} (V := α) (G := G) (u := u) Walk.nil) ↔
      ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) u = true)
cons :
  ∀ {u v w : α} (h : G.Adj u v) (p : G.Walk v w)
    (ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)),
    Even (Walk.cons h p).length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
⊢ Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)

Tactic:
induction p with
  | nil => simp
  | @cons u v w h p ih =>
    simp only [Walk.length_cons, Nat.even_add_one]
    have : ¬ c u = true ↔ c v = true := by
      rw [← not_iff, ← Bool.eq_iff_iff]
      exact c.valid h
    tauto

Premises used: Nat.even_add_one, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
rw :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
⊢ Odd p.length ↔ (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)

Tactic:
rw [← Nat.not_even_iff_odd, c.even_length_iff_congr p]

Premises used: Nat.not_even_iff_odd, SimpleGraph.Coloring.even_length_iff_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
⊢ G.chromaticNumber ≤ 2

Tactic:
have h' : G.chromaticNumber ≤ 2 := Order.le_of_lt_add_one <| not_le.mp h
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv : (a : G.Coloring (Fin 2)) → G.Coloring Bool) c
⊢ ¬(c' : (a : α) → Bool) u = true ↔ (c' : (a : α) → Bool) u = true

Tactic:
have : ¬c' u ↔ c' u := (c'.odd_length_iff_not_congr p).mp hOdd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv : (a : G.Coloring (Fin 2)) → G.Coloring Bool) c
this : ¬(c' : (a : α) → Bool) u = true ↔ (c' : (a : α) → Bool) u = true
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : Even (α := ℕ) 0
u v : Fin 0
hadj : Adj (cycleGraph 0) u v
⊢ Ne (α := Bool) ((fun (u : Fin 0) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin 0) ↦ decide ((↑u : ℕ) % 2 = 0)) v)

Tactic:
u.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : Even (α := ℕ) 0
u v : Fin 0
hadj : Adj (cycleGraph 0) u v
⊢ Ne (α := Bool) ((fun (u : Fin 0) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin 0) ↦ decide ((↑u : ℕ) % 2 = 0)) v)

Tactic:
exact u.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : Even (α := ℕ) 1
u v : Fin 1
hadj : Adj (cycleGraph 1) u v
⊢ Ne (α := Bool) ((fun (u : Fin 1) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin 1) ↦ decide ((↑u : ℕ) % 2 = 0)) v)

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
hadj : Adj (cycleGraph (n + 2)) u v
simp : ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
⊢ Ne (α := Bool) ((fun (u : Fin (n + 2)) ↦ decide ((↑u : ℕ) % 2 = 0)) u)
    ((fun (u : Fin (n + 2)) ↦ decide ((↑u : ℕ) % 2 = 0)) v)

Tactic:
simp only [ne_eq, decide_eq_decide]

Premises used: decide_eq_decide, ne_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
hadj : Adj (cycleGraph (n + 2)) u v
⊢ u - v = 1 ∨ v - u = 1

Tactic:
simp only [cycleGraph_adj] at hadj

Premises used: SimpleGraph.cycleGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
inl : ¬(Odd v ↔ Even v)
⊢ ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)

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]

Premises used: Fin.even_add_one_iff_odd, Fin.even_iff_mod_of_even, add_eq_of_eq_sub', Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
inl : ¬Odd v ↔ Even v
⊢ ¬(Odd v ↔ Even v)

Tactic:
apply Classical.not_iff.mpr

Premises used: Iff.mpr, Classical.not_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬Odd v ↔ Even v

Tactic:
simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

Premises used: Fin.not_odd_iff_even_of_even, Fin.not_even_iff_odd_of_even
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
inr : ¬(Even u ↔ Odd u)
⊢ ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)

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]

Premises used: Fin.even_add_one_iff_odd, Fin.even_iff_mod_of_even, add_eq_of_eq_sub', Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
inr : ¬Even u ↔ Odd u
⊢ ¬(Even u ↔ Odd u)

Tactic:
apply Classical.not_iff.mpr

Premises used: Iff.mpr, Classical.not_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬Even u ↔ Odd u

Tactic:
simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

Premises used: Fin.not_odd_iff_even_of_even, Fin.not_even_iff_odd_of_even
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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)
inr : ∀ (huv : v - u = 1), ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
⊢ ¬((↑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]

Premises used: Iff.mpr, Fin.not_odd_iff_even_of_even, Classical.not_iff, Fin.even_add_one_iff_odd, Fin.even_iff_mod_of_even, Fin.not_even_iff_odd_of_even
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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)

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]

Premises used: Iff.mpr, Fin.not_odd_iff_even_of_even, Classical.not_iff, Fin.even_add_one_iff_odd, Fin.even_iff_mod_of_even, Fin.not_even_iff_odd_of_even
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : Even n
u v : Fin n
hadj : (cycleGraph n).Adj u v
⊢ Ne (α := Bool) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) v)

Tactic:
match n with
    | 0 => exact u.elim0
    | 1 => simp at h
    | n + 2 =>
      simp only [ne_eq, decide_eq_decide]
      simp only [cycleGraph_adj] at hadj
      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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
⊢ (cycleGraph n).Colorable (Fintype.card Bool)

Tactic:
have hc := (cycleGraph.bicoloring_of_even n hEven).colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
a : (cycleGraph n).chromaticNumber ≤ 2
a₁ : 2 ≤ (cycleGraph n).chromaticNumber
⊢ (cycleGraph n).chromaticNumber = 2

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).chromaticNumber ≤ 2

Tactic:
apply hc.chromaticNumber_le

Premises used: SimpleGraph.Colorable.chromaticNumber_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩

Tactic:
simp [cycleGraph_adj', Fin.sub_val_of_le]

Premises used: Fin.sub_val_of_le, SimpleGraph.cycleGraph_adj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).Adj ⟨0, ⋯⟩ ⟨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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
hadj : (cycleGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩
⊢ 2 ≤ (cycleGraph n).chromaticNumber

Tactic:
two_le_chromaticNumber_of_adj hadj

Premises used: SimpleGraph.two_le_chromaticNumber_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
hadj : (cycleGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩
⊢ 2 ≤ (cycleGraph n).chromaticNumber

Tactic:
exact two_le_chromaticNumber_of_adj hadj

Premises used: SimpleGraph.two_le_chromaticNumber_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
u : Fin n
⊢ (↑u : ℕ) % 2 < 3

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : LE.le (α := ℕ) 2 0
u v : Fin 0
hadj : Adj (cycleGraph 0) u v
⊢ Ne (α := Fin 3) ((fun (u : Fin 0) ↦ if (↑u : ℕ) = HSub.hSub (α := ℕ) 0 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) u)
    ((fun (u : Fin 0) ↦ if (↑u : ℕ) = HSub.hSub (α := ℕ) 0 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) v)

Tactic:
u.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : LE.le (α := ℕ) 2 0
u v : Fin 0
hadj : Adj (cycleGraph 0) u v
⊢ Ne (α := Fin 3) ((fun (u : Fin 0) ↦ if (↑u : ℕ) = HSub.hSub (α := ℕ) 0 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) u)
    ((fun (u : Fin 0) ↦ if (↑u : ℕ) = HSub.hSub (α := ℕ) 0 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) v)

Tactic:
exact u.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : LE.le (α := ℕ) 2 1
u v : Fin 1
hadj : Adj (cycleGraph 1) u v
⊢ Ne (α := Fin 3) ((fun (u : Fin 1) ↦ if (↑u : ℕ) = HSub.hSub (α := ℕ) 1 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) u)
    ((fun (u : Fin 1) ↦ if (↑u : ℕ) = HSub.hSub (α := ℕ) 1 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) v)

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n_1 n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : Adj (cycleGraph (n + 2)) u v
⊢ u - v = 1 ∨ v - u = 1

Tactic:
simp only [cycleGraph_adj] at hadj

Premises used: SimpleGraph.cycleGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
neg₁ : ∀ (hu : ¬(↑u : ℕ) = n + 2 - 1), ¬(↑v : ℕ) = n + 2 - 1 → (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3) ≠ ⟨(↑v : ℕ) % 2, ⋯⟩
⊢ (if (↑u : ℕ) = n + 2 - 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) ≠
    if (↑v : ℕ) = n + 2 - 1 then 2 else ⟨(↑v : ℕ) % 2, ⋯⟩

Tactic:
split_ifs with hu hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
⊢ Ne (α := Fin 3) 2 2

Tactic:
simp [Fin.eq_mk_iff_val_eq.mpr hu, Fin.eq_mk_iff_val_eq.mpr hv] at hadj

Premises used: Iff.mpr, Fin.eq_mk_iff_val_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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)

Tactic:
(Fin.ne_of_lt (Fin.mk_lt_of_lt_val (?_))).symm

Premises used: Fin.ne_of_lt, Fin.mk_lt_of_lt_val, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
neg : (↑v : ℕ) % 2 < (↑2 : ℕ)
⊢ 2 ≠ (⟨(↑v : ℕ) % 2, ⋯⟩ : Fin 3)

Tactic:
refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val (?_))).symm

Premises used: Fin.ne_of_lt, Fin.mk_lt_of_lt_val, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
⊢ (↑v : ℕ) % 2 < (↑2 : ℕ)

Tactic:
v.val.mod_lt Nat.zero_lt_two

Premises used: Fin.val, Nat.mod_lt, Nat.zero_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
⊢ (↑v : ℕ) % 2 < (↑2 : ℕ)

Tactic:
exact v.val.mod_lt Nat.zero_lt_two

Premises used: Fin.val, Nat.mod_lt, Nat.zero_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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

Tactic:
(Fin.ne_of_lt (Fin.mk_lt_of_lt_val ?_))

Premises used: Fin.ne_of_lt, Fin.mk_lt_of_lt_val
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
pos : (↑u : ℕ) % 2 < (↑2 : ℕ)
⊢ (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3) ≠ 2

Tactic:
refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val ?_))

Premises used: Fin.ne_of_lt, Fin.mk_lt_of_lt_val
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 < (↑2 : ℕ)

Tactic:
u.val.mod_lt Nat.zero_lt_two

Premises used: Fin.val, Nat.mod_lt, Nat.zero_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 < (↑2 : ℕ)

Tactic:
exact u.val.mod_lt Nat.zero_lt_two

Premises used: Fin.val, Nat.mod_lt, Nat.zero_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
neg : ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
⊢ (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3) ≠ ⟨(↑v : ℕ) % 2, ⋯⟩

Tactic:
simp only [ne_eq, Fin.ext_iff]

Premises used: Fin.ext_iff, ne_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
fin_omega fin_omega₁ :
  ∀ (h : LE.le (α := ℤ) (↑2 : ℤ) (↑(n + 2) : ℤ)), LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ)
⊢ (↑u : ℕ) + (↑1 : ℕ) < n + 2

Tactic:
fin_omega
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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

Tactic:
have hu' : u.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
fin_omega fin_omega₁ :
  ∀ (h : LE.le (α := ℤ) (↑2 : ℤ) (↑(n + 2) : ℤ)) (hu' : LT.lt (α := ℤ) (↑((↑u : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ)),
    LT.lt (α := ℤ) (↑((↑v : ℕ) + 1) : ℤ) (↑(n + 2) : ℤ)
⊢ (↑v : ℕ) + (↑1 : ℕ) < n + 2

Tactic:
fin_omega
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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

Tactic:
have hv' : v.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
neg : ¬(↑(v + 1) : ℕ) % 2 = (↑v : ℕ) % 2
⊢ ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2

Tactic:
rw [← add_eq_of_eq_sub' huv.symm]

Premises used: add_eq_of_eq_sub', Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
neg : ¬((↑v : ℕ) + 1) % 2 = (↑v : ℕ) % 2
⊢ ¬(↑(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]

Premises used: Fin.val_one, Fin.val_add_eq_of_add_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
simp : ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (Even x ↔ Even y)

Tactic:
simp [Nat.even_iff]

Premises used: Nat.even_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 ↔ (x % 2 = 0 ↔ y % 2 = 0)

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
neg : ¬((Even (↑v : ℕ) ↔ Even (α := ℕ) 1) ↔ Even (↑v : ℕ))
⊢ ¬((↑v : ℕ) + 1) % 2 = (↑v : ℕ) % 2

Tactic:
rw [show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,
            Nat.even_add]

Premises used: Nat.even_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
neg : ¬False
⊢ ¬((Even (↑v : ℕ) ↔ Even (α := ℕ) 1) ↔ Even (↑v : ℕ))

Tactic:
simp only [Nat.not_even_one, iff_false, not_iff_self, iff_not_self]

Premises used: iff_false, iff_not_self, Nat.not_even_one, not_iff_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
⊢ ¬False

Tactic:
id

Premises used: id, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
⊢ ¬False

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
neg : ¬(↑u : ℕ) % 2 = (↑(u + 1) : ℕ) % 2
⊢ ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2

Tactic:
rw [← add_eq_of_eq_sub' huv.symm]

Premises used: add_eq_of_eq_sub', Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
neg : ¬(↑u : ℕ) % 2 = ((↑u : ℕ) + 1) % 2
⊢ ¬(↑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]

Premises used: Fin.val_one, Fin.val_add_eq_of_add_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
simp : ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (Even x ↔ Even y)

Tactic:
simp [Nat.even_iff]

Premises used: Nat.even_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 ↔ (x % 2 = 0 ↔ y % 2 = 0)

Tactic:
lia