-- 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)
m :
  s.pt ⟶
    Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))
hm :
  ∀ (j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))),
    m ≫ NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))) j = s.π.app j
x : s.pt
h :
  ∀ (i : Fin (n + 1)),
    (X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x)).vertex i =
      Path.vertex
        {
          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 := ⋯ }
        i
h₁ :
  ∀ (i : Fin n),
    (X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x)).arrow i =
      Path.arrow
        {
          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 := ⋯ }
        i
⊢ X.spine n ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : s.pt) → X _⦋n⦌) x) =
    {
      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 := ⋯ }

Tactic:
ext i