-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
    δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Proof state:
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ i ≫ δ j.succ)) k) = ↑((Hom.toOrderHom (δ j ≫ δ i.castSucc)) k)

Tactic:
dsimp [δ, Fin.succAbove]

Result:
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ ↑(if (if k.castSucc < i then k.castSucc else k.succ).castSucc < j.succ then
        (if k.castSucc < i then k.castSucc else k.succ).castSucc
      else (if k.castSucc < i then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < i.castSucc then
        (if k.castSucc < j then k.castSucc else k.succ).castSucc
      else (if k.castSucc < j then k.castSucc else k.succ).succ)

Proof state:
case a.h.h.h.mk.mk
n : ℕ
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝¹ : i < n + 2
j : ℕ
isLt✝ : j < n + 2
H : ⟨i, isLt✝¹⟩ ≤ ⟨j, isLt✝⟩
⊢ ↑(if (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).castSucc < ⟨j, isLt✝⟩.succ then
        (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).castSucc < ⟨i, isLt✝¹⟩.castSucc then
        (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).succ)

Tactic:
rcases k with ⟨k, _⟩

Result:
case a.h.h.h.mk.mk.mk
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)

Proof state:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Tactic:
ext k

Result:
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ i ≫ δ j.succ)) k) = ↑((Hom.toOrderHom (δ j ≫ δ i.castSucc)) k)

Proof state:
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ ↑(if (if k.castSucc < i then k.castSucc else k.succ).castSucc < j.succ then
        (if k.castSucc < i then k.castSucc else k.succ).castSucc
      else (if k.castSucc < i then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < i.castSucc then
        (if k.castSucc < j then k.castSucc else k.succ).castSucc
      else (if k.castSucc < j then k.castSucc else k.succ).succ)

Tactic:
rcases i with ⟨i, _⟩

Result:
case a.h.h.h.mk
n : ℕ
j : Fin (n + 2)
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝ : i < n + 2
H : ⟨i, isLt✝⟩ ≤ j
⊢ ↑(if (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).castSucc < j.succ then
        (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < ⟨i, isLt✝⟩.castSucc then
        (if k.castSucc < j then k.castSucc else k.succ).castSucc
      else (if k.castSucc < j then k.castSucc else k.succ).succ)

Proof state:
case a.h.h.h.mk
n : ℕ
j : Fin (n + 2)
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝ : i < n + 2
H : ⟨i, isLt✝⟩ ≤ j
⊢ ↑(if (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).castSucc < j.succ then
        (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < ⟨i, isLt✝⟩.castSucc then
        (if k.castSucc < j then k.castSucc else k.succ).castSucc
      else (if k.castSucc < j then k.castSucc else k.succ).succ)

Tactic:
rcases j with ⟨j, _⟩

Result:
case a.h.h.h.mk.mk
n : ℕ
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝¹ : i < n + 2
j : ℕ
isLt✝ : j < n + 2
H : ⟨i, isLt✝¹⟩ ≤ ⟨j, isLt✝⟩
⊢ ↑(if (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).castSucc < ⟨j, isLt✝⟩.succ then
        (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨i, isLt✝¹⟩ then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).castSucc < ⟨i, isLt✝¹⟩.castSucc then
        (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨j, isLt✝⟩ then k.castSucc else k.succ).succ)

Proof state:
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

Tactic:
simp at * <;> omega

Result:
no goals