awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
⊢ Eq.{u + 1} (α :=
    Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    (Path.arrow
      ((sy.spineEquiv (m + 1) ⋯ : (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.Path (m + 1))
        (sy.spineToSimplex (m + 1) ⋯ (f.map σ)))
      k)
    (Path.arrow
      ((sy.spineEquiv (m + 1) ⋯ : (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.Path (m + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f) :
          (fun (X : Type u) ↦ X)
            (Y.obj
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯)))))
      k)
have a : Eq (α := Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) sorry sorry))) :
        (a : Y.obj (op { obj := ⦋m + 1⦌, property := sorry })) → Y.obj (op { obj := ⦋1⦌, property := sorry }))
      (sy.spineToSimplex (m + 1) sorry (f.map σ)) :
    Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) sorry sorry))) :
        (a : Y.obj (op { obj := ⦋m + 1⦌, property := sorry })) → Y.obj (op { obj := ⦋1⦌, property := sorry }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (σ.app
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ sorry))) :
            (a : X.obj (op { obj := ⦋m + 1⦌, property := sorry })) → Y.obj (op { obj := ⦋m + 1⦌, property := sorry }))
          (sx.spineToSimplex (m + 1) sorry f) :
        Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ sorry))) :
    Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
Tactic: dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
⊢ Eq (α := Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯))) :
          (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯))) :
          (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯))) :
              (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))
            (sx.spineToSimplex (m + 1) ⋯ f) :
          Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯))) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
have a : Eq (α := Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) sorry sorry))) :
        (a : Y.obj (op { obj := ⦋m + 1⦌, property := sorry })) → Y.obj (op { obj := ⦋1⦌, property := sorry }))
      (sy.spineToSimplex (m + 1) sorry (f.map σ)) :
    Y.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 (mkOfSucc k) sorry sorry)) ≫
            σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := sorry })))
      (sx.spineToSimplex (m + 1) sorry f) :
    (fun (X : Type u) ↦ X)
      (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry))))
Tactic: rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality]
-- 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 + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (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))).vertex
      i =
    f.vertex i.castSucc
have rw : f.vertex ((Hom.toOrderHom (SimplexCategory.δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1)) i) =
  f.vertex i.castSucc
Tactic: rw [spine_vertex, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    SimplexCategory.const_comp, spineToSimplex_vertex]
-- 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 + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1)) i) =
    f.vertex i.castSucc
have dsimp : f.vertex (j.succAbove i) = f.vertex i.castSucc
Tactic: dsimp only [SimplexCategory.δ, len_mk, mkHom, Hom.toOrderHom_mk,
    Fin.succAboveOrderEmb_apply, OrderEmbedding.toOrderHom_coe]
-- 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 + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ f.vertex (j.succAbove i) = f.vertex i.castSucc
have rw : f.vertex i.castSucc = f.vertex i.castSucc
Tactic: rw [Fin.succAbove_of_castSucc_lt j i hij]
-- 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 + 1)
j : Fin (m + 2)
hij : j ≤ i.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))).vertex
      i =
    f.vertex i.succ
have rw : f.vertex ((Hom.toOrderHom (SimplexCategory.δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1)) i) = f.vertex i.succ
Tactic: rw [spine_vertex, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    SimplexCategory.const_comp, spineToSimplex_vertex]
-- 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 + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1)) i) =
    f.vertex i.succ
have dsimp : f.vertex (j.succAbove i) = f.vertex i.succ
Tactic: dsimp only [SimplexCategory.δ, len_mk, mkHom, Hom.toOrderHom_mk,
    Fin.succAboveOrderEmb_apply, OrderEmbedding.toOrderHom_coe]
-- 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 + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ f.vertex (j.succAbove i) = f.vertex i.succ
have rw : f.vertex i.succ = f.vertex i.succ
Tactic: rw [Fin.succAbove_of_le_castSucc j i hij]
-- 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 : i.succ.castSucc < j
⊢ (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.castSucc
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 + 1) ⦋m⦌ sorry)))) =
  f.arrow i.castSucc
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_lt 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 : i.succ.castSucc < j
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.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 =
    f.arrow i.castSucc
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.castSucc
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_lt 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 : i.succ.castSucc < j
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.castSucc
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.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 =
    f.arrow i.castSucc
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.castSucc
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_lt 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 : i.succ.castSucc < j
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.castSucc
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.castSucc
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.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 =
    f.arrow i.castSucc
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.castSucc
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_lt 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 : i.succ.castSucc < j
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.castSucc
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.castSucc
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.castSucc
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.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 =
    f.arrow i.castSucc
have rw₄ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i.castSucc) 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.castSucc
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_lt 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 : i.succ.castSucc < j
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.castSucc
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.castSucc
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.castSucc
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.castSucc
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i.castSucc) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.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 =
    f.arrow i.castSucc
have rw₅ : f.arrow i.castSucc = f.arrow i.castSucc
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_lt 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
⊢ (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))) :
      (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 + 1) ⦋m⦌ sorry)))) =
  f.arrow i.succ
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_gt hij, spineToSimplex_arrow]