-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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
dsimp :
  Eq (α :=
    obj (C := (SimplexCategory.Truncated 1)ᵒᵖ) (obj (truncation 1) X)
      (op
        (obj (incl 1 1 ⋯)
          (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 ⋯).obj { obj := ⦋1⦌, property := Truncated.Path₁._proof_5 }))) →
            ((truncation 1).obj X).obj (op ((incl 1 1 ⋯).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 ⋯).op)) :
              (a : s.pt) → X _⦋1⦌)
            x :
          X _⦋1⦌) :
      obj (C := (SimplexCategory.Truncated 1)ᵒᵖ) (obj (truncation 1) X)
        (op
          (obj (incl 1 1 ⋯)
            (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⦌)
⊢ 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)))))

Tactic:
dsimp