-- 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 : ℕ
hi : i ≤ 2
f :
  unop
      (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.op (inclusion 2))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))) ⟶
    unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ (X.spine i
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋n⦌) → X _⦋i⦌)
            (sx.spineToSimplex
              {
                vertex := fun (i : 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_2))
                            (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i)))) :
                      (a : s.pt) → X _⦋0⦌)
                    x,
                arrow := fun (i : Fin n) ↦
                  (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                        (s.π.app
                          (StructuredArrow.mk (Y :=
                            op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                                lift._proof_4))
                            (mkOfLe i.castSucc i.succ ⋯).op)) :
                      (a : s.pt) → X _⦋1⦌)
                    x,
                arrow_src := ⋯, arrow_tgt := ⋯ :
                ((trunc 1 1 lift._proof_8).obj (obj (truncation 1) X)).Path₁ n }))).vertex
      k =
    (X.spine i
          (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (s.π.app
                    (StructuredArrow.mk (Y :=
                      op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi))
                      f.op)) :
                TypeCat.Fun s.pt (X _⦋i⦌)) :
              (a : s.pt) → X _⦋i⦌)
            x)).vertex
      k
have h : Eq.{u + 1} (α := X _⦋0⦌)
  (Path.vertex (n := n)
    {
      vertex := fun (i : 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_2))
                  (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ i)))) :
            (a : s.pt) → X _⦋0⦌)
          x,
      arrow := fun (i : Fin n) ↦
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (s.π.app
                (StructuredArrow.mk (Y :=
                  op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ lift._proof_4))
                  (mkOfLe i.castSucc i.succ sorry).op)) :
            (a : s.pt) → X _⦋1⦌)
          x,
      arrow_src := sorry, arrow_tgt := sorry }
    ((Hom.toOrderHom f : (a : Fin (⦋i⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (⦋0⦌.const ⦋i⦌ k))) :
      (a : (fun (X : Type u) ↦ X) (X _⦋i⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (s.π.app
                (StructuredArrow.mk (Y :=
                  op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋i⦌ hi)) f.op)) :
            TypeCat.Fun s.pt (X _⦋i⦌)) :
          (a : s.pt) → X _⦋i⦌)
        x :
      X _⦋i⦌))
Tactic: rw [spine_map_vertex, spine_spineToSimplex_apply, spine_vertex]