awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
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)
this : ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true
cons :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₁ :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₂ :
  ¬Even p.length →
    ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
⊢ ¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
have cons₃ : ¬Even p.length →
  ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
    ¬¬(c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
Tactic: tauto
Cleared hypotheses: ih, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
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)
this : ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true
cons :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₁ :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₂ :
  ¬Even p.length →
    ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₃ :
  ¬Even p.length →
    ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₄ :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₅ :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₆ :
  ¬Even p.length →
    ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₇ :
  ¬Even p.length →
    ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
⊢ ¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
have cons₈ : Even p.length →
  ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true → ¬Even p.length → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
Tactic: tauto
Cleared hypotheses: ih, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
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)
this : ¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true
cons :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₁ :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₂ :
  ¬Even p.length →
    ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₃ :
  ¬Even p.length →
    ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₄ :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₅ :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₆ :
  ¬Even p.length →
    ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₇ :
  ¬Even p.length →
    ¬((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬¬(c : (a : α) → Bool) u = true →
        ¬(c : (a : α) → Bool) v = true →
          (¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true))
cons₈ :
  Even p.length →
    ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
      ¬(c : (a : α) → Bool) u = true →
        (c : (a : α) → Bool) v = true → ¬Even p.length → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
⊢ ¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
have cons₉ : Even p.length →
  ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true) →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true) → ¬Even p.length
Tactic: tauto
Cleared hypotheses: ih, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have nil : ∀ {u : α},
  Even (Walk.length.{u_1} (V := α) (G := G) (u := u) Walk.nil) ↔
    ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) u = 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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
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)
⊢ Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have 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)
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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ Odd p.length ↔ (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have rw : ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
Tactic: rw [← Nat.not_even_iff_odd, c.even_length_iff_congr p]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mp : ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
mp :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mpr : (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
mp :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mpr :
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mp₁ : ¬(c : (a : α) → Bool) u = true →
  (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
mp :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mpr :
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₁ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mp₂ : ¬¬(c : (a : α) → Bool) u = true →
  ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
mp :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mpr :
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₁ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₂ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₃ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₄ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mp₅ : ¬(c : (a : α) → Bool) u = true →
  (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
mp :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mpr :
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₁ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₂ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₃ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₄ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₅ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mp₆ : ¬(c : (a : α) → Bool) u = true →
  (c : (a : α) → Bool) v = true → (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
mp :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mpr :
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₁ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₂ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₃ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₄ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₅ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
mp₆ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mp₇ : ¬¬(c : (a : α) → Bool) u = true →
  ¬(c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
mp :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mpr :
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₁ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₂ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₃ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₄ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₅ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
mp₆ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true
mp₇ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mp₈ : ¬¬(c : (a : α) → Bool) u = true →
  ¬(c : (a : α) → Bool) v = true → (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
mp :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mpr :
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₁ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₂ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₃ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₄ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₅ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
mp₆ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true
mp₇ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
mp₈ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mpr₁ : ¬(c : (a : α) → Bool) u = true →
  (c : (a : α) → Bool) v = true → ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (goal)
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
mp :
  ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mpr :
  (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) →
    ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₁ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₂ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₃ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₄ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
mp₅ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
mp₆ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true
mp₇ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
mp₈ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true
mpr₁ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
⊢ ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) ↔
    (¬(c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
have mpr₂ : ¬¬(c : (a : α) → Bool) u = true →
  ¬(c : (a : α) → Bool) v = true → ¬((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
⊢ False
have h' : G.chromaticNumber ≤ 2
Tactic: have h' : G.chromaticNumber ≤ 2 := Order.le_of_lt_add_one <| not_le.mp h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
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
⊢ False
have this : ¬(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
-- 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 : Adj (cycleGraph (n + 2)) u v
⊢ Ne (α := Bool) ((fun (u : Fin (n + 2)) ↦ decide ((↑u : ℕ) % 2 = 0)) u)
    ((fun (u : Fin (n + 2)) ↦ decide ((↑u : ℕ) % 2 = 0)) v)
have simp : ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
Tactic: simp only [ne_eq, decide_eq_decide]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
n_1 n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
hadj : Adj (cycleGraph (n + 2)) u v
⊢ ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
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 : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬((↑u : ℕ) % 2 = 0 ↔ (↑v : ℕ) % 2 = 0)
have inl : ¬(Odd v ↔ Even v)
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]