-- 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⦌.len ≤ 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 (α :=
    obj (C := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
      (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) (StructuredArrow.mk (op f)))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
            (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌)))
          (↾fun (x : s.pt) ↦ lift sx s x :
            s.pt ⟶
              Cone.pt (J := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
                (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌)))
          (NatTrans.app (Cone.π (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌)))
              (StructuredArrow.mk (op f)) :
            obj (C := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
                (obj
                  (Functor.const
                    (StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))))
                  (Cone.pt (J :=
                    StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
                    (RightExtension.coneAt (rightExtensionInclusion X 2) (op ⦋n⦌))))
                (StructuredArrow.mk (op f)) ⟶
              obj (C := StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2)))
                (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) (StructuredArrow.mk (op f)))))
      x)
    (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app (StructuredArrow.mk (op f)))) x)
have h : 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 sorry).op)) :
                (a : s.pt) → X _⦋1⦌)
              x,
          arrow_src := sorry, arrow_tgt := sorry }) :
    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⦌)
Tactic: dsimp at hi ⊢