awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ¬(Even (↑u : ℕ) ↔ (Even (↑u : ℕ) ↔ Even (α := ℕ) 1))
⊢ ¬(↑u : ℕ) % 2 = ((↑u : ℕ) + 1) % 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 : v - u = 1
neg : ¬False
⊢ ¬(Even (↑u : ℕ) ↔ (Even (↑u : ℕ) ↔ Even (α := ℕ) 1))

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 : v - u = 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 : v - u = 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)
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
neg₁ : ∀ (huv : v - u = 1), ¬(↑u : ℕ) % 2 = (↑v : ℕ) % 2
⊢ ¬(↑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

Premises used: iff_false, iff_not_self, id, Fin.val_one, Nat.even_add, Nat.not_even_one, not_iff_self, 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)
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

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

Premises used: iff_false, iff_not_self, id, Fin.val_one, Nat.even_add, Nat.not_even_one, not_iff_self, Fin.val_add_eq_of_add_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
u v : Fin n
hadj : (cycleGraph n).Adj u v
⊢ Ne (α := Fin 3) ((fun (u : Fin n) ↦ if (↑u : ℕ) = n - 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) u)
    ((fun (u : Fin n) ↦ if (↑u : ℕ) = n - 1 then 2 else (⟨(↑u : ℕ) % 2, ⋯⟩ : Fin 3)) v)

Tactic:
match n with
    | 0 => exact u.elim0
    | 1 => simp at h
    | n + 2 =>
      simp only
      simp only [cycleGraph_adj] at hadj
      split_ifs with hu hv
      · simp [Fin.eq_mk_iff_val_eq.mpr hu, Fin.eq_mk_iff_val_eq.mpr hv] at hadj
      · refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val (?_))).symm
        exact v.val.mod_lt Nat.zero_lt_two
      · refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val ?_))
        exact u.val.mod_lt Nat.zero_lt_two
      · simp only [ne_eq, Fin.ext_iff]
        have hu' : u.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
        have hv' : v.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
        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
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
⊢ (cycleGraph n).Colorable (Fintype.card (Fin 3))

Tactic:
have hc := (cycleGraph.tricoloring n h).colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
a : (cycleGraph n).chromaticNumber ≤ 3
a₁ : 3 ≤ (cycleGraph n).chromaticNumber
⊢ (cycleGraph n).chromaticNumber = 3

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ (cycleGraph n).chromaticNumber ≤ 3

Tactic:
apply hc.chromaticNumber_le

Premises used: SimpleGraph.Colorable.chromaticNumber_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ n - 3 + 3 = n

Tactic:
Nat.sub_add_cancel (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne h ?_))

Premises used: Nat.succ_le_of_lt, Nat.sub_add_cancel, Nat.lt_of_le_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
refine : ¬2 = n
⊢ n - 3 + 3 = n

Tactic:
refine Nat.sub_add_cancel (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne h ?_))

Premises used: Nat.succ_le_of_lt, Nat.sub_add_cancel, Nat.lt_of_le_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
h2 : 2 = n
⊢ Odd (α := ℕ) 2

Tactic:
rw [← h2] at hOdd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
h2 : 2 = n
hOdd₁ : Odd (α := ℕ) 2
⊢ (cycleGraph n).Colorable (Fintype.card (Fin 3))

Tactic:
rw [← h2] at hOdd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
h2 : 2 = n
hOdd₁ : Odd (α := ℕ) 2
hc₁ : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ 2 = n

Tactic:
rw [← h2] at hOdd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd (α := ℕ) 2
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
h2 : 2 = n
⊢ False

Tactic:
(Nat.not_odd_iff.mpr rfl) hOdd

Premises used: Iff.mpr, Nat.not_odd_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd (α := ℕ) 2
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
h2 : 2 = n
⊢ False

Tactic:
exact (Nat.not_odd_iff.mpr rfl) hOdd

Premises used: Iff.mpr, Nat.not_odd_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ 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
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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)
rw : Odd n
⊢ Odd w.length

Tactic:
rw [cycleGraph.length_cycle, hn3]

Premises used: SimpleGraph.cycleGraph.length_cycle
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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)
⊢ Odd n

Tactic:
hOdd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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)
⊢ Odd n

