-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
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)
j : StructuredArrow (C := (SimplexCategory.Truncated 2)ᵒᵖ) (op ⦋n⦌) (Functor.op (inclusion 2))
x : s.pt
h :
  ∀ (i : SimplexCategory) (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)
⊢ 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⦌))) j :
            obj
                (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⦌))))
                j ⟶
              obj (proj (op ⦋n⦌) (Functor.op (inclusion 2)) ⋙ Functor.op (inclusion 2) ⋙ X) j)))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app j)).toFun x

Tactic:
obtain ⟨⟨i, hi⟩, ⟨f : _ ⟶ _⟩, rfl⟩ := j.mk_surjective

Premises used: CategoryTheory.StructuredArrow.mk_surjective, rfl