awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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))))
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] ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) =
    ![p.vertex 0, p.vertex 1, q.vertex 1]
      (Fin.castSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : 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

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
⊢ (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))))

Tactic:
p.arrow_src 0

Premises used: Eq.mpr, Quiver.Hom.op, SimplexCategory.mkHom, Fin.cons, Fin.induction.go, Fin.ofNat, SimplexCategory.δ, Fin.induction, SSet.Truncated.Path.arrow_src, CategoryTheory.ObjectProperty.homMk, Fin.cases, OrderEmbedding.toOrderHom, OfNat.ofNat, Matrix.vecCons, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
⊢ (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))))

Tactic:
exact p.arrow_src 0

Premises used: SSet.Truncated.Path.arrow_src, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
⊢ (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) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) =
    ![p.vertex 0, p.vertex 1, q.vertex 1]
      (Fin.castSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))

Tactic:
(q.arrow_src 0).trans h.symm

Premises used: Eq.mpr, Quiver.Hom.op, SimplexCategory.mkHom, Fin.cons, Fin.induction.go, SimplexCategory.δ, Fin.induction, SSet.Truncated.Path.arrow_src, CategoryTheory.ObjectProperty.homMk, Fin.cases, OrderEmbedding.toOrderHom, OfNat.ofNat, Eq.symm, Matrix.vecCons, Eq.trans, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
⊢ (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) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) =
    ![p.vertex 0, p.vertex 1, q.vertex 1]
      (Fin.castSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))

Tactic:
exact (q.arrow_src 0).trans h.symm

Premises used: SSet.Truncated.Path.arrow_src, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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))))
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] ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] (Fin.succ ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : 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

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
⊢ (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))))

Tactic:
p.arrow_tgt 0

Premises used: Eq.mpr, Fin.succ, Quiver.Hom.op, SimplexCategory.mkHom, Fin.cons, Fin.induction.go, Fin.ofNat, SimplexCategory.δ, Fin.induction, CategoryTheory.ObjectProperty.homMk, SSet.Truncated.Path.arrow_tgt, Fin.cases, OrderEmbedding.toOrderHom, OfNat.ofNat, Matrix.vecCons, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
⊢ (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))))

Tactic:
exact p.arrow_tgt 0

Premises used: SSet.Truncated.Path.arrow_tgt, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
⊢ (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) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] (Fin.succ ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))

Tactic:
q.arrow_tgt 0

Premises used: Eq.mpr, Fin.succ, Quiver.Hom.op, SimplexCategory.mkHom, Fin.cons, Fin.induction.go, Fin.ofNat, SimplexCategory.δ, Fin.induction, CategoryTheory.ObjectProperty.homMk, SSet.Truncated.Path.arrow_tgt, Fin.cases, OrderEmbedding.toOrderHom, OfNat.ofNat, Matrix.vecCons, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
⊢ (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) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] (Fin.succ ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))

Tactic:
exact q.arrow_tgt 0

Premises used: SSet.Truncated.Path.arrow_tgt, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f : X.Path m
j l : ℕ
h : j + l ≤ m
i : Fin (l + 1)
⊢ j + (↑i : ℕ) < m + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f : X.Path m
j l : ℕ
h : j + l ≤ m
i : Fin l
⊢ j + (↑i : ℕ) < m

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X_1 : Truncated (n + 1)
m_1 : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ Eq (α :=
    (Functor.obj (trunc (n + 1) 1 ⋯) Y).obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.obj (trunc (n + 1) 1 ⋯) Y).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op) :
          (a : ((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 })) →
            ((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
              (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
            (f.arrow i) :
          Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      (Functor.obj (trunc (n + 1) 1 ⋯) Y).obj
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋0⦌, property := ⋯ })) → Y.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) ⋯ ⋯))) :
              (a : X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
            (f.arrow i) :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))

Tactic:
ConcreteCategory.congr_hom (σ.naturality (tr (δ 1)).op) _ |>.symm

Premises used: SimplexCategory.Truncated.Hom.tr, Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, CategoryTheory.NatTrans.naturality, CategoryTheory.ObjectProperty.homMk, CategoryTheory.ConcreteCategory.congr_hom, OrderEmbedding.toOrderHom, OfNat.ofNat, Eq.symm, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X_1 : Truncated (n + 1)
m_1 : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ Eq (α :=
    (Functor.obj (trunc (n + 1) 1 ⋯) Y).obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.obj (trunc (n + 1) 1 ⋯) Y).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op) :
          (a : ((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 })) →
            ((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
              (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
            (f.arrow i) :
          Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      (Functor.obj (trunc (n + 1) 1 ⋯) Y).obj
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋0⦌, property := ⋯ })) → Y.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) ⋯ ⋯))) :
              (a : X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
            (f.arrow i) :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))

Tactic:
exact ConcreteCategory.congr_hom (σ.naturality (tr (δ 1)).op) _ |>.symm

Premises used: SimplexCategory.Truncated.Hom.tr, Quiver.Hom.op, SimplexCategory.δ, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, OfNat.ofNat, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X_1 : Truncated (n + 1)
m_1 : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ Eq (α :=
    (Functor.obj (trunc (n + 1) 1 ⋯) Y).obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.obj (trunc (n + 1) 1 ⋯) Y).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op) :
          (a : ((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 })) →
            ((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
              (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
            (f.arrow i) :
          Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      (Functor.obj (trunc (n + 1) 1 ⋯) Y).obj
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋0⦌, property := ⋯ })) → Y.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) ⋯ ⋯))) :
              (a : X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
            (f.arrow i) :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))

Tactic:
ConcreteCategory.congr_hom (σ.naturality (tr (δ 0)).op) _ |>.symm

Premises used: SimplexCategory.Truncated.Hom.tr, Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, CategoryTheory.NatTrans.naturality, CategoryTheory.ObjectProperty.homMk, CategoryTheory.ConcreteCategory.congr_hom, OrderEmbedding.toOrderHom, OfNat.ofNat, Eq.symm, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X_1 : Truncated (n + 1)
m_1 : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ Eq (α :=
    (Functor.obj (trunc (n + 1) 1 ⋯) Y).obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.obj (trunc (n + 1) 1 ⋯) Y).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op) :
          (a : ((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 })) →
            ((trunc (n + 1) 1 ⋯).obj Y).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
              (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
            (f.arrow i) :
          Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      (Functor.obj (trunc (n + 1) 1 ⋯) Y).obj
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋0⦌, property := ⋯ })) → Y.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) ⋯ ⋯))) :
              (a : X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
            (f.arrow i) :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))

Tactic:
exact ConcreteCategory.congr_hom (σ.naturality (tr (δ 0)).op) _ |>.symm

Premises used: SimplexCategory.Truncated.Hom.tr, Quiver.Hom.op, SimplexCategory.δ, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, OfNat.ofNat, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin (m + 1)
⊢ (f.map σ).vertex i =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋0⦌, property := ⋯ })))
      (f.vertex i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ (f.map σ).arrow i =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (σ.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 := ⋯ })))
      (f.arrow i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
j l : ℕ
h : j + l ≤ m
⊢ (f.map σ).interval j l h = (f.interval j l h).map σ

Tactic:
rfl

Premises used: SSet.Truncated.Path.map, rfl