-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x₂ : sigmaStdSimplex i d _⦋n⦌
hx₂ :
  x₂ ∉
    Set.range (ι := sigmaBoundary i d _⦋n⦌)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
        (a : sigmaBoundary i d _⦋n⦌) → sigmaStdSimplex i d _⦋n⦌)
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w : Epi f₁
hx₁ :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₁ : Δ[d] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
    Set.range (ι := sigmaBoundary i d _⦋n⦌)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
        (a : sigmaBoundary i d _⦋n⦌) → sigmaStdSimplex i d _⦋n⦌)
h :
  Eq (α := (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
          (a : sigmaStdSimplex i d _⦋n⦌) →
            (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
          ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₁ : Δ[d] _⦋n⦌)) :
      (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
          (a : sigmaStdSimplex i d _⦋n⦌) →
            (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
        x₂ :
      (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
refine_3 :
  ∀ (c₂ : Cell i d) (f₂ : ⦋n⦌ ⟶ ⦋d⦌),
    Epi f₂ →
      ∀
        (hx₂ :
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₂.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                  (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₂ : Δ[d] _⦋n⦌) :
              (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
            Set.range (ι := sigmaBoundary i d _⦋n⦌)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
                (a : sigmaBoundary i d _⦋n⦌) → sigmaStdSimplex i d _⦋n⦌))
        (h :
          Eq (α := (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
                  (a : sigmaStdSimplex i d _⦋n⦌) →
                    (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₁ : Δ[d] _⦋n⦌)) :
              (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
                  (a : sigmaStdSimplex i d _⦋n⦌) →
                    (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₂.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₂ : Δ[d] _⦋n⦌)) :
              (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))),
        Eq (α := sigmaStdSimplex i d _⦋n⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₁ : Δ[d] _⦋n⦌) :
            (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₂.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₂ : Δ[d] _⦋n⦌) :
            (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
        (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₁ : Δ[d] _⦋n⦌) =
    x₂

Tactic:
obtain ⟨c₂, f₂, _, rfl⟩ := isPushout_aux x₂ hx₂

Premises used: SSet.relativeCellComplexOfMono.isPushout_aux, rfl