-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsPullback (P := Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j)) (Z :=
    Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration (Order.succ j)).toSSet)
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.t j))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (homOfLE ⋯))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j))
have rw : Eq (α :=
    Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j) ⟶
      Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration (Order.succ j)).toSSet)
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.t j) ≫
      CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (homOfLE sorry))
    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j) ≫
      CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j)) ∧
  (∀
      (x₁ y₁ :
        (fun (X : Type u) ↦ X)
          (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j))),
      Eq (α :=
            (fun (X : Type u) ↦ X)
              (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration j).toSSet))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.t j)) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaHorn j))) →
                    (fun (X : Type u) ↦ X)
                      (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.filtration j).toSSet))
                x₁ :
              (fun (X : Type u) ↦ X)
                (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration j).toSSet))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.t j)) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaHorn j))) →
                    (fun (X : Type u) ↦ X)
                      (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.filtration j).toSSet))
                y₁ :
              (fun (X : Type u) ↦ X)
                (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration j).toSSet)) ∧
          Eq (α :=
            (fun (X : Type u) ↦ X)
              (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaStdSimplex j)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j)) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaHorn j))) →
                    (fun (X : Type u) ↦ X)
                      (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)))
                x₁ :
              (fun (X : Type u) ↦ X)
                (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaStdSimplex j)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j)) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaHorn j))) →
                    (fun (X : Type u) ↦ X)
                      (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)))
                y₁ :
              (fun (X : Type u) ↦ X)
                (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaStdSimplex j))) →
        x₁ = y₁) ∧
    ∀
      (x₂ :
        (fun (X : Type u) ↦ X)
          (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration j).toSSet))
      (x₃ :
        (fun (X : Type u) ↦ X)
          (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaStdSimplex j))),
      Eq (α :=
          (fun (X : Type u) ↦ X)
            (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌)
              (f.filtration (Order.succ j)).toSSet))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (homOfLE sorry)) :
                (a :
                    (fun (X : Type u) ↦ X)
                      (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.filtration j).toSSet)) →
                  (fun (X : Type u) ↦ X)
                    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj
                      (f.filtration (Order.succ j)).toSSet))
              x₂ :
            (fun (X : Type u) ↦ X)
              (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌)
                (f.filtration (Order.succ j)).toSSet))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j)) :
                (a :
                    (fun (X : Type u) ↦ X)
                      (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j))) →
                  (fun (X : Type u) ↦ X)
                    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj
                      (f.filtration (Order.succ j)).toSSet))
              x₃ :
            (fun (X : Type u) ↦ X)
              (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌)
                (f.filtration (Order.succ j)).toSSet)) →
        ∃ (x₁ :
          (fun (X : Type u) ↦ X)
            (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j))),
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.t j)) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaHorn j))) →
                    (fun (X : Type u) ↦ X)
                      (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.filtration j).toSSet))
                x₁ =
              x₂ ∧
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j)) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaHorn j))) →
                    (fun (X : Type u) ↦ X)
                      (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)))
                x₁ =
              x₃
Tactic: rw [Types.isPullback_iff]