-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n : ℕ
X_1 : Truncated (n + 1)
m_1 : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((Functor.obj (trunc (n + 1) 1 ⋯) Y).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 ⋯) Y).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op) :
          (a :
              (fun (X : Type u) ↦ X)
                (((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
            (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
            (f.arrow i) :
          (fun (X : Type u) ↦ X)
            (Y.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 ⋯) Y).obj
          (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0⦌, property := ⋯ })))
        (f.vertex i.succ) :
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
have simp : Eq (α :=
  (Functor.obj (trunc (n + 1) 1 sorry) Y).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 sorry) Y).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op) :
        (a : ((trunc (n + 1) 1 sorry).obj Y).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 })) →
          ((trunc (n + 1) 1 sorry).obj Y).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry))) :
            (a : X.obj (op { obj := ⦋1⦌, property := sorry })) → Y.obj (op { obj := ⦋1⦌, property := sorry }))
          (f.arrow i) :
        Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry))) :
    (Functor.obj (trunc (n + 1) 1 sorry) Y).obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry))) :
        (a : X.obj (op { obj := ⦋0⦌, property := sorry })) → Y.obj (op { obj := ⦋0⦌, property := sorry }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) sorry sorry))) :
            (a : X.obj (op { obj := ⦋0 + 1⦌, property := sorry })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
          (f.arrow i) :
        X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry))) :
    Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
Tactic: simp only [← f.arrow_tgt i]