-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
z : (↑(X.nonDegenerate m) : Type u)
hy :
  toN
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌))) =
    y
obtain :
  ∀
    (hy :
      toN
          (mk (dim := n)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
              (↑z : X _⦋m⦌))) =
        N.mk (↑z : X _⦋m⦌) ⋯),
    ∃! f_1 :
      ⦋dim.{u} (X := X)
            (mk (dim := n)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                (↑z : X _⦋m⦌)))⦌ ⟶
        ⦋(N.mk (↑z : X _⦋m⦌) ⋯).dim⦌,
      Epi f_1 ∧
        Eq (α :=
          (fun (X : Type u) ↦ X)
            (X _⦋dim.{u} (X := X)
                (mk (dim := n)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                    (↑z : X _⦋m⦌)))⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑z : X _⦋m⦌) ⋯).dim⦌)) →
                  (fun (X : Type u) ↦ X)
                    (X _⦋{ dim := n,
                          simplex :=
                            (ConcreteCategory.hom (X.map f.op) :
                                (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                              (↑z : X _⦋m⦌) }.dim⦌))
              (N.mk (↑z : X _⦋m⦌) ⋯).simplex :
            (fun (X : Type u) ↦ X)
              (X _⦋dim.{u} (X := X)
                  (mk (dim := n)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                      (↑z : X _⦋m⦌)))⦌))
          (simplex
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  (↑z : X _⦋m⦌))) :
            X _⦋dim.{u} (X := X)
                (mk (dim := n)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                    (↑z : X _⦋m⦌)))⦌)
⊢ ∃! f_1 :
    ⦋dim.{u} (X := X)
          (mk (dim := n)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
              (↑z : X _⦋m⦌)))⦌ ⟶
      ⦋y.dim⦌,
    Epi f_1 ∧
      Eq (α :=
        (fun (X : Type u) ↦ X)
          (X _⦋dim.{u} (X := X)
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  (↑z : X _⦋m⦌)))⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) →
                (fun (X : Type u) ↦ X)
                  (X _⦋{ dim := n,
                        simplex :=
                          (ConcreteCategory.hom (X.map f.op) :
                              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                            (↑z : X _⦋m⦌) }.dim⦌))
            y.simplex :
          (fun (X : Type u) ↦ X)
            (X _⦋dim.{u} (X := X)
                (mk (dim := n)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                    (↑z : X _⦋m⦌)))⦌))
        (simplex
            (mk (dim := n)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                (↑z : X _⦋m⦌))) :
          X _⦋dim.{u} (X := X)
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  (↑z : X _⦋m⦌)))⦌)

Tactic:
obtain rfl : y = N.mk _ z.2 := by
    rw [toN_eq_iff] at hy
    rw [← N.subcomplex_injective_iff, hy]
    exact subcomplex_eq_of_epi _ _ f rfl

Premises used: SSet.N.mk, rfl, Subtype.property