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
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
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.succ
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.succ
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.succ
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.succ
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i.succ) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
rw₅ rw₆ : f.arrow i.succ = f.arrow 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))).arrow
      i =
    f.arrow i.succ

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

Premises used: CategoryTheory.op_comp, SimplexCategory.Truncated.Hom.tr_comp, CategoryTheory.Functor.map_comp_apply, SSet.Truncated.spine_arrow, SSet.Truncated.StrictSegal.spineToSimplex_arrow, SimplexCategory.mkOfSucc_δ_gt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X_1 : Truncated (n + 1)
sx_1 : X_1.StrictSegal
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ 2 ≤ n + 1 + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X_1 : Truncated (n + 1)
sx_1 : X_1.StrictSegal
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (↑i : ℕ) + 2 ≤ m + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
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 + 2) ⦋m⦌ ⋯)))) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
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) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
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) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
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) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (intervalEdge (↑i : ℕ) 2 ⋯) ⋯ ⋯))) :
        (a : X.obj (op { obj := ⦋m + 1⦌, property := ⋯ })) → X.obj (op { obj := ⦋1⦌, property := ⋯ }))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
rw₅ rw₆ : sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯) = sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)
⊢ (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 =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i : ℕ) 2 ⋯)

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

Premises used: CategoryTheory.op_comp, SimplexCategory.Truncated.Hom.tr_comp, CategoryTheory.Functor.map_comp_apply, SSet.Truncated.StrictSegal.spineToSimplex_edge, SSet.Truncated.spine_arrow, SimplexCategory.mkOfSucc_δ_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
inst : X.IsStrictSegal
n : ℕ
⊢ Truncated.IsStrictSegal (n := n) (Functor.obj (truncation (n + 1)) X)

Tactic:
((ofIsStrictSegal X).truncation n).isStrictSegal

Premises used: SSet.Truncated.StrictSegal.isStrictSegal, SSet.StrictSegal.ofIsStrictSegal, SSet.StrictSegal.truncation
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
⊢ X.spine n (sx.spineToSimplex f) = f

Tactic:
congr_fun (sx.spine_spineToSimplex n) f

Premises used: SSet.Truncated.spine, SSet.StrictSegal.spine_spineToSimplex, congr_fun, SSet.spine
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
Δ : X _⦋n⦌
⊢ sx.spineToSimplex (X.spine n Δ) = Δ

Tactic:
congr_fun (sx.spineToSimplex_spine n) Δ

Premises used: SSet.StrictSegal.spineToSimplex_spine, congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
⊢ Function.Injective (α := X _⦋n⦌) (β := X.Path n) (⇑(sx.spineEquiv n) : (a : X _⦋n⦌) → X.Path n)

Tactic:
Equiv.injective _

Premises used: Equiv.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1)
f : X.Path n
rw : (X.spine n (sx.spineToSimplex f)).vertex i = f.vertex i
rw₁ rw₂ : f.vertex i = f.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⦌))
      (sx.spineToSimplex f) =
    f.vertex i

Tactic:
rw [← spine_vertex, spine_spineToSimplex_apply]

Premises used: SSet.spine_vertex, SSet.StrictSegal.spine_spineToSimplex_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin n
f : X.Path n
rw : (X.spine n (sx.spineToSimplex f)).arrow i = f.arrow i
rw₁ rw₂ : f.arrow i = f.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⦌))
      (sx.spineToSimplex f) =
    f.arrow i

Tactic:
rw [← spine_arrow, spine_spineToSimplex_apply]

Premises used: SSet.spine_arrow, SSet.StrictSegal.spine_spineToSimplex_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
a :
  Eq (α := X.Path l)
    ((sx.spineEquiv l : (a : X _⦋l⦌) → X.Path l)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (subinterval j l hjl).op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋l⦌))
            (sx.spineToSimplex f) :
          (fun (X : Type u) ↦ X) (X _⦋l⦌)) :
      X.Path l)
    ((sx.spineEquiv l : (a : X _⦋l⦌) → X.Path l) (sx.spineToSimplex (f.interval j l hjl)) : X.Path l)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (subinterval j l hjl).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋l⦌))
      (sx.spineToSimplex f) =
    sx.spineToSimplex (f.interval j l hjl)

Tactic:
apply sx.spineInjective

