Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
⊢ ↑(if
          (if ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).castSucc <
            ⟨j, isLt✝¹⟩.succ then
        (if ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).castSucc
      else (if ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).succ) =
    ↑(if
          (if ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).castSucc <
            ⟨i, isLt✝²⟩.castSucc then
        (if ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).castSucc
      else (if ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩ then ⟨k, isLt✝⟩.castSucc else ⟨k, isLt✝⟩.succ).succ)

Tactic:
split_ifs

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.castSucc

case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.succ

case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.succ.castSucc

case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.succ.succ

case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.castSucc.castSucc

case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.castSucc.succ

case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.succ.castSucc

case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.succ.succ

case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.castSucc.castSucc

case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.castSucc.succ

case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.succ.castSucc

case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.succ.succ

case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.succ = ↑⟨k, isLt✝⟩.castSucc.castSucc

case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.succ = ↑⟨k, isLt✝⟩.castSucc.succ

case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.succ = ↑⟨k, isLt✝⟩.succ.castSucc

case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.succ = ↑⟨k, isLt✝⟩.succ.succ