-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ 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⦌))
have 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⦌) sorry)
    ((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⦌) sorry) :
                (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₃
Tactic: rw [Types.isPullback_iff]