-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
            (a : sigmaStdSimplex i d _⦋n⦌) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            y)) :
      Y _⦋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))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaBoundary.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (∂Δ[d].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
        (Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) x) y ⋯)) =
    Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
      Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) x)
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
              (a : sigmaStdSimplex i d _⦋n⦌) →
                (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
              y)) :
        Y _⦋n⦌)
      hx
have refine_2 : (↑((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))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaBoundary.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (∂Δ[d].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
          (Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) x) y sorry))) :
    Y _⦋n⦌) =
  (↑(Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
        Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) x)
        (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
                (a : sigmaStdSimplex i d _⦋n⦌) →
                  (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                  (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                y)) :
          Y _⦋n⦌)
        hx) :
    Y _⦋n⦌)
Tactic: rw [Subtype.ext_iff]