awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
x : Y.obj (op n)
hx_1 :
  Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n))
    x
h :
  Membership.mem (γ :=
    Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
    (Subfunctor.obj ⊤ (op n))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
      Membership.mem (γ := Set (Y.obj (op n)))
        (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
      x hx_1)
hx : Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) x
⊢ Membership.mem (γ := Set (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) : Type u))
    (Set.range (ι := (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u))
        (⇑{
              toFun := fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u)) ↦
                Subtype.mk (p := fun (x : Y.obj (op n)) ↦
                  Membership.mem (γ := Set (Y.obj (op n)))
                    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
                  (↑x : Y.obj (op n)) ⋯ } :
          (a : (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op n)) : Type u)) →
            (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)) ∪
      Set.range (ι := (sigmaStdSimplex i d).obj (op n))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op n))) :
          (a : (sigmaStdSimplex i d).obj (op n)) →
            (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
      Membership.mem (γ := Set (Y.obj (op n)))
        (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
      x hx_1)

Tactic:
exact Or.inl ⟨⟨x, hx⟩, rfl⟩

Premises used: Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (FC := TypeCat.Fun) (i.app (op ⦋d⦌)) : (a : X _⦋d⦌) → Y _⦋d⦌) x = y
f : op ⦋d⦌ ⟶ op n
hx :
  Membership.mem (α := Y.obj (op n)) (γ := Set (Y.obj (op n)))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
        y :
      (fun (X : Type u) ↦ X) (Y.obj (op n)))
h :
  Membership.mem (α := (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n))
    (γ := Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
    (Subfunctor.obj ⊤ (op n))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
          y)
        hx :
      { x : Y.obj (op n) //
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x })
⊢ y ∉
    Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋d⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (i.app (op ⦋d⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y _⦋d⦌))

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (FC := TypeCat.Fun) (i.app (op ⦋d⦌)) : (a : X _⦋d⦌) → Y _⦋d⦌) x = y
f : op ⦋d⦌ ⟶ op n
hx :
  Membership.mem (α := Y.obj (op n)) (γ := Set (Y.obj (op n)))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
        y :
      (fun (X : Type u) ↦ X) (Y.obj (op n)))
h :
  Membership.mem (α := (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n))
    (γ := Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
    (Subfunctor.obj ⊤ (op n))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
          y)
        hx :
      { x : Y.obj (op n) //
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x })
c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := ⋯ }
⊢ Eq (α := Y.obj (op n))
    ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op n)) :
              (a : (sigmaStdSimplex i d).obj (op 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].obj (op n))) →
                  (fun (X : Type u) ↦ X) ((sigmaStdSimplex i d).obj (op n)))
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op n) ⟶ ⦋d⦌) → Δ[d].obj (op n)) f.unop :
                Δ[d].obj (op n)))) :
        Y.obj (op n)) :
      Y.obj (op n))
    ((↑(Subtype.mk (p := fun (x : Y.obj (op n)) ↦
            Membership.mem (γ := Set (Y.obj (op n)))
              (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
              y)
            hx) :
        Y.obj (op n)) :
      Y.obj (op n))

Tactic:
c.b_app_ι_app_objEquiv_symm_val _

Premises used: Quiver.Hom.op, Quiver.Hom.unop, SSet.relativeCellComplexOfMono.Cell.b_app_ι_app_objEquiv_symm_val
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (FC := TypeCat.Fun) (i.app (op ⦋d⦌)) : (a : X _⦋d⦌) → Y _⦋d⦌) x = y
f : op ⦋d⦌ ⟶ op n
hx :
  Membership.mem (α := Y.obj (op n)) (γ := Set (Y.obj (op n)))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
        y :
      (fun (X : Type u) ↦ X) (Y.obj (op n)))
h :
  Membership.mem (α := (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n))
    (γ := Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
    (Subfunctor.obj ⊤ (op n))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
          y)
        hx :
      { x : Y.obj (op n) //
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x })
c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := ⋯ }
⊢ Eq (α := Y.obj (op n))
    ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op n)) :
              (a : (sigmaStdSimplex i d).obj (op 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].obj (op n))) →
                  (fun (X : Type u) ↦ X) ((sigmaStdSimplex i d).obj (op n)))
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op n) ⟶ ⦋d⦌) → Δ[d].obj (op n)) f.unop :
                Δ[d].obj (op n)))) :
        Y.obj (op n)) :
      Y.obj (op n))
    ((↑(Subtype.mk (p := fun (x : Y.obj (op n)) ↦
            Membership.mem (γ := Set (Y.obj (op n)))
              (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
              y)
            hx) :
        Y.obj (op n)) :
      Y.obj (op n))

Tactic:
exact c.b_app_ι_app_objEquiv_symm_val _

Premises used: SSet.relativeCellComplexOfMono.Cell.b_app_ι_app_objEquiv_symm_val
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategoryᵒᵖ
⊢ Eq (α :=
    Set
      ((fun (X : Type u) ↦ X)
        ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj n)))
    (Set.range (ι :=
        (fun (X : Type u) ↦ X) ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d)).obj n))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((r i d).app n)) :
          (a : (fun (X : Type u) ↦ X) (((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).toSSet.obj n)) →
            (fun (X : Type u) ↦ X) (((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).toSSet.obj n)) ∪
      Set.range (ι := (fun (X : Type u) ↦ X) ((sigmaStdSimplex i d).obj n))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app n)) :
          (a : (fun (X : Type u) ↦ X) ((sigmaStdSimplex i d).obj n)) →
            (fun (X : Type u) ↦ X) (((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).toSSet.obj n)))
    Set.univ

