awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
a :
  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))
⊢ 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)

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk]

Premises used: SSet.Truncated.StrictSegal.spineEquiv, Equiv.coe_fn_mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
a :
  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
⊢ 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))

Tactic:
rw [spine_spineToSimplex_apply]

Premises used: SSet.Truncated.StrictSegal.spine_spineToSimplex_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
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 : (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)) =
    (X.spine m h (sx.spineToSimplex m h f)).interval j l hjl

Tactic:
spine_map_subinterval X m h j l hjl <| sx.spineToSimplex m h f

Premises used: SSet.Truncated.spine_map_subinterval, SSet.Truncated.StrictSegal.spineToSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
h₁ : f = X.spine m h (sx.spineToSimplex m h f)
⊢ 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

Tactic:
convert! spine_map_subinterval X m h j l hjl <| sx.spineToSimplex m h f

Premises used: SSet.Truncated.spine_map_subinterval, SSet.Truncated.StrictSegal.spineToSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ f = X.spine m h (sx.spineToSimplex m h f)

Tactic:
sx.spine_spineToSimplex_apply m h f |>.symm

Premises used: SSet.Truncated.StrictSegal.spine_spineToSimplex_apply, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ f = X.spine m h (sx.spineToSimplex m h f)

Tactic:
exact sx.spine_spineToSimplex_apply m h f |>.symm

Premises used: SSet.Truncated.StrictSegal.spine_spineToSimplex_apply, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ l ≤ n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
a :
  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))
⊢ 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)

Tactic:
apply sy.spineInjective (m + 1)

Premises used: SSet.Truncated.StrictSegal.spineInjective, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
a :
  ∀ (k : Fin (m + 1)),
    Eq.{u + 1} (α :=
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
      (Path.arrow
        ((sy.spineEquiv (m + 1) ⋯ : (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.Path (m + 1))
          (sy.spineToSimplex (m + 1) ⋯ (f.map σ)))
        k)
      (Path.arrow
        ((sy.spineEquiv (m + 1) ⋯ : (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.Path (m + 1))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (σ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯))) :
                (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                  (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })))
              (sx.spineToSimplex (m + 1) ⋯ f) :
            (fun (X : Type u) ↦ X)
              (Y.obj
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯)))))
        k)
⊢ 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))

Tactic:
ext k
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
a :
  Eq (α := Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯))) :
          (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯))) :
          (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯))) :
              (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))
            (sx.spineToSimplex (m + 1) ⋯ f) :
          Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯))) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
⊢ Eq.{u + 1} (α :=
    Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    (Path.arrow
      ((sy.spineEquiv (m + 1) ⋯ : (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.Path (m + 1))
        (sy.spineToSimplex (m + 1) ⋯ (f.map σ)))
      k)
    (Path.arrow
      ((sy.spineEquiv (m + 1) ⋯ : (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.Path (m + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f) :
          (fun (X : Type u) ↦ X)
            (Y.obj
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯)))))
      k)

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]

Premises used: SSet.Truncated.spine_arrow, SSet.Truncated.StrictSegal.spineEquiv, Equiv.coe_fn_mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
a :
  Eq (α := Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯))) :
          (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯)) ≫
              σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋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) ⦋1⦌ ⋯))))
⊢ Eq (α := Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯))) :
          (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯))) :
          (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (σ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯))) :
              (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))
            (sx.spineToSimplex (m + 1) ⋯ f) :
          Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ ⋯))) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))

Tactic:
rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality]

Premises used: CategoryTheory.Functor.map, CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.app, CategoryTheory.types_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
⊢ Eq (α := Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯))) :
          (a : Y.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → Y.obj (op { obj := ⦋1⦌, property := ⋯ }))
        (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) :
      Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map (Quiver.Hom.op (tr (mkOfSucc k) ⋯ ⋯)) ≫
              σ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋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) ⦋1⦌ ⋯))))

Tactic:
simp [-NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
rw :
  f.vertex ((Hom.toOrderHom (SimplexCategory.δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1)) i) =
    f.vertex i.castSucc
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).vertex
      i =
    f.vertex i.castSucc

Tactic:
rw [spine_vertex, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    SimplexCategory.const_comp, spineToSimplex_vertex]

Premises used: CategoryTheory.op_comp, SimplexCategory.const_comp, SimplexCategory.Truncated.Hom.tr_comp, CategoryTheory.Functor.map_comp_apply, SSet.Truncated.StrictSegal.spineToSimplex_vertex, SSet.Truncated.spine_vertex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
dsimp : f.vertex (j.succAbove i) = f.vertex i.castSucc
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1)) i) =
    f.vertex i.castSucc

Tactic:
dsimp only [SimplexCategory.δ, len_mk, mkHom, Hom.toOrderHom_mk,
    Fin.succAboveOrderEmb_apply, OrderEmbedding.toOrderHom_coe]

Premises used: SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe, SimplexCategory.mkHom, SimplexCategory.δ, SimplexCategory.Hom.toOrderHom_mk, Fin.succAboveOrderEmb_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
rw rw₁ : f.vertex i.castSucc = f.vertex i.castSucc
⊢ f.vertex (j.succAbove i) = f.vertex i.castSucc

Tactic:
rw [Fin.succAbove_of_castSucc_lt j i hij]

Premises used: Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
rw :
  f.vertex ((Hom.toOrderHom (SimplexCategory.δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1)) i) =
    f.vertex i.succ
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).vertex
      i =
    f.vertex i.succ

Tactic:
rw [spine_vertex, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    SimplexCategory.const_comp, spineToSimplex_vertex]

Premises used: CategoryTheory.op_comp, SimplexCategory.const_comp, SimplexCategory.Truncated.Hom.tr_comp, CategoryTheory.Functor.map_comp_apply, SSet.Truncated.StrictSegal.spineToSimplex_vertex, SSet.Truncated.spine_vertex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
dsimp : f.vertex (j.succAbove i) = f.vertex i.succ
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1)) i) =
    f.vertex i.succ

Tactic:
dsimp only [SimplexCategory.δ, len_mk, mkHom, Hom.toOrderHom_mk,
    Fin.succAboveOrderEmb_apply, OrderEmbedding.toOrderHom_coe]

Premises used: SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe, SimplexCategory.mkHom, SimplexCategory.δ, SimplexCategory.Hom.toOrderHom_mk, Fin.succAboveOrderEmb_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
rw rw₁ : f.vertex i.succ = f.vertex i.succ
⊢ f.vertex (j.succAbove i) = f.vertex i.succ

Tactic:
rw [Fin.succAbove_of_le_castSucc j i hij]

Premises used: Fin.succAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
          (sx.spineToSimplex (m + 1) ⋯ f) :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ ⋯)))) =
    f.arrow i.castSucc
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯) ≫ Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.castSucc
rw₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.castSucc
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i ≫ SimplexCategory.δ j) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.castSucc
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i.castSucc) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.castSucc
rw₅ rw₆ : f.arrow i.castSucc = f.arrow i.castSucc
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ j) ⋯ ⋯))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m + 1⦌, property := ⋯ }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := ⋯ })))
            (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.castSucc

Tactic:
rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_lt hij, spineToSimplex_arrow]

Premises used: CategoryTheory.op_comp, SimplexCategory.Truncated.Hom.tr_comp, SimplexCategory.mkOfSucc_δ_lt, CategoryTheory.Functor.map_comp_apply, SSet.Truncated.spine_arrow, SSet.Truncated.StrictSegal.spineToSimplex_arrow