-- 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 : ℕ
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⦌)
h :
  ∀ (k : Fin (i + 1)),
    Eq.{u + 1} (α := X _⦋0⦌)
      (Path.vertex
        ((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 ⋯).op)) :
                        (a : s.pt) → X _⦋1⦌)
                      x,
                  arrow_src := ⋯, arrow_tgt := ⋯ }) :
            X _⦋i⦌))
        k)
      (Path.vertex
        ((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⦌))
        k)
h₁ :
  ∀ (k : Fin i),
    Eq.{u + 1} (α := X _⦋1⦌)
      (Path.arrow
        ((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 ⋯).op)) :
                        (a : s.pt) → X _⦋1⦌)
                      x,
                  arrow_src := ⋯, arrow_tgt := ⋯ }) :
            X _⦋i⦌))
        k)
      (Path.arrow
        ((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⦌))
        k)
⊢ 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 ⋯).op)) :
                      (a : s.pt) → X _⦋1⦌)
                    x,
                arrow_src := ⋯, arrow_tgt := ⋯ }) :
          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:
ext k