-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ h))
i : Fin m
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((Functor.obj (trunc (n + 1) 1 ⋯) X).obj
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.obj (trunc (n + 1) 1 ⋯) X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op) :
          (a :
              (fun (X : Type u) ↦ X)
                (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
            (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
            Δ :
          (fun (X : Type u) ↦ X)
            (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))) :
      (fun (X : Type u) ↦ X)
        ((Functor.obj (trunc (n + 1) 1 ⋯) X).obj
          (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ i.castSucc) ⋯ h))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
        Δ :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
have simp : Eq (α :=
  X.obj
    (op
      (Functor.obj (incl 1 (n + 1) sorry)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (ObjectProperty.homMk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) (SimplexCategory.δ 1)))) :
        (a : X.obj (op ((incl 1 (n + 1) sorry).obj { obj := ⦋1⦌, property := Path₁._proof_5 }))) →
          X.obj (op ((incl 1 (n + 1) sorry).obj { obj := ⦋0⦌, property := Path₁._proof_1 })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) sorry h))) :
            (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
          Δ :
        X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry))) :
    X.obj
      (op
        (Functor.obj (incl 1 (n + 1) sorry)
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) sorry sorry))) :
        (a : X.obj (op { obj := ⦋1⦌, property := sorry })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) sorry h))) :
            (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
          Δ :
        X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry))) :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
Tactic: simp [← δ_one_mkOfSucc, tr_comp]