awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ ⋯)))) =
    f.arrow i.succ
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.succ
have rw₁ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) sorry sorry) ≫ Quiver.Hom.op (tr (mkOfSucc i) sorry sorry))) :
      (a : X.obj (op { obj := ⦋m + 1⦌, property := sorry })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
    (sx.spineToSimplex (m + 1) sorry f) =
  f.arrow i.succ
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_gt hij, spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ ⋯)))) =
    f.arrow i.succ
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯) ≫ Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.succ
have rw₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) sorry sorry ≫ tr (SimplexCategory.δ j) sorry sorry))) :
      (a : X.obj (op { obj := ⦋m + 1⦌, property := sorry })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
    (sx.spineToSimplex (m + 1) sorry f) =
  f.arrow i.succ
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_gt hij, spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ ⋯)))) =
    f.arrow i.succ
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯) ≫ Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
rw₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.succ
have rw₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i ≫ SimplexCategory.δ j) sorry sorry))) :
      (a : X.obj (op { obj := ⦋m + 1⦌, property := sorry })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
    (sx.spineToSimplex (m + 1) sorry f) =
  f.arrow i.succ
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_gt hij, spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ ⋯)))) =
    f.arrow i.succ
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯) ≫ Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
rw₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i ≫ SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.succ
have rw₄ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i.succ) sorry sorry))) :
      (a : X.obj (op { obj := ⦋m + 1⦌, property := sorry })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
    (sx.spineToSimplex (m + 1) sorry f) =
  f.arrow i.succ
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_gt hij, spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ ⋯)))) =
    f.arrow i.succ
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯) ≫ Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
rw₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i ≫ SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i.succ) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.succ
have rw₅ : f.arrow i.succ = f.arrow i.succ
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_gt hij, spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) sorry sorry))) :
      (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := sorry }))) →
        (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := sorry })))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) sorry sorry))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := sorry }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := sorry })))
        (sx.spineToSimplex (m + 1) sorry f) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 2) ⦋m⦌ sorry)))) =
  sx.spineToDiagonal 2 sorry (f.interval (↑i : ℕ) 2 sorry)
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_eq hij, spineToSimplex_edge]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 2) ⦋m⦌ ⋯)))) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
have rw₁ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) sorry sorry) ≫ Quiver.Hom.op (tr (mkOfSucc i) sorry sorry))) :
      (a : X.obj (op { obj := ⦋m + 1⦌, property := sorry })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
    (sx.spineToSimplex (m + 1) sorry f) =
  sx.spineToDiagonal 2 sorry (f.interval (↑i : ℕ) 2 sorry)
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_eq hij, spineToSimplex_edge]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 2) ⦋m⦌ ⋯)))) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯) ≫ Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
have rw₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) sorry sorry ≫ tr (SimplexCategory.δ j) sorry sorry))) :
      (a : X.obj (op { obj := ⦋m + 1⦌, property := sorry })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
    (sx.spineToSimplex (m + 1) sorry f) =
  sx.spineToDiagonal 2 sorry (f.interval (↑i : ℕ) 2 sorry)
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_eq hij, spineToSimplex_edge]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 2) ⦋m⦌ ⋯)))) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯) ≫ Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
rw₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
have rw₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i ≫ SimplexCategory.δ j) sorry sorry))) :
      (a : X.obj (op { obj := ⦋m + 1⦌, property := sorry })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
    (sx.spineToSimplex (m + 1) sorry f) =
  sx.spineToDiagonal 2 sorry (f.interval (↑i : ℕ) 2 sorry)
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_eq hij, spineToSimplex_edge]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 2) ⦋m⦌ ⋯)))) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯) ≫ Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
rw₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i ≫ SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
have rw₄ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (intervalEdge (↑i : ℕ) 2 sorry) sorry sorry))) :
      (a : X.obj (op { obj := ⦋m + 1⦌, property := sorry })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
    (sx.spineToSimplex (m + 1) sorry f) =
  sx.spineToDiagonal 2 sorry (f.interval (↑i : ℕ) 2 sorry)
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_eq hij, spineToSimplex_edge]