awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n_1 : ℕ
X_1 : Truncated (n_1 + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
i : Fin 2
0 :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Functor.obj (trunc (n + 1) 1 ⋯) X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op) :
        (a :
            (fun (X : Type u) ↦ X)
              (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
          (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
      (![p.arrow 0, q.arrow 0] ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) =
    ![p.vertex 0, p.vertex 1, q.vertex 1]
      (Fin.castSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Functor.obj (trunc (n + 1) 1 ⋯) X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op) :
        (a :
            (fun (X : Type u) ↦ X)
              (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
          (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
      (![p.arrow 0, q.arrow 0] i) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] i.castSucc
have 1 : (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((Functor.obj (trunc (n + 1) 1 sorry) X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op) :
      (a :
          (fun (X : Type u) ↦ X)
            (((trunc (n + 1) 1 sorry).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
        (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 sorry).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
    (![p.arrow 0, q.arrow 0] ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1)))) =
  ![p.vertex 0, p.vertex 1, q.vertex 1] (Fin.castSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1))))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n_1 : ℕ
X_1 : Truncated (n_1 + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
i : Fin 2
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Functor.obj (trunc (n + 1) 1 ⋯) X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op) :
        (a :
            (fun (X : Type u) ↦ X)
              (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
          (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
      (![p.arrow 0, q.arrow 0] i) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] i.succ
have 0 : (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((Functor.obj (trunc (n + 1) 1 sorry) X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op) :
      (a :
          (fun (X : Type u) ↦ X)
            (((trunc (n + 1) 1 sorry).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
        (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 sorry).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
    (![p.arrow 0, q.arrow 0] ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1)))) =
  ![p.vertex 0, p.vertex 1, q.vertex 1] (Fin.succ ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1))))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n_1 : ℕ
X_1 : Truncated (n_1 + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
i : Fin 2
0 :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Functor.obj (trunc (n + 1) 1 ⋯) X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op) :
        (a :
            (fun (X : Type u) ↦ X)
              (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
          (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
      (![p.arrow 0, q.arrow 0] ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] (Fin.succ ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Functor.obj (trunc (n + 1) 1 ⋯) X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op) :
        (a :
            (fun (X : Type u) ↦ X)
              (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
          (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
      (![p.arrow 0, q.arrow 0] i) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] i.succ
have 1 : (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((Functor.obj (trunc (n + 1) 1 sorry) X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op) :
      (a :
          (fun (X : Type u) ↦ X)
            (((trunc (n + 1) 1 sorry).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
        (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 sorry).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
    (![p.arrow 0, q.arrow 0] ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1)))) =
  ![p.vertex 0, p.vertex 1, q.vertex 1] (Fin.succ ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1))))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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)
⊢ (X.spine a hₐ
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map φ.op) :
              (a_1 : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := hₘ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋a⦌, property := hₐ })))
            Δ)).vertex
      i =
    (X.spine m hₘ Δ).vertex
      ((Hom.toOrderHom φ.hom :
          (a : Fin ({ obj := ⦋a⦌, property := hₐ }.obj.len + 1)) → Fin ({ obj := ⦋m⦌, property := hₘ }.obj.len + 1))
        i)
have dsimp : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋a⦌ i) sorry hₐ))) :
        (a : X.obj (op { obj := ⦋a⦌, property := hₐ })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
      ((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⦌ sorry)))
  ((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)) sorry hₘ))) :
        (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
      Δ :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
Tactic: dsimp only [spine_vertex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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)
⊢ 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⦌ ⋯)))
have rw : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (φ.op ≫ Quiver.Hom.op (tr (⦋0⦌.const ⦋a⦌ i) sorry hₐ))) :
        (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
      Δ :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  ((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)) sorry hₘ))) :
        (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
      Δ :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
Tactic: rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp',
    SimplexCategory.const_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ))
⊢ X.spine l ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) ⋯ 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 := ⋯ })))
        Δ) =
    (X.spine m hₘ Δ).interval j l h
have hᵥ : ∀ (i : Fin (l + 1)),
  (X.spine l sorry
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) 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 })))
            Δ)).vertex
      i =
    ((X.spine m hₘ Δ).interval j l h).vertex i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ))
hᵥ :
  ∀ (i : Fin (l + 1)),
    (X.spine l ⋯
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) ⋯ 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 := ⋯ })))
              Δ)).vertex
        i =
      ((X.spine m hₘ Δ).interval j l h).vertex i
⊢ X.spine l ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) ⋯ 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 := ⋯ })))
        Δ) =
    (X.spine m hₘ Δ).interval j l h
have hₐ : ∀ (i : Fin l),
  (X.spine l sorry
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) 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 })))
            Δ)).arrow
      i =
    ((X.spine m hₘ Δ).interval j l h).arrow i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ))
i : Fin (l + 1)
⊢ (X.spine l ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) ⋯ 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 := ⋯ })))
            Δ)).vertex
      i =
    ((X.spine m hₘ Δ).interval j l h).vertex i
have hᵥ : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋l⦌ i) sorry sorry))) :
        (a : X.obj (op { obj := ⦋l⦌, property := sorry })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) sorry hₘ).op) :
            (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋l⦌, property := sorry }))
          Δ :
        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) ⦋0⦌ sorry)))
  (Path.vertex
      {
        vertex := fun (i : Fin (l + 1)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ (⟨j + (↑i : ℕ), sorry⟩ : Fin (m + 1))) sorry hₘ))) :
              (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
            Δ,
        arrow := fun (i : Fin l) ↦ (X.spine m hₘ Δ).arrow ⟨j + (↑i : ℕ), sorry⟩, arrow_src := sorry, arrow_tgt := sorry }
      i :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