Premises used: SSet.StrictSegal.spineInjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
a :
  X.spine l
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (subinterval j l hjl).op) : (a : X _⦋n⦌) → X _⦋l⦌)
        (sx.spineToSimplex f)) =
    X.spine l (sx.spineToSimplex (f.interval j l hjl))
⊢ Eq (α := X.Path l)
    ((sx.spineEquiv l : (a : X _⦋l⦌) → X.Path l)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (subinterval j l hjl).op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋l⦌))
            (sx.spineToSimplex f) :
          (fun (X : Type u) ↦ X) (X _⦋l⦌)) :
      X.Path l)
    ((sx.spineEquiv l : (a : X _⦋l⦌) → X.Path l) (sx.spineToSimplex (f.interval j l hjl)) : X.Path l)

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk]

Premises used: Equiv.coe_fn_mk, SSet.StrictSegal.spineEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
a :
  X.spine l
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (subinterval j l hjl).op) : (a : X _⦋n⦌) → X _⦋l⦌)
        (sx.spineToSimplex f)) =
    f.interval j l hjl
a₁ : (X.spine n (sx.spineToSimplex f)).interval j l hjl = f.interval j l hjl
a₂ a₃ : f.interval j l hjl = f.interval j l hjl
⊢ X.spine l
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (subinterval j l hjl).op) : (a : X _⦋n⦌) → X _⦋l⦌)
        (sx.spineToSimplex f)) =
    X.spine l (sx.spineToSimplex (f.interval j l hjl))

Tactic:
rw [spine_spineToSimplex_apply, spine_map_subinterval,
    spine_spineToSimplex_apply]

Premises used: SSet.spine_map_subinterval, SSet.StrictSegal.spine_spineToSimplex_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
dsimp :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (intervalEdge j l hjl).op) : (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex f) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (diag l).op) : (a : X _⦋l⦌) → X _⦋1⦌)
        (sx.spineToSimplex (f.interval j l hjl)) :
      X _⦋1⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (intervalEdge j l hjl).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval j l hjl)

Tactic:
dsimp only [spineToDiagonal, SimplicialObject.diagonal]

Premises used: SSet.StrictSegal.spineToDiagonal, CategoryTheory.SimplicialObject.diagonal
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
rw :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (intervalEdge j l hjl).op) : (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex f) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (diag l).op) : (a : X _⦋l⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (subinterval j l hjl).op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋l⦌))
            (sx.spineToSimplex f) :
          (fun (X : Type u) ↦ X) (X _⦋l⦌)) :
      X _⦋1⦌)
rw₁ :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (intervalEdge j l hjl).op) : (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex f) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((subinterval j l hjl).op ≫ (diag l).op)) : (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex f) :
      X _⦋1⦌)
rw₂ :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (intervalEdge j l hjl).op) : (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex f) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (diag l ≫ subinterval j l hjl).op) : (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex f) :
      X _⦋1⦌)
rw₃ rw₄ :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (intervalEdge j l hjl).op) : (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex f) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (intervalEdge j l hjl).op) : (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex f) :
      X _⦋1⦌)
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (intervalEdge j l hjl).op) : (a : X _⦋n⦌) → X _⦋1⦌)
        (sx.spineToSimplex f) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (diag l).op) : (a : X _⦋l⦌) → X _⦋1⦌)
        (sx.spineToSimplex (f.interval j l hjl)) :
      X _⦋1⦌)

Tactic:
rw [← spineToSimplex_interval, ← Functor.map_comp_apply, ← op_comp,
    diag_subinterval_eq]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply, SSet.StrictSegal.spineToSimplex_interval, SimplexCategory.diag_subinterval_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
a :
  Eq (α := Y.Path (n + 1))
    ((sy.spineEquiv (n + 1) : (a : Y _⦋n + 1⦌) → Y.Path (n + 1)) (sy.spineToSimplex (f.map σ)) : Y.Path (n + 1))
    ((sy.spineEquiv (n + 1) : (a : Y _⦋n + 1⦌) → Y.Path (n + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋n + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
            (sx.spineToSimplex f) :
          (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌)) :
      Y.Path (n + 1))
⊢ sy.spineToSimplex (f.map σ) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋n + 1⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
      (sx.spineToSimplex f)

Tactic:
apply sy.spineInjective

Premises used: SSet.StrictSegal.spineInjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
a :
  ∀ (k : Fin (n + 1)),
    Eq.{u + 1} (α := Y _⦋1⦌)
      (Path.arrow ((sy.spineEquiv (n + 1) : (a : Y _⦋n + 1⦌) → Y.Path (n + 1)) (sy.spineToSimplex (f.map σ))) k)
      (Path.arrow
        ((sy.spineEquiv (n + 1) : (a : Y _⦋n + 1⦌) → Y.Path (n + 1))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
              (sx.spineToSimplex f) :
            (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌)))
        k)
