-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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 : ℕ
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 ⋯))
      (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 ⋯)) :
                  (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₃
⊢ 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))

Tactic:
rw [Types.isPullback_iff]

Premises used: CategoryTheory.Limits.Types.isPullback_iff