-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ 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₃

Tactic:
⟨NatTrans.congr_app (w i d) _,
      fun x₁ x₂ ⟨_, h⟩ ↦ injective_of_mono ((l i d).app (op ⦋n⦌)) h,
      fun ⟨x, hx⟩ y h ↦ ?_⟩

Premises used: _private.0.SSet.relativeCellComplexOfMono.isPullback.match_2, _private.0.SSet.relativeCellComplexOfMono.isPullback.match_3, CategoryTheory.ConcreteCategory.hom, Exists, CategoryTheory.NatTrans.congr_app, And, SimplexCategory.mk, Opposite.op, And.intro, SSet.relativeCellComplexOfMono.l, CategoryTheory.injective_of_mono, SSet.relativeCellComplexOfMono.w, Eq, DFunLike.coe, SSet.relativeCellComplexOfMono.t, CategoryTheory.NatTrans.app