Tactic: dsimp only [spine_vertex, Path.interval]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ))
i : Fin (l + 1)
⊢ 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 ⦋l⦌ i) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋l⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) ⋯ hₘ).op) :
              (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋l⦌, property := ⋯ }))
            Δ :
          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) ⦋0⦌ ⋯)))
    (Path.vertex
        {
          vertex := fun (i : Fin (l + 1)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ (⟨j + (↑i : ℕ), ⋯⟩ : Fin (m + 1))) ⋯ hₘ))) :
                (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
              Δ,
          arrow := fun (i : Fin l) ↦ (X.spine m hₘ Δ).arrow ⟨j + (↑i : ℕ), ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
        i :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
have hᵥ : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map ((tr (subinterval j l h) sorry hₘ).op ≫ Quiver.Hom.op (tr (⦋0⦌.const ⦋l⦌ i) sorry sorry))) :
        (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
      Δ :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  (Path.vertex
      {
        vertex := fun (i : Fin (l + 1)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ (⟨j + (↑i : ℕ), sorry⟩ : Fin (m + 1))) sorry hₘ))) :
              (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋0⦌, property := sorry }))
            Δ,
        arrow := fun (i : Fin l) ↦ (X.spine m hₘ Δ).arrow ⟨j + (↑i : ℕ), sorry⟩, arrow_src := sorry, arrow_tgt := sorry }
      i :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
Tactic: rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp,
      const_subinterval_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ))
i : Fin l
⊢ (X.spine l ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) ⋯ 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 := ⋯ })))
            Δ)).arrow
      i =
    ((X.spine m hₘ Δ).interval j l h).arrow i
have hₐ : 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 (mkOfSucc i) 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 h) sorry hₘ).op) :
            (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋l⦌, property := sorry }))
          Δ :
        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)))
  (Path.arrow
      { vertex := fun (i : Fin (l + 1)) ↦ (X.spine m hₘ Δ).vertex ⟨j + (↑i : ℕ), sorry⟩,
        arrow := fun (i : Fin l) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map (Quiver.Hom.op (tr (mkOfSucc (⟨j + (↑i : ℕ), sorry⟩ : Fin m)) sorry hₘ))) :
              (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
            Δ,
        arrow_src := sorry, arrow_tgt := sorry }
      i :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
Tactic: dsimp only [spine_arrow, Path.interval]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hₘ))
i : Fin l
⊢ 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 (mkOfSucc i) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋l⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l h) ⋯ hₘ).op) :
              (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋l⦌, property := ⋯ }))
            Δ :
          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⦌ ⋯)))
    (Path.arrow
        { vertex := fun (i : Fin (l + 1)) ↦ (X.spine m hₘ Δ).vertex ⟨j + (↑i : ℕ), ⋯⟩,
          arrow := fun (i : Fin l) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.map (Quiver.Hom.op (tr (mkOfSucc (⟨j + (↑i : ℕ), ⋯⟩ : Fin m)) ⋯ hₘ))) :
                (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
              Δ,
          arrow_src := ⋯, arrow_tgt := ⋯ }
        i :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
have hₐ : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map ((tr (subinterval j l h) sorry hₘ).op ≫ Quiver.Hom.op (tr (mkOfSucc i) sorry sorry))) :
        (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
      Δ :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
  (Path.arrow
      { vertex := fun (i : Fin (l + 1)) ↦ (X.spine m hₘ Δ).vertex ⟨j + (↑i : ℕ), sorry⟩,
        arrow := fun (i : Fin l) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map (Quiver.Hom.op (tr (mkOfSucc (⟨j + (↑i : ℕ), sorry⟩ : Fin m)) sorry hₘ))) :
              (a : X.obj (op { obj := ⦋m⦌, property := hₘ })) → X.obj (op { obj := ⦋1⦌, property := sorry }))
            Δ,
        arrow_src := sorry, arrow_tgt := sorry }
      i :
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ sorry)))
Tactic: rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp,
      mkOfSucc_subinterval_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin (n + 1)
⊢ f.vertex i = g.vertex i
have rw : g.vertex i = g.vertex i
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin n
⊢ f.arrow i = g.arrow i
have rw : g.arrow i = g.arrow i
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
⊢ f = g
have hᵥ : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), f.vertex i = g.vertex i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
hᵥ : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), f.vertex i = g.vertex i
⊢ f = g
have hₐ : ∀ (i : Fin 0), f.arrow i = g.arrow i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ f.vertex i = g.vertex i
have hᵥ : f.vertex ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋0⦌.len + 1))) =
  g.vertex ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
n : ℕ
f : X.Path n
j l : ℕ
k' : Fin l
k : Fin n
h : j + l ≤ n
hkk' : j + (↑k' : ℕ) = (↑k : ℕ)
⊢ (f.interval j l h).arrow k' = f.arrow k
have dsimp : f.arrow (⟨j + (↑k' : ℕ), sorry⟩ : Fin n) = f.arrow k
Tactic: dsimp [interval, arrow, Truncated.Path.interval, Truncated.Path.arrow]