-- 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ₘ))
a : ℕ
hₐ : a ≤ n + 1
φ :
  Quiver.Hom (V := ObjectProperty.FullSubcategory (C := SimplexCategory) fun (a : SimplexCategory) ↦ a.len ≤ n + 1)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋a⦌ hₐ)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ)
i : Fin (a + 1)
rw :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (φ.op ≫ Quiver.Hom.op (tr (⦋0⦌.const ⦋a⦌ i) ⋯ 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⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom : (a : Fin (a + 1)) → Fin (m + 1)) i)) ⋯ 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⦌ ⋯)))
rw₁ :
  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 ⦋a⦌ i) ⋯ 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⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom : (a : Fin (a + 1)) → Fin (m + 1)) i)) ⋯ 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⦌ ⋯)))
rw₂ :
  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 ⦋a⦌ i ≫ φ.hom) ⋯ 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⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom : (a : Fin (a + 1)) → Fin (m + 1)) i)) ⋯ 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⦌ ⋯)))
rw₃ rw₄ :
  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
                    (ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1)
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ))
                    ((Hom.toOrderHom φ.hom : (a : Fin (⦋a⦌.len + 1)) → Fin ({ obj := ⦋m⦌, property := hₘ }.obj.len + 1))
                      i))
                  ⋯ 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⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom : (a : Fin (a + 1)) → Fin (m + 1)) i)) ⋯ 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⦌ ⋯)))
⊢ 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 ⦋a⦌ i) ⋯ hₐ))) :
          (a : X.obj (op { obj := ⦋a⦌, property := hₐ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map φ.op) :
              (a_1 : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋a⦌, property := hₐ }))
            Δ :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋a⦌ hₐ))) :
      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 ⦋m⦌ ((Hom.toOrderHom φ.hom : (a : Fin (a + 1)) → Fin (m + 1)) i)) ⋯ 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⦌ ⋯)))

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp',
    SimplexCategory.const_comp]

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