-- 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
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
cons₁₆ :
  Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬Even p.length →
          (c : (a : α) → Bool) v = true →
            (c : (a : α) → Bool) w = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
cons₁₇ :
  Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬Even p.length →
          ¬(c : (a : α) → Bool) v = true →
            ¬(c : (a : α) → Bool) w = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
cons₁₈ :
  Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        (c : (a : α) → Bool) v = true →
          (c : (a : α) → Bool) w = true → (c : (a : α) → Bool) u = true → (c : (a : α) → Bool) w = true → ¬Even p.length
cons₁₉ :
  Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        (c : (a : α) → Bool) v = true →
          (c : (a : α) → Bool) w = true →
            ¬(c : (a : α) → Bool) u = true → ¬(c : (a : α) → Bool) w = true → ¬Even p.length
cons₂₀ :
  Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬(c : (a : α) → Bool) v = true →
          ¬(c : (a : α) → Bool) w = true →
            (c : (a : α) → Bool) u = true → (c : (a : α) → Bool) w = true → ¬Even p.length
cons₂₁ :
  Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬(c : (a : α) → Bool) v = true →
          ¬(c : (a : α) → Bool) w = true →
            ¬(c : (a : α) → Bool) u = true → ¬(c : (a : α) → Bool) w = true → ¬Even p.length
cons₂₂ :
  Even p.length →
    (c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        ¬Even p.length →
          (c : (a : α) → Bool) v = true →
            (c : (a : α) → Bool) w = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
cons₂₃ :
  Even p.length →
    (c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        ¬Even p.length →
          ¬(c : (a : α) → Bool) v = true →
            ¬(c : (a : α) → Bool) w = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
cons₂₄ :
  Even p.length →
    (c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        (c : (a : α) → Bool) v = true →
          (c : (a : α) → Bool) w = true → (c : (a : α) → Bool) u = true → (c : (a : α) → Bool) w = true → ¬Even p.length
cons₂₅ :
  Even p.length →
    (c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        (c : (a : α) → Bool) v = true →
          (c : (a : α) → Bool) w = true →
            ¬(c : (a : α) → Bool) u = true → ¬(c : (a : α) → Bool) w = true → ¬Even p.length
cons₂₆ :
  Even p.length →
    (c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        ¬(c : (a : α) → Bool) v = true →
          ¬(c : (a : α) → Bool) w = true →
            (c : (a : α) → Bool) u = true → (c : (a : α) → Bool) w = true → ¬Even p.length
cons₂₇ :
  Even p.length →
    (c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        ¬(c : (a : α) → Bool) v = true →
          ¬(c : (a : α) → Bool) w = true →
            ¬(c : (a : α) → Bool) u = true → ¬(c : (a : α) → Bool) w = true → ¬Even p.length
cons₂₈ :
  ¬Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬Even p.length →
          ¬(c : (a : α) → Bool) v = true →
            (c : (a : α) → Bool) w = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
cons₂₉ cons₃₀ :
  ¬Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬Even p.length →
          ¬¬(c : (a : α) → Bool) v = true →
            ¬(c : (a : α) → Bool) w = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
cons₃₁ :
  ¬Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬Even p.length →
          ¬¬(c : (a : α) → Bool) v = true →
            ¬(c : (a : α) → Bool) w = true → (c : (a : α) → Bool) u = true → (c : (a : α) → Bool) w = true
cons₃₂ :
  ¬Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬Even p.length →
          ¬¬(c : (a : α) → Bool) v = true →
            ¬(c : (a : α) → Bool) w = true → (c : (a : α) → Bool) w = true → (c : (a : α) → Bool) u = true
cons₃₃ :
  ¬Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬(c : (a : α) → Bool) v = true →
          (c : (a : α) → Bool) w = true → (c : (a : α) → Bool) u = true → (c : (a : α) → Bool) w = true → ¬Even p.length
cons₃₄ :
  ¬Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬(c : (a : α) → Bool) v = true →
          (c : (a : α) → Bool) w = true →
            ¬(c : (a : α) → Bool) u = true → ¬(c : (a : α) → Bool) w = true → ¬Even p.length
cons₃₅ :
  ¬Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬¬(c : (a : α) → Bool) v = true →
          ¬(c : (a : α) → Bool) w = true →
            (c : (a : α) → Bool) u = true → (c : (a : α) → Bool) w = true → ¬Even p.length
cons₃₆ cons₃₇ :
  ¬Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬¬(c : (a : α) → Bool) v = true →
          ¬(c : (a : α) → Bool) w = true →
            ¬(c : (a : α) → Bool) u = true → ¬(c : (a : α) → Bool) w = true → ¬Even p.length
cons₃₈ :
  ¬Even p.length →
    ¬(c : (a : α) → Bool) u = true →
      (c : (a : α) → Bool) v = true →
        ¬¬(c : (a : α) → Bool) v = true →
          ¬(c : (a : α) → Bool) w = true →
            ¬(c : (a : α) → Bool) u = true → ¬(c : (a : α) → Bool) w = true → Even p.length → False
cons₃₉ :
  ¬Even p.length →
    (c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        ¬Even p.length →
          ¬(c : (a : α) → Bool) v = true →
            (c : (a : α) → Bool) w = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
cons₄₀ :
  ¬Even p.length →
    (c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        ¬Even p.length →
          ¬¬(c : (a : α) → Bool) v = true →
            ¬(c : (a : α) → Bool) w = true → ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
cons₄₁ :
  ¬Even p.length →
    (c : (a : α) → Bool) u = true →
      ¬(c : (a : α) → Bool) v = true →
        ¬Even p.length →
          ¬(c : (a : α) → Bool) v = true →
            (c : (a : α) → Bool) w = true → ((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) u = true →
    ¬(c : (a : α) → Bool) v = true →
      ¬Even p.length →
        ¬(c : (a : α) → Bool) v = true →
          (c : (a : α) → Bool) w = true → (c : (a : α) → Bool) u = true → (c : (a : α) → Bool) w = true
Tactic: tauto
Cleared hypotheses: ih, this