-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
refine_1 :
  IsPullback (P := Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (sigmaBoundary i d))
    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (t i d))
    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (l i d))
    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (r i d))
    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (b i d))
refine_2 :
  Eq (α :=
    Set
      ((fun (X : Type u) ↦ X)
        (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌)
          (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))))))
    (Set.range (ι :=
        (fun (X : Type u) ↦ X)
          (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌)
            (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d))))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (r i d))) :
          (a :
              (fun (X : Type u) ↦ X)
                (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj
                  ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).toSSet)) →
            (fun (X : Type u) ↦ X)
              (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj
                ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).toSSet)) ⊔
      Set.range (ι :=
        (fun (X : Type u) ↦ X) (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (sigmaStdSimplex i d)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (b i d))) :
          (a : (fun (X : Type u) ↦ X) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d))) →
            (fun (X : Type u) ↦ X)
              (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj
                ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).toSSet)))
    Set.univ
refine_3 :
  ∀ (x₃ y₃ : Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (sigmaStdSimplex i d)),
    x₃ ∉
        Set.range (ι :=
          (fun (X : Type u) ↦ X) (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (sigmaBoundary i d)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (l i d))) :
            (a : (fun (X : Type u) ↦ X) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaBoundary i d))) →
              (fun (X : Type u) ↦ X) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d))) →
      y₃ ∉
          Set.range (ι :=
            (fun (X : Type u) ↦ X) (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (sigmaBoundary i d)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                  (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (l i d))) :
              (a : (fun (X : Type u) ↦ X) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaBoundary i d))) →
                (fun (X : Type u) ↦ X) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d))) →
        Eq (α :=
            (fun (X : Type u) ↦ X)
              (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌)
                (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (b i d)) :
                  (a : (fun (X : Type u) ↦ X) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d))) →
                    (fun (X : Type u) ↦ X)
                      (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj
                        ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).toSSet))
                x₃ :
              (fun (X : Type u) ↦ X)
                (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌)
                  (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (b i d)) :
                  (a : (fun (X : Type u) ↦ X) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d))) →
                    (fun (X : Type u) ↦ X)
                      (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj
                        ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).toSSet))
                y₃ :
              (fun (X : Type u) ↦ X)
                (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌)
                  (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))))) →
          x₃ = y₃
⊢ IsPushout (Z := Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (sigmaBoundary i d))
    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (t i d))
    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (l i d))
    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (r i d))
    (CategoryTheory.Functor.map (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (b i d))

Tactic:
refine Types.isPushout_of_isPullback_of_mono' ?_ ?_ ?_

Premises used: CategoryTheory.Limits.Types.isPushout_of_isPullback_of_mono'