-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (X.map
                        (Quiver.Hom.op
                          (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                              (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                            ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.castSucc.succ) :
                                (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                                  (SimplexCategory.σ i.succ) :
                                Δ[n + 1] _⦋n + 1 + 1⦌))))) :
                    (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
                  x,
                (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.castSucc.succ) :
                    (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
                  (stdSimplex.objMk₁ i.castSucc.succ.succ)).2 :
            Δ[1] _⦋n + 1⦌) :
          (a : Fin (n + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (X.map
                        (Quiver.Hom.op
                          (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                              (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                            ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.castSucc.succ) :
                                (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                                  (SimplexCategory.σ i.castSucc) :
                                Δ[n + 1] _⦋n + 1 + 1⦌))))) :
                    (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
                  x,
                (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.castSucc.succ) :
                    (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
                  (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).2 :
            Δ[1] _⦋n + 1⦌) :
          (a : Fin (n + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
have h : Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
  (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (X.map
                      (Quiver.Hom.op
                        (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                            (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.castSucc.succ) :
                              (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                                (SimplexCategory.σ i.succ) :
                              Δ[n + 1] _⦋n + 1 + 1⦌))))) :
                  (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
                x,
              stdSimplex.objMk₁ (i.castSucc.succ.succ.pred sorry)) :
            X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌).2 :
        (a : Fin (n + 1 + 1)) → Fin (1 + 1))
      k :
    Fin (HAdd.hAdd (α := ℕ) 1 1))
  (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (X.map
                      (Quiver.Hom.op
                        (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                            (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.castSucc.succ) :
                              (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                                (SimplexCategory.σ i.castSucc) :
                              Δ[n + 1] _⦋n + 1 + 1⦌))))) :
                  (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
                x,
              stdSimplex.objMk₁ (i.castSucc.castSucc.succ.castPred sorry)) :
            X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌).2 :
        (a : Fin (n + 1 + 1)) → Fin (1 + 1))
      k :
    Fin (HAdd.hAdd (α := ℕ) 1 1))
Tactic: rw [stdSimplex.δ_objMk₁_of_lt _ _ (by simp), stdSimplex.δ_objMk₁_of_le _ _ (by simp)]