-- 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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n) (hk : i + k = j),
    Eq (α := (fun (X : Type u) ↦ X) (X _⦋1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨j, ⋯⟩ : Fin (n + 1)) hij).op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (lift sx s x) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (s.π.app (strArrowMk₂ (mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨j, ⋯⟩ : Fin (n + 1)) hij) fac_aux₁._proof_1)) :
            (a :
                (fun (X : Type u) ↦ X)
                  (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                    (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) →
              (fun (X : Type u) ↦ X)
                ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                  (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1)))
          x :
        (fun (X : Type u) ↦ X)
          (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X)
            (strArrowMk₂ (mkOfLe (⟨i, ⋯⟩ : Fin (n + 1)) (⟨j, ⋯⟩ : Fin (n + 1)) hij) fac_aux₁._proof_1)))
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_11
α₀ : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)) :=
  strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯)) ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ :
  Eq (α := (fun (X : Type u) ↦ X) (X.obj (obj (Functor.op (inclusion 2)) α₀.right)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α₀.hom) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X.obj ((inclusion 2).op.obj α₀.right)))
        (lift sx s x) :
      (fun (X : Type u) ↦ X) (X.obj (obj (Functor.op (inclusion 2)) α₀.right)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app α₀) :
          (a : (fun (X : Type u) ↦ X) (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj α₀)) →
            (fun (X : Type u) ↦ X) ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj α₀))
        x :
      (fun (X : Type u) ↦ X) (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) α₀))
h₂ :
  Eq (α := (fun (X : Type u) ↦ X) (X.obj (obj (Functor.op (inclusion 2)) α₂.right)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α₂.hom) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X.obj ((inclusion 2).op.obj α₂.right)))
        (lift sx s x) :
      (fun (X : Type u) ↦ X) (X.obj (obj (Functor.op (inclusion 2)) α₂.right)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app α₂) :
          (a : (fun (X : Type u) ↦ X) (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj α₂)) →
            (fun (X : Type u) ↦ X) ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj α₂))
        x :
      (fun (X : Type u) ↦ X) (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) α₂))
t : Fin (HAdd.hAdd (α := ℕ) 1 1)
a :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc t).op) : (a : X _⦋2⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map
                  (Quiver.Hom.op
                    (mkOfLeComp (⟨i, ⋯⟩ : Fin (n + 1)) (⟨i + k, ⋯⟩ : Fin (n + 1)) (⟨j, ⋯⟩ : Fin (n + 1)) ⋯ ⋯))) :
              (a : X _⦋n⦌) → X _⦋2⦌)
            (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 _⦋2⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc t).op) : (a : X _⦋2⦌) → X _⦋1⦌)
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (s.π.app (strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_11)) :
              (a : s.pt) → X _⦋2⦌)
            x :
          X _⦋2⦌) :
      X _⦋1⦌)
⊢ Eq.{u + 1} (α := X _⦋1⦌)
    (Path.arrow
      ((sx.spineEquiv 2 : (a : X _⦋2⦌) → X.Path 2)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map α.hom) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X.obj ((inclusion 2).op.obj α.right)))
            (lift sx s x) :
          (fun (X : Type u) ↦ X) (X.obj (obj (Functor.op (inclusion 2)) α.right))))
      t)
    (Path.arrow
      ((sx.spineEquiv 2 : (a : X _⦋2⦌) → X.Path 2)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app α) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj α)) →
                (fun (X : Type u) ↦ X) ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj α))
            x :
          (fun (X : Type u) ↦ X) (obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) α)))
      t)

Tactic:
dsimp [spineEquiv, α]

Premises used: SSet.StrictSegal.spineEquiv