Tactic:
congr($(sup_range_r_range_b i d).obj n)

Premises used: congrArg, CategoryTheory.Subfunctor.obj, id, SSet.relativeCellComplexOfMono.sup_range_r_range_b
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
y : sigmaStdSimplex i d _⦋n⦌
hy :
  y ∉
    Set.range (ι := (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
        (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
obtain :
  ∀ (c : Cell i d) (s : Δ[d] _⦋n⦌)
    (hy :
      ((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⦌))
            s :
          (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
        Set.range (ι := (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
            (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))),
    ∃ (c_1 : Cell i d) (f : ⦋n⦌ ⟶ ⦋d⦌) (_ : Epi f),
      Eq (α := (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c_1.ι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⦌))
            s :
          (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
⊢ ∃ (c : Cell i d) (f : ⦋n⦌ ⟶ ⦋d⦌) (_ : Epi f),
    (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⦌) =
      y

Tactic:
obtain ⟨c, s, rfl⟩ := ιSigmaStdSimplex_jointly_surjective y

Premises used: SSet.relativeCellComplexOfMono.ιSigmaStdSimplex_jointly_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
c : Cell i d
s : Δ[d] _⦋n⦌
hy :
  ((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⦌))
        s :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
    Set.range (ι := (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
        (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
⊢ s ∉ ∂Δ[d].obj (op ⦋n⦌)

Tactic:
have hs : s ∉ ∂Δ[d].obj _ :=
    fun hs ↦ hy (⟨c.ιSigmaBoundary.app _ ⟨s, hs⟩, congr($(c.ι_l).app _ ⟨s, _⟩)⟩)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
c : Cell i d
s : Δ[d] _⦋n⦌
hy :
  ((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⦌))
        s :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
    Set.range (ι := (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
        (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
hs : s ∉ ∂Δ[d].obj (op ⦋n⦌)
⊢ Eq (α := (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⦌)
            (((stdSimplex.objEquiv : Δ[d] _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ ⦋d⦌)) : (a : Δ[d] _⦋n⦌) → unop (op ⦋n⦌) ⟶ ⦋d⦌) s) :
          Δ[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⦌))
        s :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
c : Cell i d
s : Δ[d] _⦋n⦌
hy :
  ((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⦌))
        s :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
    Set.range (ι := (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
        (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
hs : s ∉ ∂Δ[d].obj (op ⦋n⦌)
refine :
  Epi (C := SimplexCategory) (X := ⦋n⦌) (Y := ⦋d⦌)
    (((stdSimplex.objEquiv : Δ[d] _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ ⦋d⦌)) : (a : Δ[d] _⦋n⦌) → unop (op ⦋n⦌) ⟶ ⦋d⦌) s)
⊢ ∃ (c_1 : Cell i d) (f : ⦋n⦌ ⟶ ⦋d⦌) (_ : Epi f),
    Eq (α := (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c_1.ι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⦌))
          s :
        (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))

Tactic:
refine ⟨c, stdSimplex.objEquiv s, ?_, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
c : Cell i d
s : Δ[d] _⦋n⦌
hy :
  ((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⦌))
        s :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
    Set.range (ι := (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
        (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
hs : s ∉ ∂Δ[d].obj (op ⦋n⦌)
⊢ Epi (C := SimplexCategory) (X := ⦋n⦌) (Y := ⦋d⦌)
    (((stdSimplex.objEquiv : Δ[d] _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ ⦋d⦌)) : (a : Δ[d] _⦋n⦌) → unop (op ⦋n⦌) ⟶ ⦋d⦌) s)

Tactic:
simpa [SimplexCategory.epi_iff_surjective, boundary] using hs

Premises used: SSet.boundary, SimplexCategory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
refine :
  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))
⊢ IsColimit (F := span (t i d) (l i d) ⋙ evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌)
    (Functor.mapCocone (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (PushoutCocone.mk (r i d) (b i d) ⋯))

Tactic:
refine (isColimitMapCoconePushoutCoconeEquiv _ _).2
      (IsPushout.isColimit ?_)

Premises used: CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv, Equiv.invFun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ 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:
Types.isPushout_of_isPullback_of_mono' ?_ ?_ ?_

Premises used: CategoryTheory.Limits.Types.isPushout_of_isPullback_of_mono'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ 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))

Tactic:
(isPullback i d).map ((evaluation _ _).obj _)

Premises used: SSet.relativeCellComplexOfMono.isPullback, CategoryTheory.evaluation, CategoryTheory.IsPullback.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ 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))

Tactic:
exact (isPullback i d).map ((evaluation _ _).obj _)

Premises used: SSet.relativeCellComplexOfMono.isPullback, CategoryTheory.evaluation, CategoryTheory.IsPullback.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ 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

Tactic:
range_r_app_union_range_b_app _ _ _

Premises used: SSet.relativeCellComplexOfMono.range_r_app_union_range_b_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ 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

Tactic:
exact range_r_app_union_range_b_app _ _ _

Premises used: SSet.relativeCellComplexOfMono.range_r_app_union_range_b_app