-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
refine :
  ∀ (x : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u))
    (y : (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) (x : Y _⦋n⦌)
    (hx :
      Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) x)
    (h :
      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))
            (Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
              Membership.mem (γ := Set (Y _⦋n⦌))
                (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) x)
              x hx) :
          (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))
            y :
          (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₁ =
          Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
            Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
              x)
            x hx ∧
        (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₁ =
          y
⊢ 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:
refine ⟨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 ↦ ?_⟩