awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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))
i : Fin m
⊢ Eq (α :=
    X.obj
      (op
        (Functor.obj (incl 1 (n + 1) ⋯)
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op
                (ObjectProperty.homMk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) (SimplexCategory.δ 1)))) :
          (a : X.obj (op ((incl 1 (n + 1) ⋯).obj { obj := ⦋1⦌, property := Path₁._proof_5 }))) →
            X.obj (op ((incl 1 (n + 1) ⋯).obj { obj := ⦋0⦌, property := Path₁._proof_1 })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
              (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
            Δ :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      X.obj
        (op
          (Functor.obj (incl 1 (n + 1) ⋯)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
              (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
            Δ :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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))
i : Fin m
⊢ Eq (α :=
    X.obj
      (op
        (Functor.obj (incl 1 (n + 1) ⋯)
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op
                (ObjectProperty.homMk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) (SimplexCategory.δ 0)))) :
          (a : X.obj (op ((incl 1 (n + 1) ⋯).obj { obj := ⦋1⦌, property := Path₁._proof_5 }))) →
            X.obj (op ((incl 1 (n + 1) ⋯).obj { obj := ⦋0⦌, property := Path₁._proof_1 })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
              (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
            Δ :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      X.obj
        (op
          (Functor.obj (incl 1 (n + 1) ⋯)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) ⋯ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) → X.obj (op { obj := ⦋0⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
              (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
            Δ :
          X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
k m : ℕ
h : m ≤ k + 1
hₙ : k ≤ n
⊢ ((trunc (n + 1) (k + 1) ⋯).obj X).spine m h = X.spine m ⋯

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, SSet.Truncated.spine, Quiver.Hom.op, CategoryTheory.ObjectProperty.ιOfLE, SimplexCategory.mkHom, CategoryTheory.Functor.comp, SimplexCategory.mkOfSucc, SimplexCategory.const, CategoryTheory.ObjectProperty.homMk, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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ₘ))
i : Fin (m + 1)
⊢ (X.spine m hₘ Δ).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 := ⋯ })))
      Δ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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ₘ))
i : Fin m
⊢ (X.spine m hₘ Δ).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 := ⋯ })))
      Δ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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)
dsimp :
  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⦌ ⋯)))
⊢ (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)

Tactic:
dsimp only [spine_vertex]

Premises used: SSet.Truncated.spine_vertex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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ₘ))
⊢ l ≤ n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
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
⊢ 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

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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)
hᵥ :
  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⦌ ⋯)))
⊢ (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

Tactic:
dsimp only [spine_vertex, Path.interval]

Premises used: SSet.Truncated.spine_vertex, SSet.Truncated.Path.interval
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
hₐ :
  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⦌ ⋯)))
⊢ (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

Tactic:
dsimp only [spine_arrow, Path.interval]

Premises used: SSet.Truncated.spine_arrow, SSet.Truncated.Path.interval
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin (n + 1)
rw rw₁ : g.vertex i = g.vertex i
⊢ f.vertex i = g.vertex i

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin n
rw rw₁ : g.arrow i = g.arrow i
⊢ f.arrow i = g.arrow i

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
f : X.Path n
i : Fin n
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 1) :
        (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (f.arrow i) =
    f.vertex i.castSucc

Tactic:
Truncated.Path.arrow_src f i

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, SSet.Truncated.Path.arrow_src, OrderEmbedding.toOrderHom, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
f : X.Path n
i : Fin n
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (f.arrow i) =
    f.vertex i.succ

Tactic:
Truncated.Path.arrow_tgt f i

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, SSet.Truncated.Path.arrow_tgt, OrderEmbedding.toOrderHom, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
f g : X.Path n
hᵥ : f.vertex = g.vertex
hₐ : f.arrow = g.arrow
⊢ f = g

Tactic:
Truncated.Path.ext hᵥ hₐ

Premises used: SSet.Truncated.Path.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
⊢ f = g

Tactic:
Truncated.Path.ext' h

Premises used: SSet.Truncated.Path.ext'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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
hₐ : ∀ (i : Fin 0), f.arrow i = g.arrow i
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
hᵥ :
  f.vertex ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1))) =
    g.vertex ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)
⊢ f.vertex i = g.vertex i

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
⊢ f.vertex ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1))) =
    g.vertex ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)

Tactic:
h

Premises used: Fin.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
⊢ f.vertex ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1))) =
    g.vertex ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)

