-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (hypothesis)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x_1 : SimplexCategoryᵒᵖ
n : ℕ
x_2 : (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
have h₁ : Eq.{u + 1} (α := Y _⦋n⦌)
  (↑((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)) :
    Y _⦋n⦌)
  (↑((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) :
    Y _⦋n⦌)
Tactic: rw [Subtype.ext_iff] at h
Cleared hypotheses: h