-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X_1 : Truncated (n + 1)
m_1 : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
simp :
  Eq (α :=
    (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 : ((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 })) →
            ((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 : X.obj (op { obj := ⦋1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
            (f.arrow i) :
          Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      (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 : X.obj (op { obj := ⦋0⦌, property := ⋯ })) → Y.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) ⋯ ⋯))) :
              (a : X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
            (f.arrow i) :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
⊢ 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⦌ ⋯))))

Tactic:
simp only [← f.arrow_tgt i]

Premises used: SSet.Truncated.Path.arrow_tgt