Tactic:
exact hOdd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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)
⊢ Odd w.length

Tactic:
have hOdd' : Odd w.length := by
      rw [cycleGraph.length_cycle, hn3]
      exact hOdd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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
a : 3 ≤ chromaticNumber (V := Fin (n - 3 + 3)) (cycleGraph (n - 3 + 3))
⊢ 3 ≤ (cycleGraph n).chromaticNumber

Tactic:
rw [← hn3]
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 ≤ chromaticNumber (V := Fin (n - 3 + 3)) (cycleGraph (n - 3 + 3))

Tactic:
Walk.three_le_chromaticNumber_of_odd_loop w hOdd'

Premises used: SimpleGraph.Walk.three_le_chromaticNumber_of_odd_loop
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 ≤ chromaticNumber (V := Fin (n - 3 + 3)) (cycleGraph (n - 3 + 3))

Tactic:
exact Walk.three_le_chromaticNumber_of_odd_loop w hOdd'

Premises used: SimpleGraph.Walk.three_le_chromaticNumber_of_odd_loop
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
r t : ℕ
⊢ (completeEquipartiteGraph r t).Colorable r

Tactic:
⟨Coloring.completeEquipartiteGraph⟩

Premises used: Nonempty.intro, SimpleGraph.Coloring.completeEquipartiteGraph, SimpleGraph.Colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
simp_rw : G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), Even w.length

Tactic:
simp_rw [← Nat.not_odd_iff_even]

Premises used: Nat.not_odd_iff_even
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
mp : G.Colorable 2 → ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
mpr : (∀ (u : α) (w : G.Walk u u), ¬Odd w.length) → G.Colorable 2
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u : α
w : G.Walk u u
ho : Odd w.length
⊢ LE.le (α := ℕ∞) 3 (↑2 : ℕ∞)

Tactic:
have := (w.three_le_chromaticNumber_of_odd_loop ho).trans h.chromaticNumber_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u : α
w : G.Walk u u
ho : Odd w.length
this : LE.le (α := ℕ∞) 3 (↑2 : ℕ∞)
⊢ False

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
mpr : ∀ (c : G.ConnectedComponent), c.toSimpleGraph.Colorable 2
⊢ G.Colorable 2

Tactic:
apply colorable_iff_forall_connectedComponents.2

Premises used: SimpleGraph.colorable_iff_forall_connectedComponents, Iff.mpr
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
mpr : ∀ (w : α) (hv : w ∈ c.supp), c.toSimpleGraph.Colorable 2
⊢ c.toSimpleGraph.Colorable 2

Tactic:
obtain ⟨_, hv⟩ := c.nonempty_supp

Premises used: SimpleGraph.ConnectedComponent.nonempty_supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w : α
hv : w ∈ c.supp
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 ⋯)))
        (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
⊢ c.toSimpleGraph.Colorable 2

Tactic:
use fun a ↦ Fin.ofNat 2 (c.connected_toSimpleGraph ⟨_, hv⟩ a).some.length

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Walk.length, Fin.ofNat, Nonempty.some, Subtype.mk, SimpleGraph.ConnectedComponent.connected_toSimpleGraph, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 ⋯)))
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 ⋯) hab) (reverse (Nonempty.some ⋯)))))
⊢ False

Tactic:
apply h _ <| (((c.connected_toSimpleGraph ⟨_, hv⟩ a).some.concat hab).append
                 (c.connected_toSimpleGraph ⟨_, hv⟩ b).some.reverse).map c.toSimpleGraph_hom

Premises used: SimpleGraph.Walk.map, SimpleGraph.Connected.preconnected, SimpleGraph.ConnectedComponent.toSimpleGraph_hom, Nonempty.some, SimpleGraph.Walk.concat, Subtype.mk, SimpleGraph.ConnectedComponent.connected_toSimpleGraph, SimpleGraph.Walk.reverse, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 ⋯)))
map_rel' :
  Odd
    (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 ⋯) +
      1)
⊢ 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 ⋯)))))

Tactic:
rw [length_map, length_append, length_concat, length_reverse, add_right_comm]

