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

Proof state:
case a.h.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hik)]

Result:
case a.h.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)

Proof state:
case a.h.h.inl.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
rwa [Fin.predAbove_of_le_castSucc _ _ hjk, Fin.castSucc_castPred]

Result:
no goals

Proof state:
case a.h.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hik),
Fin.succ_predAbove_succ, Fin.succAbove_of_le_castSucc]

Result:
case a.h.h.inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc

Proof state:
case a.h.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
rcases le_or_lt i k with (hik | hik)

Result:
case a.h.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

case a.h.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

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

Tactic:
ext k : 3

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

Proof state:
case a.h.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
have hjk := H.trans_lt' hik

Result:
case a.h.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)

Proof state:
case a.h.h.inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ (k.castPred ⋯).castSucc < i

Tactic:
rwa [Fin.castSucc_castPred]

Result:
no goals

Proof state:
case a.h.h.inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
rcases le_or_lt k (j.castSucc) with (hjk | hjk)

Result:
case a.h.h.inl.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc

case a.h.h.inl.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i ≤ (j.predAbove k).castSucc

Proof state:
case a.h.h.inl.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
rw [Fin.le_castSucc_iff, Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succ_pred]

Result:
case a.h.h.inl.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i < k

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

Tactic:
dsimp [σ, δ]

Result:
case a.h.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

Proof state:
case a.h.h.inl.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i < k

Tactic:
exact H.trans_lt hjk

Result:
no goals

Proof state:
case a.h.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
rw [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr
  (hjk.trans (Fin.castSucc_lt_succ _)).le),
  Fin.predAbove_of_le_castSucc _ _ hjk.le, Fin.castPred_castSucc, Fin.succAbove_of_castSucc_lt,
  Fin.castSucc_castPred]

Result:
case a.h.h.inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ (k.castPred ⋯).castSucc < i