-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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 ⋯
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 ⋯).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 ⋯).op))) →
                (fun (X : Type u) ↦ X)
                  ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                    (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op)))
            x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      (⟨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_1))
              (Quiver.Hom.op (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)))) :
        (a : s.pt) → X _⦋0⦌)
      x)
⊢ 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⦌)

Tactic:
rw [lift, StrictSegal.spineToSimplex_vertex]

Premises used: SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift, SSet.StrictSegal.spineToSimplex_vertex