-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ))
i : Fin (l + 1)
hᵥ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map ((tr (subinterval j l h) ⋯ hₘ).op ≫ Quiver.Hom.op (tr (⦋0⦌.const ⦋l⦌ i) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        Δ :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    (Path.vertex
        {
          vertex := fun (i : Fin (l + 1)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ (⟨j + (↑i : ℕ), ⋯⟩ : Fin (m + 1))) ⋯ hₘ))) :
                (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
              Δ,
          arrow := fun (i : Fin l) ↦ (X.spine m hₘ Δ).arrow ⟨j + (↑i : ℕ), ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
        i :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
hᵥ₁ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋l⦌ i) ⋯ ⋯ ≫ tr (subinterval j l h) ⋯ hₘ))) :
          (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        Δ :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    (Path.vertex
        {
          vertex := fun (i : Fin (l + 1)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ (⟨j + (↑i : ℕ), ⋯⟩ : Fin (m + 1))) ⋯ hₘ))) :
                (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
              Δ,
          arrow := fun (i : Fin l) ↦ (X.spine m hₘ Δ).arrow ⟨j + (↑i : ℕ), ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
        i :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
hᵥ₂ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋l⦌ i ≫ subinterval j l h) ⋯ hₘ))) :
          (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        Δ :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    (Path.vertex
        {
          vertex := fun (i : Fin (l + 1)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ (⟨j + (↑i : ℕ), ⋯⟩ : Fin (m + 1))) ⋯ hₘ))) :
                (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
              Δ,
          arrow := fun (i : Fin l) ↦ (X.spine m hₘ Δ).arrow ⟨j + (↑i : ℕ), ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
        i :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
hᵥ₃ hᵥ₄ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ ⟨j + (↑i : ℕ), ⋯⟩) ⋯ hₘ))) :
            TypeCat.Fun
              (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ)))
              (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))) :
          (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        Δ :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    (Path.vertex
        {
          vertex := fun (i : Fin (l + 1)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ (⟨j + (↑i : ℕ), ⋯⟩ : Fin (m + 1))) ⋯ hₘ))) :
                (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
              Δ,
          arrow := fun (i : Fin l) ↦ (X.spine m hₘ Δ).arrow ⟨j + (↑i : ℕ), ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
        i :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
⊢ Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋l⦌ i) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋l⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) ⋯ hₘ).op) :
              (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋l⦌, property := ⋯ }))
            Δ :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋l⦌ ⋯))) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    (Path.vertex
        {
          vertex := fun (i : Fin (l + 1)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ (⟨j + (↑i : ℕ), ⋯⟩ : Fin (m + 1))) ⋯ hₘ))) :
                (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
              Δ,
          arrow := fun (i : Fin l) ↦ (X.spine m hₘ Δ).arrow ⟨j + (↑i : ℕ), ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
        i :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp,
      const_subinterval_eq]

Premises used: CategoryTheory.op_comp, SimplexCategory.Truncated.Hom.tr_comp, SimplexCategory.const_subinterval_eq, CategoryTheory.Functor.map_comp_apply