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

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

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

Result:
case a.h.h.cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

case a.h.h.cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Proof state:
case inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : k ≤ j
⊢ i ≤ j.predAbove k.castSucc

Tactic:
rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
Fin.castPred_castSucc]

Result:
no goals

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

Tactic:
ext k : 3

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

Proof state:
case a.h.h.cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove k.succ = i.predAbove (j.predAbove k.castSucc).succ

Tactic:
rw [Fin.predAbove_of_le_castSucc _ k.castSucc
(Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
(Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
(Fin.succ_le_castSucc_iff.mpr h)]

Result:
no goals

Proof state:
case a.h.h.cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
(Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
Fin.succ_predAbove_succ]

Result:
case a.h.h.cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove k.succ = i.predAbove (j.predAbove k.castSucc).succ

Proof state:
case a.h.h.cast.zero
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ j.predAbove (i.castSucc.predAbove (Fin.castSucc 0)) = i.predAbove (j.succ.predAbove (Fin.castSucc 0))

Tactic:
rw [Fin.castSucc_zero, Fin.predAbove_of_le_castSucc _ 0 (Fin.zero_le _),
Fin.predAbove_of_le_castSucc _ _ (Fin.zero_le _), Fin.castPred_zero,
Fin.predAbove_of_le_castSucc _ 0 (Fin.zero_le _),
Fin.predAbove_of_le_castSucc _ _ (Fin.zero_le _)]

Result:
no goals

Proof state:
case a.h.h.cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _ (Fin.castSucc_lt_castSucc_iff.mpr
(Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
Fin.succ_predAbove_succ]

Result:
case a.h.h.cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove k.castSucc = i.predAbove (j.predAbove k.castSucc).succ

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

Tactic:
simp only [len_mk, Fin.predAbove_right_last]

Result:
no goals

Proof state:
case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i ≤ j.predAbove k.castSucc

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
Fin.le_pred_iff,
Fin.succ_le_castSucc_iff]

Result:
case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i < k

Proof state:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ i ≤ j.predAbove k.castSucc

Tactic:
rcases le_or_lt k j with (hkj | hkj)

Result:
case inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : k ≤ j
⊢ i ≤ j.predAbove k.castSucc

case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i ≤ j.predAbove k.castSucc

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

Tactic:
dsimp [σ]

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

Proof state:
case a.h.h.cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove k.castSucc = i.predAbove (j.predAbove k.castSucc).succ

Tactic:
rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]

Result:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ i ≤ j.predAbove k.castSucc

Proof state:
case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i < k

Tactic:
exact H.trans_lt hkj

Result:
no goals