-- 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
φ : strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) lift._proof_3 ⟶ strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) lift._proof_1 :=
  homMk (Quiver.Hom.op (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯)) ⋯
⊢ 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.δ 1) 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.castSucc)))) :
          (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.castSucc).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.castSucc).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.castSucc)))))

Tactic:
ConcreteCategory.congr_hom (s.w φ) x

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, CategoryTheory.Limits.Cone.w, CategoryTheory.ObjectProperty.homMk, CategoryTheory.ConcreteCategory.congr_hom, OrderEmbedding.toOrderHom, SimplexCategory.Hom.mk