-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
lemma factor_δ_spec {m n : ℕ} (f : ⦋m⦌ ⟶ ⦋n+1⦌) (j : Fin (n+2))
    (hj : ∀ (k : Fin (m+1)), f.toOrderHom k ≠ j) :
    factor_δ f j ≫ δ j = f

Proof state:
case a.h.h.succ.inl
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : (Hom.toOrderHom f) k < j.succ
⊢ j.succ.succAbove (j.predAbove ((Hom.toOrderHom f) k)) = (Hom.toOrderHom f) k

Tactic:
rw [predAbove_of_le_castSucc j _]

Result:
case a.h.h.succ.inl
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : (Hom.toOrderHom f) k < j.succ
⊢ j.succ.succAbove (((Hom.toOrderHom f) k).castPred ⋯) = (Hom.toOrderHom f) k

case a.h.h.succ.inl
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : (Hom.toOrderHom f) k < j.succ
⊢ (Hom.toOrderHom f) k ≤ j.castSucc

Proof state:
case a.h.h.succ.inl.h
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : (Hom.toOrderHom f) k < j.succ
⊢ (((Hom.toOrderHom f) k).castPred ⋯).castSucc < j.succ

Tactic:
rwa [castSucc_lt_succ_iff, castPred_le_iff, le_castSucc_iff]

Result:
no goals

Proof state:
case a.h.h.succ.inr
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : j.succ < (Hom.toOrderHom f) k
⊢ j.succ.succAbove (((Hom.toOrderHom f) k).pred ⋯) = (Hom.toOrderHom f) k

Tactic:
rw [succAbove_of_le_castSucc]

Result:
case a.h.h.succ.inr
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : j.succ < (Hom.toOrderHom f) k
⊢ (((Hom.toOrderHom f) k).pred ⋯).succ = (Hom.toOrderHom f) k

case a.h.h.succ.inr.h
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : j.succ < (Hom.toOrderHom f) k
⊢ j.succ ≤ (((Hom.toOrderHom f) k).pred ⋯).castSucc

Proof state:
case a.h.h.succ
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj : (Hom.toOrderHom f) k ≠ j.succ
⊢ j.succ.succAbove ((predAbove 0 j.succ).predAbove ((Hom.toOrderHom f) k)) = (Hom.toOrderHom f) k

Tactic:
rw [predAbove_of_castSucc_lt 0 _ (castSucc_zero ▸ succ_pos _), pred_succ]

Result:
case a.h.h.succ
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj : (Hom.toOrderHom f) k ≠ j.succ
⊢ j.succ.succAbove (j.predAbove ((Hom.toOrderHom f) k)) = (Hom.toOrderHom f) k

Proof state:
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ j
⊢ factor_δ f j ≫ δ j = f

Tactic:
ext k : 3

Result:
case a.h.h
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ j
k : Fin (⦋m⦌.len + 1)
⊢ (Hom.toOrderHom (factor_δ f j ≫ δ j)) k = (Hom.toOrderHom f) k

Proof state:
case a.h.h.zero
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
hj : (Hom.toOrderHom f) k ≠ 0
⊢ succAbove 0 ((predAbove 0 0).predAbove ((Hom.toOrderHom f) k)) = (Hom.toOrderHom f) k

Tactic:
rw [predAbove_of_le_castSucc _ _ (zero_le _), castPred_zero, predAbove_of_castSucc_lt 0 _
(castSucc_zero ▸ pos_of_ne_zero hj),
zero_succAbove, succ_pred]

Result:
no goals

Proof state:
case a.h.h.succ.inr
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : j.succ < (Hom.toOrderHom f) k
⊢ j.succ.succAbove (((Hom.toOrderHom f) k).pred ⋯) = (Hom.toOrderHom f) k

case a.h.h.succ.inr.h
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : j.succ < (Hom.toOrderHom f) k
⊢ j.castSucc < (Hom.toOrderHom f) k

Tactic:
swap

Result:
case a.h.h.succ.inr.h
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : j.succ < (Hom.toOrderHom f) k
⊢ j.castSucc < (Hom.toOrderHom f) k

case a.h.h.succ.inr
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
j : Fin (n + 1)
hj✝ : (Hom.toOrderHom f) k ≠ j.succ
hj : j.succ < (Hom.toOrderHom f) k
⊢ j.succ.succAbove (((Hom.toOrderHom f) k).pred ⋯) = (Hom.toOrderHom f) k