-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
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
⊢ ∃! 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⦌)))⦌)
have 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⦌) sorry),
  ∃! 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⦌) sorry).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⦌) sorry).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⦌) sorry).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
Cleared hypotheses: y, hy