⊢ Eq (α := Y.Path (n + 1))
    ((sy.spineEquiv (n + 1) : (a : Y _⦋n + 1⦌) → Y.Path (n + 1)) (sy.spineToSimplex (f.map σ)) : Y.Path (n + 1))
    ((sy.spineEquiv (n + 1) : (a : Y _⦋n + 1⦌) → Y.Path (n + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋n + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
            (sx.spineToSimplex f) :
          (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌)) :
      Y.Path (n + 1))

Tactic:
ext k
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
a :
  Eq (α := Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (mkOfSucc k).op) : (a : Y _⦋n + 1⦌) → Y _⦋1⦌)
        (sy.spineToSimplex (f.map σ)) :
      Y _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (mkOfSucc k).op) : (a : Y _⦋n + 1⦌) → Y _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋n + 1⦌)) : (a : X _⦋n + 1⦌) → Y _⦋n + 1⦌)
            (sx.spineToSimplex f) :
          Y _⦋n + 1⦌) :
      Y _⦋1⦌)
⊢ Eq.{u + 1} (α := Y _⦋1⦌)
    (Path.arrow ((sy.spineEquiv (n + 1) : (a : Y _⦋n + 1⦌) → Y.Path (n + 1)) (sy.spineToSimplex (f.map σ))) k)
    (Path.arrow
      ((sy.spineEquiv (n + 1) : (a : Y _⦋n + 1⦌) → Y.Path (n + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋n + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
            (sx.spineToSimplex f) :
          (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌)))
      k)

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

Premises used: SSet.spine_arrow, Equiv.coe_fn_mk, SSet.StrictSegal.spineEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
simp :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i))) : (a : X _⦋n⦌) → X _⦋0⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    f.vertex i.castSucc
⊢ (X.spine n
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            (sx.spineToSimplex f))).vertex
      i =
    f.vertex i.castSucc

Tactic:
simp only [SimplicialObject.δ, spine_vertex]

Premises used: SSet.spine_vertex, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
rw : f.vertex ((Hom.toOrderHom (δ j) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) i) = f.vertex i.castSucc
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i))) : (a : X _⦋n⦌) → X _⦋0⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    f.vertex i.castSucc

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

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

Tactic:
simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk,
    OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply]

Premises used: SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe, SimplexCategory.mkHom, SimplexCategory.δ, SimplexCategory.Hom.toOrderHom, Fin.succAboveOrderEmb_apply, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : 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 h]

Premises used: Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
simp :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i))) : (a : X _⦋n⦌) → X _⦋0⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    f.vertex i.succ
⊢ (X.spine n
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            (sx.spineToSimplex f))).vertex
      i =
    f.vertex i.succ

Tactic:
simp only [SimplicialObject.δ, spine_vertex]

Premises used: SSet.spine_vertex, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
rw : f.vertex ((Hom.toOrderHom (δ j) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) i) = f.vertex i.succ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i))) : (a : X _⦋n⦌) → X _⦋0⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    f.vertex i.succ

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

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

Tactic:
simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk,
    OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply]

Premises used: SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe, SimplexCategory.mkHom, SimplexCategory.δ, SimplexCategory.Hom.toOrderHom, Fin.succAboveOrderEmb_apply, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : 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 h]

Premises used: Fin.succAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
simp :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i).op) : (a : X _⦋n⦌) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ j).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) (sx.spineToSimplex f) :
        X _⦋n⦌) =
    f.arrow i.castSucc
⊢ (X.spine n
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            (sx.spineToSimplex f))).arrow
      i =
    f.arrow i.castSucc

Tactic:
simp only [SimplicialObject.δ, spine_arrow]

Premises used: SSet.spine_arrow, CategoryTheory.SimplicialObject.δ