-- 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)
mpr₂ :
  ¬¬(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)
mpr₄ :
  ¬¬(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) → False
mpr₆ :
  ¬¬(c : (a : α) → Bool) u = true →
    ¬(c : (a : α) → Bool) v = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) v = true) → False
mp₉ mp₁₀ mp₁₁ :
  ¬(c : (a : α) → Bool) u = true →
    (c : (a : α) → Bool) v = true → ¬(c : (a : α) → Bool) u = true → (c : (a : α) → Bool) v = true
mp₁₂ 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) v = true → (c : (a : α) → Bool) u = true → False
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