-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
rw :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (intervalEdge j l hjl) ⋯ h))) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sx.spineToSimplex m h f) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (diag l) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋l⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l hjl) ⋯ h).op) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋l⦌, property := ⋯ })))
            (sx.spineToSimplex m h f) :
          (fun (X : Type u) ↦ X)
            (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) ⦋1⦌ ⋯)))
h₁ : m ≤ n + 1
rw₁ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (intervalEdge j l hjl) ⋯ h))) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sx.spineToSimplex m h f) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map ((tr (subinterval j l hjl) ⋯ h).op ≫ Quiver.Hom.op (tr (diag l) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sx.spineToSimplex m h f) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
h₂ : m ≤ n + 1
rw₂ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (intervalEdge j l hjl) ⋯ h))) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sx.spineToSimplex m h f) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map (Quiver.Hom.op (tr (diag l) ⋯ ⋯ ≫ tr (subinterval j l hjl) ⋯ h))) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sx.spineToSimplex m h f) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
h₃ : m ≤ n + 1
rw₃ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (intervalEdge j l hjl) ⋯ h))) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sx.spineToSimplex m h f) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (diag l ≫ subinterval j l hjl) ⋯ h))) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sx.spineToSimplex m h f) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
h₄ : m ≤ n + 1
⊢ Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (intervalEdge j l hjl) ⋯ h))) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sx.spineToSimplex m h f) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (diag l) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋l⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sx.spineToSimplex l ⋯ (f.interval j l hjl)) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
have rw₄ : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (intervalEdge j l hjl) sorry h))) :
        (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
      (sx.spineToSimplex m h f) :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (intervalEdge j l hjl) sorry h))) :
        (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
      (sx.spineToSimplex m h f) :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
Tactic: rw [← spineToSimplex_interval, ← Functor.map_comp_apply, ← op_comp,
    ← tr_comp, diag_subinterval_eq]