awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
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 ⋯)
⊢ (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 ⋯)
have rw₅ : sx.spineToDiagonal 2 sorry (f.interval (↑i : ℕ) 2 sorry) = sx.spineToDiagonal 2 sorry (f.interval (↑i : ℕ) 2 sorry)
Tactic: rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_eq hij, spineToSimplex_edge]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1)
f : X.Path n
⊢ (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
have rw : (X.spine n (sx.spineToSimplex f)).vertex i = f.vertex i
Tactic: rw [← spine_vertex, spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
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
⊢ (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
have rw₁ : f.vertex i = f.vertex i
Tactic: rw [← spine_vertex, spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin n
f : X.Path n
⊢ (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
have rw : (X.spine n (sx.spineToSimplex f)).arrow i = f.arrow i
Tactic: rw [← spine_arrow, spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
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
⊢ (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
have rw₁ : f.arrow i = f.arrow i
Tactic: rw [← spine_arrow, spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (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)
have 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)
Tactic: apply sx.spineInjective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ 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)
have 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))
Tactic: dsimp only [spineEquiv, Equiv.coe_fn_mk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ 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))
have 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
Tactic: rw [spine_spineToSimplex_apply, spine_map_subinterval,
    spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
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
⊢ 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))
have a₁ : (X.spine n (sx.spineToSimplex f)).interval j l hjl = f.interval j l hjl
Tactic: rw [spine_spineToSimplex_apply, spine_map_subinterval,
    spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
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
⊢ 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))
have a₂ : f.interval j l hjl = f.interval j l hjl
Tactic: rw [spine_spineToSimplex_apply, spine_map_subinterval,
    spine_spineToSimplex_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (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)
have 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⦌)
Tactic: dsimp only [spineToDiagonal, SimplicialObject.diagonal]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ 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⦌)
have 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⦌)
Tactic: rw [← spineToSimplex_interval, ← Functor.map_comp_apply, ← op_comp,
    diag_subinterval_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
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⦌)
⊢ 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⦌)
have 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⦌)
Tactic: rw [← spineToSimplex_interval, ← Functor.map_comp_apply, ← op_comp,
    diag_subinterval_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
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⦌)
⊢ 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⦌)
have 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⦌)
Tactic: rw [← spineToSimplex_interval, ← Functor.map_comp_apply, ← op_comp,
    diag_subinterval_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
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⦌)
⊢ 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⦌)
have 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⦌)
Tactic: rw [← spineToSimplex_interval, ← Functor.map_comp_apply, ← op_comp,
    diag_subinterval_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ 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)
have 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))
Tactic: apply sy.spineInjective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ 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))
have 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)
Tactic: ext k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
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)
have 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⦌)
Tactic: dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ 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⦌)
have 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) (σ.app (Opposite.op ⦋n + 1⦌) ≫ Y.map (mkOfSucc k).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
      (sx.spineToSimplex f) :
    (fun (X : Type u) ↦ X) (Y _⦋1⦌))
Tactic: rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality, types_comp_apply,
    spineToSimplex_arrow, spineToSimplex_arrow, Path.map_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
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) (σ.app (Opposite.op ⦋n + 1⦌) ≫ Y.map (mkOfSucc k).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
        (sx.spineToSimplex f) :
      (fun (X : Type u) ↦ X) (Y _⦋1⦌))
⊢ 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⦌)
have 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) (X.map (mkOfSucc k).op ≫ σ.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
      (sx.spineToSimplex f) :
    (fun (X : Type u) ↦ X) (Y _⦋1⦌))
Tactic: rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality, types_comp_apply,
    spineToSimplex_arrow, spineToSimplex_arrow, Path.map_arrow]