awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
m : SimplexCategory
hm : m.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))))
      x
have w : ∀ (m : ℕ) (hm : ⦋m⦌.len ≤ n + 1)
  (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
      x
Tactic: induction m using SimplexCategory.rec with | _ m
Cleared hypotheses: m, hm, x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
m : ℕ
hm : ⦋m⦌.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
      x
have w : ∀ (hm : ⦋0⦌.len ≤ n + 1)
  (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
      x
Tactic: obtain _ | m := m
Cleared hypotheses: m, hm, x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
m : ℕ
hm : ⦋m⦌.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))
w :
  ∀ (hm : ⦋0⦌.len ≤ n + 1)
    (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
        x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
      x
have w₁ : ∀ (m : ℕ) (hm : ⦋m + 1⦌.len ≤ n + 1)
  (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))))
      x
Tactic: obtain _ | m := m
Cleared hypotheses: m, hm, x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (hypothesis)
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
hm : ⦋0⦌.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
      x
have fac : SimplexCategory.δ (Fin.castSucc 0) ≫ SimplexCategory.σ 0 = 𝟙 ⦋0⦌
Tactic: have fac := δ_comp_σ_self (i := (0 : Fin 1))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin (m + 1)
f : X.Path m
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ i) ⋯ h))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
      (sx.spineToSimplex m h f) =
    f.vertex i
have rw : (X.spine m h (sx.spineToSimplex m h f)).vertex i = f.vertex i
Tactic: rw [← spine_vertex, spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin (m + 1)
f : X.Path m
rw : (X.spine m h (sx.spineToSimplex m h f)).vertex i = f.vertex i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ i) ⋯ h))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
      (sx.spineToSimplex m h f) =
    f.vertex i
have rw₁ : f.vertex i = f.vertex i
Tactic: rw [← spine_vertex, spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin m
f : X.Path m
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      (sx.spineToSimplex m h f) =
    f.arrow i
have rw : (X.spine m h (sx.spineToSimplex m h f)).arrow i = f.arrow i
Tactic: rw [← spine_arrow, spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin m
f : X.Path m
rw : (X.spine m h (sx.spineToSimplex m h f)).arrow i = f.arrow i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      (sx.spineToSimplex m h f) =
    f.arrow i
have rw₁ : f.arrow i = f.arrow i
Tactic: rw [← spine_arrow, spine_spineToSimplex_apply]
-- 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
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋l⦌ ⋯))))
    ((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⦌ ⋯))))
    (sx.spineToSimplex l ⋯ (f.interval j l hjl) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋l⦌ ⋯)))
have a : Eq (α := X.Path l)
  ((sx.spineEquiv l sorry : (a : X.obj (op { obj := ⦋l⦌, property := sorry })) → X.Path l)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l hjl) sorry 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 := sorry })))
          (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⦌ sorry)))) :
    X.Path l)
  ((sx.spineEquiv l sorry : (a : X.obj (op { obj := ⦋l⦌, property := sorry })) → X.Path l)
      (sx.spineToSimplex l sorry (f.interval j l hjl)) :
    X.Path l)
Tactic: apply sx.spineInjective l
-- 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
⊢ Eq (α := X.Path l)
    ((sx.spineEquiv l ⋯ : (a : X.obj (op { obj := ⦋l⦌, property := ⋯ })) → X.Path l)
        ((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.Path l)
    ((sx.spineEquiv l ⋯ : (a : X.obj (op { obj := ⦋l⦌, property := ⋯ })) → X.Path l)
        (sx.spineToSimplex l ⋯ (f.interval j l hjl)) :
      X.Path l)
have a : X.spine l sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l hjl) sorry h).op) :
        (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋l⦌, property := sorry }))
      (sx.spineToSimplex m h f)) =
  X.spine l sorry (sx.spineToSimplex l sorry (f.interval j l hjl))
Tactic: dsimp only [spineEquiv, Equiv.coe_fn_mk]
-- 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
⊢ X.spine l ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l hjl) ⋯ h).op) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋l⦌, property := ⋯ }))
        (sx.spineToSimplex m h f)) =
    X.spine l ⋯ (sx.spineToSimplex l ⋯ (f.interval j l hjl))
have a : X.spine l sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l hjl) sorry h).op) :
        (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋l⦌, property := sorry }))
      (sx.spineToSimplex m h f)) =
  f.interval j l hjl
Tactic: rw [spine_spineToSimplex_apply]
-- 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
⊢ X.spine l ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l hjl) ⋯ h).op) :
          (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋l⦌, property := ⋯ }))
        (sx.spineToSimplex m h f)) =
    f.interval j l hjl
have h₁ : f = X.spine m h (sx.spineToSimplex m h f)
Tactic: convert! spine_map_subinterval X m h j l hjl <| sx.spineToSimplex m h f
-- 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
⊢ 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 (diag l) sorry sorry))) :
        (a : X.obj (op { obj := ⦋l⦌, property := sorry })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l hjl) sorry 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 := sorry })))
          (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⦌ sorry)))) :
    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]
-- 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
⊢ sy.spineToSimplex (m + 1) ⋯ (f.map σ) =
    (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)
have a : Eq (α := Y.Path (m + 1))
  ((sy.spineEquiv (m + 1) sorry : (a : Y.obj (op { obj := ⦋m + 1⦌, property := sorry })) → Y.Path (m + 1))
      (sy.spineToSimplex (m + 1) sorry (f.map σ)) :
    Y.Path (m + 1))
  ((sy.spineEquiv (m + 1) sorry : (a : Y.obj (op { obj := ⦋m + 1⦌, property := sorry })) → Y.Path (m + 1))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (σ.app
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 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 := ⦋m + 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) ⦋m + 1⦌ sorry)))) :
    Y.Path (m + 1))
Tactic: apply sy.spineInjective (m + 1)
-- 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
⊢ Eq (α := Y.Path (m + 1))
    ((sy.spineEquiv (m + 1) ⋯ : (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.Path (m + 1))
        (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) :
      Y.Path (m + 1))
    ((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⦌ ⋯)))) :
      Y.Path (m + 1))
have a : ∀ (k : Fin (m + 1)),
  Eq.{u + 1} (α :=
    Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
    (Path.arrow
      ((sy.spineEquiv (m + 1) sorry : (a : Y.obj (op { obj := ⦋m + 1⦌, property := sorry })) → Y.Path (m + 1))
        (sy.spineToSimplex (m + 1) sorry (f.map σ)))
      k)
    (Path.arrow
      ((sy.spineEquiv (m + 1) sorry : (a : Y.obj (op { obj := ⦋m + 1⦌, property := sorry })) → Y.Path (m + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 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 := ⦋m + 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) ⦋m + 1⦌ sorry)))))
      k)
Tactic: ext k