-- 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 : ℕ
refine :
  ∀ (x₁ x₂ : Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaStdSimplex j))
    (hx₁ :
      x₁ ∉
        Set.range (ι :=
          (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.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))))
    (hx₂ :
      x₂ ∉
        Set.range (ι :=
          (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.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))))
    (h :
      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⦌) (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))
        ((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₁ = x₂
⊢ IsPushout (Z := Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j)) (P :=
    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:
refine Types.isPushout_of_isPullback_of_mono'
      ((f.isPullback j).map ((CategoryTheory.evaluation _ _).obj _))
      (f.range_homOfLE_app_union_range_b_app _ _) (fun x₁ x₂ hx₁ hx₂ h ↦ ?_)

Premises used: CategoryTheory.Limits.Types.isPushout_of_isPullback_of_mono', SSet.Subcomplex.Pairing.RankFunction.range_homOfLE_app_union_range_b_app, SSet.Subcomplex.Pairing.RankFunction.isPullback, CategoryTheory.evaluation, CategoryTheory.IsPullback.map, CategoryTheory.Functor.obj