awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⦌))
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⦌))
⊢ 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 ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (sx.spineToSimplex f) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌)) :
    (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⦌))
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⦌))
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 ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
            (sx.spineToSimplex f) :
          (fun (X : Type u) ↦ X) (X _⦋1⦌)) :
      (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₃ : (f.map σ).arrow k =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋1⦌)) :
      (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (sx.spineToSimplex f) :
      (fun (X : Type u) ↦ X) (X _⦋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⦌))
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⦌))
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 ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
            (sx.spineToSimplex f) :
          (fun (X : Type u) ↦ X) (X _⦋1⦌)) :
      (fun (X : Type u) ↦ X) (Y _⦋1⦌))
a₃ :
  (f.map σ).arrow k =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (sx.spineToSimplex f) :
        (fun (X : Type u) ↦ X) (X _⦋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₄ : (f.map σ).arrow k =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app (Opposite.op ⦋1⦌)) :
      (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
    (f.arrow k)
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 : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ (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
have 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
Tactic: simp only [SimplicialObject.δ, spine_vertex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ (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
have rw : f.vertex ((Hom.toOrderHom (δ j) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) i) = f.vertex i.castSucc
Tactic: rw [← Functor.map_comp_apply, ← op_comp, SimplexCategory.const_comp,
    spineToSimplex_vertex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ f.vertex ((Hom.toOrderHom (δ j) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) i) = f.vertex i.castSucc
have simp : f.vertex (j.succAbove i) = f.vertex i.castSucc
Tactic: simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk,
    OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ f.vertex (j.succAbove i) = f.vertex i.castSucc
have rw : f.vertex i.castSucc = f.vertex i.castSucc
Tactic: rw [Fin.succAbove_of_castSucc_lt j i h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ 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.succ
have 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
Tactic: simp only [SimplicialObject.δ, spine_vertex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ 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.succ
have rw : f.vertex ((Hom.toOrderHom (δ j) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) i) = f.vertex i.succ
Tactic: rw [← Functor.map_comp_apply, ← op_comp, SimplexCategory.const_comp,
    spineToSimplex_vertex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ f.vertex ((Hom.toOrderHom (δ j) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) i) = f.vertex i.succ
have simp : f.vertex (j.succAbove i) = f.vertex i.succ
Tactic: simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk,
    OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ f.vertex (j.succAbove i) = f.vertex i.succ
have rw : f.vertex i.succ = f.vertex i.succ
Tactic: rw [Fin.succAbove_of_le_castSucc j i h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (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
have 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
Tactic: simp only [SimplicialObject.δ, spine_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (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
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
    (sx.spineToSimplex f) =
  f.arrow i.castSucc
Tactic: rw [← Functor.map_comp_apply, ← op_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.castSucc
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.castSucc).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
    (sx.spineToSimplex f) =
  f.arrow i.castSucc
Tactic: rw [mkOfSucc_δ_lt h, spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.castSucc).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.castSucc
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.castSucc
have rw₁ : f.arrow i.castSucc = f.arrow i.castSucc
Tactic: rw [mkOfSucc_δ_lt h, spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.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.succ
have 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.succ
Tactic: simp only [SimplicialObject.δ, spine_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (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.succ
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
    (sx.spineToSimplex f) =
  f.arrow i.succ
Tactic: rw [← Functor.map_comp_apply, ← op_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.succ
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.succ).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
    (sx.spineToSimplex f) =
  f.arrow i.succ
Tactic: rw [mkOfSucc_δ_gt h, spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.succ).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.succ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    f.arrow i.succ
have rw₁ : f.arrow i.succ = f.arrow i.succ
Tactic: rw [mkOfSucc_δ_gt h, spineToSimplex_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.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 =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)
have 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⦌) =
  sx.spineToDiagonal (f.interval (↑i : ℕ) 2 sorry)
Tactic: simp only [SimplicialObject.δ, spine_arrow]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (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⦌) =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
    (sx.spineToSimplex f) =
  sx.spineToDiagonal (f.interval (↑i : ℕ) 2 sorry)
Tactic: rw [← Functor.map_comp_apply, ← op_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (intervalEdge (↑i : ℕ) 2 sorry))) :
      (a : X _⦋n + 1⦌) → X _⦋1⦌)
    (sx.spineToSimplex f) =
  sx.spineToDiagonal (f.interval (↑i : ℕ) 2 sorry)
Tactic: rw [mkOfSucc_δ_eq h, spineToSimplex_edge]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (intervalEdge (↑i : ℕ) 2 ⋯))) :
        (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i ≫ δ j).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
      (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval (↑i : ℕ) 2 ⋯)
have rw₁ : sx.spineToDiagonal (f.interval (↑i : ℕ) 2 sorry) = sx.spineToDiagonal (f.interval (↑i : ℕ) 2 sorry)
Tactic: rw [mkOfSucc_δ_eq h, spineToSimplex_edge]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
⊢ { s : X _⦋n + 1⦌ // X.spine (n + 1) s = p }
have succ : Eq (α := (fun (X : Type u) ↦ X) (X _⦋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⦌))
      (p.arrow 0) :
    (fun (X : Type u) ↦ X) (X _⦋0⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (↑(hn (p.interval 1 n sorry)) : X _⦋n⦌) :
    (fun (X : Type u) ↦ X) (X _⦋0⦌))
Tactic: refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
succ :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋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⦌))
        (p.arrow 0) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
⊢ { s : X _⦋n + 1⦌ // X.spine (n + 1) s = p }
have succ₁ : X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n sorry)) : X _⦋n⦌) sorry) = p
Tactic: refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋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⦌))
        (p.arrow 0) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) :
      (fun (X : Type u) ↦ X) (X _⦋0⦌))
have succ : p.vertex (Fin.succ 0) =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ 0))) :
      (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
    (↑(hn (p.interval 1 n sorry)) : X _⦋n⦌)
Tactic: rw [p.arrow_tgt 0]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
⊢ X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯) = p
have succ : ∀ (i : Fin (n + 1)),
  (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n sorry)) : X _⦋n⦌) sorry)).arrow i = p.arrow i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal (goal)
Goal:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s : X _⦋n⦌ // X.spine n s = p }
p : X.Path (n + 1)
i : Fin (n + 1)
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n ⋯)) : X _⦋n⦌) ⋯)).arrow i = p.arrow i
have succ : (X.spine (n + 1) ((h n).concat (p.arrow 0) (↑(hn (p.interval 1 n sorry)) : X _⦋n⦌) sorry)).arrow 0 = p.arrow 0
Tactic: obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ
Cleared hypotheses: i