-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
rw :
  Eq (α :=
      sigmaBoundary i d _⦋n⦌ ⟶
        (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
      ((t i d).app (op ⦋n⦌) ≫
        ↾fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)) ↦
          Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
            Membership.mem (γ := Set (Y _⦋n⦌))
              (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) x)
            (↑x : Y _⦋n⦌) ⋯)
      ((l i d).app (op ⦋n⦌) ≫ (b i d).app (op ⦋n⦌)) ∧
    (∀ (x₁ y₁ : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)),
        Eq (α :=
              (fun (X : Type u) ↦ X)
                (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
                      (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
                  x₁ :
                (fun (X : Type u) ↦ X)
                  (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
                      (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
                  y₁ :
                (fun (X : Type u) ↦ X)
                  (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)) ∧
            Eq (α := (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
                      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                  x₁ :
                (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
                      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                  y₁ :
                (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) →
          x₁ = y₁) ∧
      ∀
        (x₂ :
          (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u))
        (x₃ : (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)),
        Eq (α :=
            (fun (X : Type u) ↦ X)
              (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (↾fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)) ↦
                      Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
                        Membership.mem (γ := Set (Y _⦋n⦌))
                          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) x)
                        (↑x : Y _⦋n⦌) ⋯) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u)) →
                    (fun (X : Type u) ↦ X)
                      (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
                x₂ :
              (fun (X : Type u) ↦ X)
                (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
                  (a : (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) →
                    (fun (X : Type u) ↦ X)
                      (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
                x₃ :
              (fun (X : Type u) ↦ X)
                (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u)) →
          ∃ (x₁ : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)),
            (ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
                      (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
                  x₁ =
                x₂ ∧
              (ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
                      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                  x₁ =
                x₃
⊢ IsPullback (P := sigmaBoundary i d _⦋n⦌) ((t i d).app (op ⦋n⦌)) ((l i d).app (op ⦋n⦌))
    (↾fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)) ↦
      Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
        Membership.mem (γ := Set (Y _⦋n⦌))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) x)
        (↑x : Y _⦋n⦌) ⋯)
    ((b i d).app (op ⦋n⦌))

Tactic:
rw [Types.isPullback_iff]

Premises used: CategoryTheory.Limits.Types.isPullback_iff