-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
simp :
  Eq (α :=
    X.obj
      (op
        (Functor.obj (incl 1 (n + 1) ⋯)
          (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) ⋯).obj { obj := ⦋1⦌, property := Path₁._proof_5 }))) →
            X.obj (op ((incl 1 (n + 1) ⋯).obj { obj := ⦋0⦌, property := Path₁._proof_1 })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
              (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
            Δ :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      X.obj
        (op
          (Functor.obj (incl 1 (n + 1) ⋯)
            (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) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
              (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
            Δ :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      X.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 ⋯) 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⦌ ⋯))))

Tactic:
simp [← δ_one_mkOfSucc, tr_comp]

Premises used: SimplexCategory.Truncated.Hom.tr_comp, SimplexCategory.δ_one_mkOfSucc