Tactic:
exact h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin 0
⊢ f.arrow i = g.arrow i

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
f : X.Path n
j l : ℕ
k' : Fin l
k : Fin n
h : j + l ≤ n
hkk' : j + (↑k' : ℕ) = (↑k : ℕ)
dsimp : f.arrow (⟨j + (↑k' : ℕ), ⋯⟩ : Fin n) = f.arrow k
⊢ (f.interval j l h).arrow k' = f.arrow k

Tactic:
dsimp [interval, arrow, Truncated.Path.interval, Truncated.Path.arrow]

Premises used: SSet.Truncated.Path.arrow, SSet.Path.arrow, SSet.Path.interval, SSet.Truncated.Path.interval
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
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.arrow (⟨j + (↑k' : ℕ), ⋯⟩ : Fin n) = f.arrow k

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X Y : SSet
n : ℕ
f : X.Path n
σ : X ⟶ Y
i : Fin (n + 1)
⊢ (f.map σ).vertex i =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (op ⦋0⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y _⦋0⦌))
      (f.vertex i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X Y : SSet
n : ℕ
f : X.Path n
σ : X ⟶ Y
i : Fin n
⊢ (f.map σ).arrow i =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
      (f.arrow i)

Tactic:
rfl

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

Tactic:
rfl

Premises used: SSet.Path.map, SSet.Truncated.Path.map, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
Δ : X _⦋n⦌
i : Fin (n + 1)
⊢ (X.spine n Δ).vertex i =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      Δ

Tactic:
rfl

Premises used: Quiver.Hom.op, SimplexCategory.const, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
Δ : X _⦋n⦌
i : Fin n
⊢ (X.spine n Δ).arrow i =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      Δ

Tactic:
rfl

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.mkOfSucc, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1⦌
zero :
  ∀ (x : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌),
    X.spine 0
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
          x) =
      (X.spine (HAdd.hAdd (α := ℕ) 0 1) x).interval 1 0 ⋯
succ :
  ∀ (m : ℕ) (x : X _⦋m + 1 + 1⦌),
    X.spine (m + 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m + 1⦌))
          x) =
      (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯
⊢ X.spine m
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) =
    (X.spine (m + 1) x).interval 1 m ⋯

Tactic:
obtain _ | m := m
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
x : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
zero :
  Path.vertex (n := 0)
      (X.spine 0
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
          x))
      0 =
    ((X.spine (HAdd.hAdd (α := ℕ) 0 1) x).interval 1 0 ⋯).vertex 0
⊢ X.spine 0
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        x) =
    (X.spine (HAdd.hAdd (α := ℕ) 0 1) x).interval 1 0 ⋯

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
x : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
zero :
  Eq (α := X _⦋0⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (X _⦋0⦌)) : (a : X _⦋0⦌) → X _⦋0⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) : (a : X _⦋1⦌) → X _⦋0⦌) x : X _⦋0⦌) :
      X _⦋0⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) : (a : X _⦋1⦌) → X _⦋0⦌) x : X _⦋0⦌)
⊢ Path.vertex (n := 0)
      (X.spine 0
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
          x))
      0 =
    ((X.spine (HAdd.hAdd (α := ℕ) 0 1) x).interval 1 0 ⋯).vertex 0

Tactic:
simp [spine, Path.vertex, Truncated.Path.vertex, SimplicialObject.truncation,
      Truncated.spine, Path.interval, Truncated.Path.interval, Truncated.inclusion,
      Truncated.Hom.tr, ← SimplexCategory.δ_zero_eq_const, ← SimplicialObject.δ_def]

Premises used: SimplexCategory.Truncated.Hom.tr, SSet.Truncated.spine, CategoryTheory.SimplicialObject.δ_def, SimplexCategory.δ_zero_eq_const, SimplexCategory.Truncated.inclusion, SSet.Path.interval, SSet.spine, CategoryTheory.SimplicialObject.truncation, SSet.Truncated.Path.interval, SSet.Path.vertex, SSet.Truncated.Path.vertex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
x : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
⊢ Eq (α := X _⦋0⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (X _⦋0⦌)) : (a : X _⦋0⦌) → X _⦋0⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) : (a : X _⦋1⦌) → X _⦋0⦌) x : X _⦋0⦌) :
      X _⦋0⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) : (a : X _⦋1⦌) → X _⦋0⦌) x : X _⦋0⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
succ :
  ∀ (i : Fin (m + 1)),
    Path.arrow
        (X.spine (m + 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m + 1⦌))
            x))
        i =
      ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
⊢ X.spine (m + 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m + 1⦌))
        x) =
    (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
succ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i).op) : (a : X _⦋m + 1⦌) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) : (a : X _⦋m + 1 + 1⦌) → X _⦋m + 1⦌) x :
        X _⦋m + 1⦌) =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
⊢ Path.arrow
      (X.spine (m + 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m + 1⦌))
          x))
      i =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ 0 < i.succ.castSucc

Tactic:
simp