-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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₃
have 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⦌) 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))
          (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
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 ↦ ?_⟩