-- 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.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

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.succ ≤ (((Hom.toOrderHom f) k).pred ⋯).castSucc

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

Proof state:
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:
exact (castSucc_lt_succ _).trans hj

Result:
no goals

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 (((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

Tactic:
swap

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
⊢ (Hom.toOrderHom f) k ≤ j.castSucc

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

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 (j.predAbove ((Hom.toOrderHom f) k)) = (Hom.toOrderHom f) k

Tactic:
rcases hj.lt_or_lt with (hj | hj)

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 (j.predAbove ((Hom.toOrderHom f) k)) = (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 (j.predAbove ((Hom.toOrderHom f) k)) = (Hom.toOrderHom f) k

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 (((Hom.toOrderHom f) k).castPred ⋯) = (Hom.toOrderHom f) k

Tactic:
rw [succAbove_of_castSucc_lt]

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
⊢ (((Hom.toOrderHom f) k).castPred ⋯).castSucc = (Hom.toOrderHom f) k

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

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
⊢ (((Hom.toOrderHom f) k).pred ⋯).succ = (Hom.toOrderHom f) k

Tactic:
rw [succ_pred]

Result:
no goals

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
⊢ (((Hom.toOrderHom f) k).castPred ⋯).castSucc = (Hom.toOrderHom f) k

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:
swap

Result:
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

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).castPred ⋯).castSucc = (Hom.toOrderHom f) k

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
⊢ (((Hom.toOrderHom f) k).castPred ⋯).castSucc = (Hom.toOrderHom f) k

Tactic:
rw [castSucc_castPred]

Result:
no goals

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

Tactic:
dsimp [factor_δ, δ, σ]

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

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 (j.predAbove ((Hom.toOrderHom f) k)) = (Hom.toOrderHom f) k

Tactic:
rw [predAbove_of_castSucc_lt]

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
⊢ 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

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
⊢ (Hom.toOrderHom f) k ≤ j.castSucc

Tactic:
exact (le_castSucc_iff.mpr hj)

Result:
no goals

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

Tactic:
specialize hj k

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

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

Tactic:
rwa [succ_le_castSucc_iff, lt_pred_iff]

Result:
no goals