Premises used: add_right_comm, SimpleGraph.Walk.length_map, SimpleGraph.Walk.length_concat, SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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) : ℕ)
simp_rw₁ :
  (↑(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

Tactic:
simp_rw [← Fin.val_natCast, ← Fin.ofNat_eq_cast, he]

Premises used: Fin.val_natCast, Fin.ofNat_eq_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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

Tactic:
have : ((Nonempty.some (c.connected_toSimpleGraph ⟨_, hv⟩ a)).length) % 2 =
        (Nonempty.some (c.connected_toSimpleGraph ⟨_, hv⟩ b)).length % 2 := by
      simp_rw [← Fin.val_natCast, ← Fin.ofNat_eq_cast, he]
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 ⋯)))
this :
  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
⊢ (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 =
    0

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
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 ⋯)))
this :
  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
⊢ Odd
    (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 ⋯) +
      1)

Tactic:
exact (Nat.even_iff.mpr (by lia)).add_one

Premises used: Iff.mpr, Even.add_one, Nat.even_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
inst : Finite.{u_1 + 1} (↑G.edgeSet : Type u_1)
inst_1 : Finite K
⊢ Finite (G.EdgeLabeling K)

Tactic:
Pi.finite

Premises used: Pi.finite, SimpleGraph.EdgeLabeling
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
inst : Nonempty K
⊢ Nonempty (G.EdgeLabeling K)

Tactic:
Pi.instNonempty

Premises used: SimpleGraph.EdgeLabeling, Pi.instNonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
inst : Subsingleton K
⊢ Subsingleton (G.EdgeLabeling K)

Tactic:
Pi.instSubsingleton

Premises used: Pi.instSubsingleton, SimpleGraph.EdgeLabeling
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
inst : Nonempty.{u_1 + 1} (↑G.edgeSet : Type u_1)
inst_1 : Nontrivial K
⊢ Nontrivial (G.EdgeLabeling K)

Tactic:
Function.nontrivial

Premises used: Function.nontrivial, SimpleGraph.EdgeLabeling
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
K : Type u_3
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : Fintype K
rw : Fintype.card K ^ Finset.card.{u_1} (α := Sym2 V) (edgeFinset ⊤) = Fintype.card K ^ (Fintype.card V).choose 2
rw₁ rw₂ : Fintype.card K ^ (Fintype.card V).choose 2 = Fintype.card K ^ (Fintype.card V).choose 2
⊢ Fintype.card K ^ Fintype.card.{u_1} (↑(edgeSet ⊤) : Type u_1) = Fintype.card K ^ (Fintype.card V).choose 2

Tactic:
rw [← edgeFinset_card, card_edgeFinset_top_eq_card_choose_two]

Premises used: SimpleGraph.card_edgeFinset_top_eq_card_choose_two, SimpleGraph.edgeFinset_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x y : V
h : G.Adj x y
⊢ C.get x y h = C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) h)

Tactic:
rfl

Premises used: rfl, SimpleGraph.EdgeLabeling.get
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x y : V
h : G.Adj y x
⊢ C.get y x h = C.get x y ⋯

Tactic:
simp [EdgeLabeling.get, Sym2.eq_swap]

Premises used: Sym2.eq_swap, SimpleGraph.EdgeLabeling.get
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
h₁ :
  ∀ (e : Sym2 V) (he : e ∈ G.edgeSet),
    C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e he) =
      C' (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e he)
⊢ C = C'

Tactic:
funext ⟨e, he⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
e : Sym2 V
he : e ∈ G.edgeSet
h₁ :
  ∀ (x y : V) (he : s(x, y) ∈ G.edgeSet),
    C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) he) =
      C' (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) he)
⊢ C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e he) =
    C' (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e he)

Tactic:
induction e using Sym2.inductionOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
x y : V
he : s(x, y) ∈ G.edgeSet
⊢ C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) he) =
    C' (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) he)

Tactic:
h _ _ he

Premises used: SimpleGraph.EdgeLabeling.get
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
x y : V
he : s(x, y) ∈ G.edgeSet
⊢ C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) he) =
    C' (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) he)

Tactic:
exact h _ _ he
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
C : G.EdgeLabeling K
f : G' →g G
e : (↑G'.edgeSet : Type u_2)
⊢ C.pullback f e = C (f.mapEdgeSet e)

Tactic:
rfl

Premises used: SimpleGraph.EdgeLabeling.pullback, rfl