-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
pos : (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ)
neg :
  (↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) - 1 → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
pos₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₁ :
  (↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) - 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
neg₂ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
pos₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
neg₃ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      (↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1
pos₄ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ)
neg₄ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → (↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1
pos₅ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1
neg₅ :
  (↑j : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑i : ℕ) - 1 →
      ¬(↑k : ℕ) + 1 < (↑j : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1 + 1
pos₆ : ¬(↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑j : ℕ) + 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) = (↑k : ℕ)
pos₇ :
  ¬(↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) →
      (↑k : ℕ) < (↑j : ℕ) + 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1
neg₆ :
  ¬(↑j : ℕ) < (↑i : ℕ) →
    (↑k : ℕ) < (↑i : ℕ) →
      (↑k : ℕ) < (↑j : ℕ) + 1 → ¬(↑k : ℕ) < (↑j : ℕ) → ¬(↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) = (↑k : ℕ) + 1 + 1
pos₈ :
  ¬(↑j : ℕ) < (↑i : ℕ) → (↑k : ℕ) < (↑i : ℕ) → ¬(↑k : ℕ) < (↑j : ℕ) + 1 → (↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ)
⊢ (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
have pos₉ : ¬(↑j : ℕ) < (↑i : ℕ) →
  (↑k : ℕ) < (↑i : ℕ) →
    ¬(↑k : ℕ) < (↑j : ℕ) + 1 → ¬(↑k : ℕ) < (↑j : ℕ) → (↑k : ℕ) + 1 < (↑i : ℕ) → (↑k : ℕ) + 1 = (↑k : ℕ) + 1
Tactic: split_ifs