-- 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⦌
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    i.succ) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
          δ Y i.castSucc.succ))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    i.castSucc) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
          δ Y i.castSucc.succ))
      x
have h : Eq (α := Y _⦋n + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
        (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌) → Y _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ (tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1]) i.castSucc.succ) :
            (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) → (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌)
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                i.succ) :
            (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) :
        tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1] _⦋n + 1⦌) :
    Y _⦋n + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
        (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌) → Y _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ (tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1]) i.castSucc.succ) :
            (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) → (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌)
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                i.castSucc) :
            (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) :
        tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1] _⦋n + 1⦌) :
    Y _⦋n + 1⦌)
Tactic: simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.δ_naturality_apply]