-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  Eq (α :=
    X _⦋(↑(⟨(↑(↑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))))) :
        ℕ)⦌)
    ((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)))) :
      (fun (X : Type u) ↦ X)
        (X _⦋(↑(⟨(↑(↑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))))) :
            ℕ)⦌))
    (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⦌)
⊢ ψ
      (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

Tactic:
rwa [SSet.S.ext_iff]

Premises used: SSet.S.ext_iff