-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
pos :
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
    (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
        (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc →
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
            (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)
neg :
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
    (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
        ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc →
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
            (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ)
pos₁ :
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
    (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
      ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
        (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨i, isLt⟩.castSucc →
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
            (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ)
neg₁ :
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
    (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
      ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
        ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨i, isLt⟩.castSucc →
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
            (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ)
pos₂ :
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
    ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
        (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc →
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ) =
            (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)
neg₂ :
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
    ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
        ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc →
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ) =
            (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ)
⊢ (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨j, isLt_1⟩ : Fin (n + 2)).succ then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ) =
    (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨i, isLt⟩ : Fin (n + 2)).castSucc then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ)
have pos₃ : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
  ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
    ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨i, isLt⟩.castSucc →
        (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ)
Tactic: split_ifs