-- 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⦌)
⊢ Eq (α := X _⦋i⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (op f)) : (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 := ⋯ }) :
      X _⦋i⦌)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (s.π.app (StructuredArrow.mk (op f))) :
            TypeCat.Fun s.pt (X _⦋i⦌)) :
          (a : s.pt) → X _⦋i⦌)
        x :
      X _⦋i⦌)
have h : Eq (α := X.Path i)
  ((sx.spineEquiv i : (a : X _⦋i⦌) → X.Path i)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (op f)) : (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 sorry).op)) :
                    (a : s.pt) → X _⦋1⦌)
                  x,
              arrow_src := sorry, arrow_tgt := sorry }) :
        X _⦋i⦌) :
    X.Path i)
  ((sx.spineEquiv i : (a : X _⦋i⦌) → X.Path i)
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (s.π.app (StructuredArrow.mk (op f))) :
              TypeCat.Fun s.pt (X _⦋i⦌)) :
            (a : s.pt) → X _⦋i⦌)
          x :
        X _⦋i⦌) :
    X.Path i)
Tactic: apply sx.spineInjective