-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal (goal)
Goal:
X_1 : SSet
sx_1 : X_1.StrictSegal
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 : Fin n
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((obj (C := Truncated (HAdd.hAdd (α := ℕ) 0 1)) (Truncated.trunc (HAdd.hAdd (α := ℕ) 0 1) 1 ⋯)
            (obj (truncation 1) X)).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌
            Truncated.Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((obj (C := Truncated (HAdd.hAdd (α := ℕ) 0 1)) (Truncated.trunc (HAdd.hAdd (α := ℕ) 0 1) 1 ⋯)
                  (obj (truncation 1) X)).map
              (Hom.tr (SimplexCategory.δ 0) Truncated.Path₁._proof_1 Truncated.Path₁._proof_5).op) :
          (a :
              (fun (X : Type u) ↦ X)
                (((Truncated.trunc (0 + 1) 1 ⋯).obj ((truncation 1).obj X)).obj
                  (op { obj := ⦋0 + 1⦌, property := Truncated.Path₁._proof_5 }))) →
            (fun (X : Type u) ↦ X)
              (((Truncated.trunc (0 + 1) 1 ⋯).obj ((truncation 1).obj X)).obj
                (op { obj := ⦋0⦌, property := Truncated.Path₁._proof_1 })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op)) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                      (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) →
                (fun (X : Type u) ↦ X)
                  ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                    (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op)))
            x :
          (fun (X : Type u) ↦ X)
            (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 (mkOfLe i.castSucc i.succ ⋯).op))) :
      (fun (X : Type u) ↦ X)
        ((obj (C := Truncated (HAdd.hAdd (α := ℕ) 0 1)) (Truncated.trunc (HAdd.hAdd (α := ℕ) 0 1) 1 ⋯)
              (obj (truncation 1) X)).obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌
              Truncated.Path₁._proof_1))))
    ((ConcreteCategory.hom (FC := 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
                  ((obj (C := SimplexCategory.Truncated 2) (inclusion 2)
                        (unop
                          (op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              lift._proof_2)))).const
                    ⦋n⦌ i.succ)))) :
          (a :
              (fun (X : Type u) ↦ X)
                (((Functor.const (StructuredArrow (op ⦋n⦌) (inclusion 2).op)).obj s.pt).obj
                  (StructuredArrow.mk
                    (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i.succ).op))) →
            (fun (X : Type u) ↦ X)
              ((proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X).obj
                (StructuredArrow.mk
                  (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i.succ).op)))
        x :
      (fun (X : Type u) ↦ X)
        (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 (Y :=
            op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ lift._proof_2))
            (Quiver.Hom.op
              ((obj (C := SimplexCategory.Truncated 2) (inclusion 2)
                    (unop
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          lift._proof_2)))).const
                ⦋n⦌ i.succ)))))
have dsimp : Eq (α :=
  obj (C := (SimplexCategory.Truncated 1)ᵒᵖ) (obj (truncation 1) X)
    (op
      (obj (incl 1 1 sorry)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌ Truncated.Path₁._proof_1))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (obj (truncation 1) X)
            (Quiver.Hom.op (ObjectProperty.homMk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) (SimplexCategory.δ 0)))) :
        (a : ((truncation 1).obj X).obj (op ((incl 1 1 sorry).obj { obj := ⦋1⦌, property := Truncated.Path₁._proof_5 }))) →
          ((truncation 1).obj X).obj (op ((incl 1 1 sorry).obj { obj := ⦋0⦌, property := Truncated.Path₁._proof_1 })))
      ((@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 :
        X _⦋1⦌) :
    obj (C := (SimplexCategory.Truncated 1)ᵒᵖ) (obj (truncation 1) X)
      (op
        (obj (incl 1 1 sorry)
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 1) ⦋0⦌
            Truncated.Path₁._proof_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.succ)))) :
        (a : s.pt) → X _⦋0⦌)
      x :
    X _⦋0⦌)
Tactic: dsimp