-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem δ_comp_σ_self {n} {i : Fin (n + 1)} :
    δ (Fin.castSucc i) ≫ σ i = 𝟙 ⦋n⦌

Proof state:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩)) ⟨j, hj⟩) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) ⟨j, hj⟩)

Tactic:
simp? at hj says simp only [len_mk] at hj

Result:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩)) ⟨j, hj⟩) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) ⟨j, hj⟩)

Proof state:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩)) ⟨j, hj⟩) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) ⟨j, hj⟩)

Tactic:
simp only [len_mk] at hj

Result:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩)) ⟨j, hj⟩) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) ⟨j, hj⟩)

Proof state:
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ False

Tactic:
all_goals omega

Result:
no goals

Proof state:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else ↑((if j < i then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯)) =
    j

Tactic:
split_ifs

Result:
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : ¬i < j
⊢ ↑(⟨j, ⋯⟩.castPred ⋯) = j

case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : i < j + 1
⊢ j + 1 - 1 = j

case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j

Proof state:
case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case mk
n i : ℕ
hi : i < n + 1
⊢ δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩ = 𝟙 ⦋n⦌

Tactic:
ext ⟨j, hj⟩

Result:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩)) ⟨j, hj⟩) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) ⟨j, hj⟩)

Proof state:
case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j

Tactic:
simp

Result:
case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ False

Proof state:
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : ¬i < j
⊢ ↑(⟨j, ⋯⟩.castPred ⋯) = j

case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : i < j + 1
⊢ j + 1 - 1 = j

case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j

Tactic:
any_goals simp

Result:
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ False

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌

Tactic:
rcases i with ⟨i, hi⟩

Result:
case mk
n i : ℕ
hi : i < n + 1
⊢ δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩ = 𝟙 ⦋n⦌

Proof state:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ ↑(if h : ⟨i, ⋯⟩ < if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩ then
        (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).pred ⋯
      else (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯) =
    j

Tactic:
simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred, Fin.coe_castLT]

Result:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else ↑((if j < i then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯)) =
    j

Proof state:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩)) ⟨j, hj⟩) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) ⟨j, hj⟩)

Tactic:
dsimp [σ, δ, Fin.predAbove, Fin.succAbove]

Result:
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ ↑(if h : ⟨i, ⋯⟩ < if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩ then
        (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).pred ⋯
      else (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯) =
    j