-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
s :
  Cone (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
    (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this :
  mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i, ⋯⟩ : Fin (n + 1)) ⋯ =
    CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (⦋n⦌.len + 1))) lift._proof_1 ⟶
  strArrowMk₂ (CategoryStruct.comp (Y := ⦋0⦌) (⦋1⦌.const ⦋0⦌ 0) (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ (⟨i, ⋯⟩ : Fin (n + 1))))) :
          (a : X _⦋n⦌) → X _⦋0⦌)
        (lift sx s x) :
      X _⦋0⦌)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (s.π.app
              (StructuredArrow.mk (Y :=
                op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ lift._proof_1))
                (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)))) :
          (a : s.pt) → X _⦋0⦌)
        x :
      X _⦋0⦌)
have zero : Eq.{u + 1} (α := (fun (X : Type u) ↦ X) (X _⦋0⦌))
  (Path.vertex
    {
      vertex := fun (i : Fin (n + 1)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (s.π.app
                (StructuredArrow.mk (Y :=
                  op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ lift._proof_2))
                  (Quiver.Hom.op
                    ((obj (C := SimplexCategory.Truncated 2) (inclusion 2)
                          (unop
                            (op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                lift._proof_2)))).const
                      ⦋n⦌ i)))) :
            (a :
                (fun (X : Type u) ↦ X)
                  (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                    (StructuredArrow.mk
                      (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i).op))) →
              (fun (X : Type u) ↦ X)
                ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                  (StructuredArrow.mk
                    (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i).op)))
          x,
      arrow := fun (i : Fin n) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ sorry).op)) :
            (a :
                (fun (X : Type u) ↦ X)
                  (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                    (StructuredArrow.mk (mkOfLe i.castSucc i.succ sorry).op))) →
              (fun (X : Type u) ↦ X)
                ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                  (StructuredArrow.mk (mkOfLe i.castSucc i.succ sorry).op)))
          x,
      arrow_src := sorry, arrow_tgt := sorry }
    (⟨i, sorry⟩ : Fin (n + 1)))
  ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (s.π.app
          (StructuredArrow.mk (Y :=
            op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ lift._proof_1))
            (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ⟨i, sorry⟩)))) :
      (a : s.pt) → X _⦋0⦌)
    x)
Tactic: rw [lift, StrictSegal.spineToSimplex_vertex]