-- 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)
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
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 →
          ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true) → ¬Even p.length
⊢ ¬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