-- 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⦌
⊢ Eq (α := X _⦋n + 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)).1 :
      X _⦋n + 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)).1 :
      X _⦋n + 1⦌)
have h : Eq (α := X _⦋n + 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⦌)
                    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                      (SimplexCategory.δ i.castSucc.succ ≫ SimplexCategory.σ i.succ))))) :
            (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)).1 :
    X _⦋n + 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)).1 :
    X _⦋n + 1⦌)
Tactic: rw [stdSimplex.δ_objEquiv_symm_apply, stdSimplex.δ_objEquiv_symm_apply,
        SimplexCategory.δ_comp_σ_succ, ← Fin.castSucc_succ, SimplexCategory.δ_comp_σ_self]