-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (FC := TypeCat.Fun) (i.app (op ⦋d⦌)) : (a : X _⦋d⦌) → Y _⦋d⦌) x = y
f : op ⦋d⦌ ⟶ op n
hx :
  Membership.mem (α := Y.obj (op n)) (γ := Set (Y.obj (op n)))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
        y :
      (fun (X : Type u) ↦ X) (Y.obj (op n)))
h :
  Membership.mem (α := (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n))
    (γ := Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
    (Subfunctor.obj ⊤ (op n))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
          y)
        hx :
      { x : Y.obj (op n) //
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x })
c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := ⋯ }
⊢ Eq (α := (↑(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 : (sigmaStdSimplex i d).obj (op 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].obj (op n))) → (fun (X : Type u) ↦ X) ((sigmaStdSimplex i d).obj (op n)))
          ((Equiv.symm stdSimplex.objEquiv : (a : unop (op n) ⟶ ⦋d⦌) → Δ[d].obj (op n)) f.unop : Δ[d].obj (op n))) :
      (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) : Type u))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
          y)
        hx :
      { x : Y.obj (op n) //
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x })
have inr : Eq (α := Y.obj (op n))
  ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op n)) :
            (a : (sigmaStdSimplex i d).obj (op 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].obj (op n))) →
                (fun (X : Type u) ↦ X) ((sigmaStdSimplex i d).obj (op n)))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op n) ⟶ ⦋d⦌) → Δ[d].obj (op n)) f.unop : Δ[d].obj (op n)))) :
      Y.obj (op n)) :
    Y.obj (op n))
  ((↑(Subtype.mk (p := fun (x : Y.obj (op n)) ↦
          Membership.mem (γ := Set (Y.obj (op n)))
            (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
              (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
            y)
          hx) :
      Y.obj (op n)) :
    Y.obj (op n))
Tactic: rw [Subtype.ext_iff]