-- 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
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)
⊢ 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)
have 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, sorry⟩ : Fin (n + 1)) (⟨i + k, sorry⟩ : Fin (n + 1)) (⟨j, sorry⟩ : Fin (n + 1)) sorry sorry))) :
            (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 sorry).op)) :
                    (a : s.pt) → X _⦋1⦌)
                  x,
              arrow_src := sorry, arrow_tgt := sorry }) :
        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, sorry⟩ ⟨i + k, sorry⟩ ⟨j, sorry⟩ sorry sorry) fac_aux₂._proof_11)) :
            (a : s.pt) → X _⦋2⦌)
          x :
        X _⦋2⦌) :
    X _⦋1⦌)
Tactic: dsimp [spineEquiv, α]