-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
t : T
f :
  ⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌ ⟶
    ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌
w : CategoryTheory.Mono f
hf :
  (CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌))
      (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))) =
    (↑(↑t : (↑P.II : Type u)) : A.N).simplex
⊢ ψ
      (Sigma.mk (β :=
        fun
          (d :
            Fin
              (S.dim.{u} (X := X)
                (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ↦
        ⦋(↑d : ℕ)⦌ ⟶
          ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
        (⟨(↑(↑t : (↑P.II : Type u)) : A.N).dim, ⋯⟩ :
          Fin
            (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
        f) =
    (↑(↑t : (↑P.II : Type u)) : A.N).toS
have refine_2 : Eq (α :=
  X _⦋(↑(⟨(↑(↑t : (↑P.II : Type u)) : A.N).dim, sorry⟩ :
          Fin
            (S.dim.{u} (X := X)
              (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) :
      ℕ)⦌)
  ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(↑⟨(↑(↑t : (↑P.II : Type u)) : A.N).dim, sorry⟩ : ℕ)⦌))
      (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))) :
    (fun (X : Type u) ↦ X)
      (X _⦋(↑(⟨(↑(↑t : (↑P.II : Type u)) : A.N).dim, sorry⟩ :
              Fin
                (S.dim.{u} (X := X)
                  (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) :
          ℕ)⦌))
  (S.simplex (↑(↑t : (↑P.II : Type u)) : A.N).toN.1 : X _⦋S.dim.{u} (X := X) (↑(↑t : (↑P.II : Type u)) : A.N).toN.1⦌)
Tactic: rwa [SSet.S.ext_iff]