-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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
⊢ 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))
have 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₃
Tactic: refine Types.isPushout_of_isPullback_of_mono' ?_ ?_ ?_