awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x_1 : SimplexCategoryᵒᵖ
n : ℕ
x_2 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
y : (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) x
h :
  x =
    (↑((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))
          y) :
      Y _⦋n⦌)
⊢ ∃ (x₁ : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
          x₁ =
        Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
          Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
            x)
          x hx ∧
      (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⦌))
          x₁ =
        y
have subst : ∀
  (hx :
    Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
      (↑((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))
            y) :
        Y _⦋n⦌)),
  ∃ (x₁ : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
          x₁ =
        Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
          Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
            x)
          (↑((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))
                y) :
            Y _⦋n⦌)
          hx ∧
      (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⦌))
          x₁ =
        y
Tactic: subst h
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    (↑((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⦌))
            y)) :
      Y _⦋n⦌)
⊢ ∃ (x₁ : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
          x₁ =
        Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
          Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
            x)
          (↑((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⦌))
                  y)) :
            Y _⦋n⦌)
          hx ∧
      Eq (α := (fun (X : Type u) ↦ X) (sigmaStdSimplex 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⦌))
            x₁ :
          (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⦌))
            y :
          (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
have refine_1 : Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) y
Tactic: refine ⟨c.ιSigmaBoundary.app _ ⟨y, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (hypothesis)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    (↑((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⦌))
            y)) :
      Y _⦋n⦌)
⊢ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) y
have hx₁ : Membership.mem (α := Y _⦋n⦌) (γ := Set (Y _⦋n⦌))
  (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋n⦌)) : (a : Δ[d] _⦋n⦌) → Y _⦋n⦌) y : Y _⦋n⦌)
Tactic: rw [dsimp% congr($(c.ι_b_ι).app (op ⦋n⦌) y)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (α := Y _⦋n⦌) (γ := Set (Y _⦋n⦌))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋n⦌)) : (a : Δ[d] _⦋n⦌) → Y _⦋n⦌) y : Y _⦋n⦌)
⊢ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) y
have refine_1 : Membership.mem (γ := Set (Δ[d] _⦋n⦌))
  ((Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map).obj (op ⦋n⦌)) y
Tactic: rwa [← c.preimage_map, Subcomplex.preimage_obj, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (α := Y _⦋n⦌) (γ := Set (Y _⦋n⦌))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋n⦌)) : (a : Δ[d] _⦋n⦌) → Y _⦋n⦌) y : Y _⦋n⦌)
refine_1 :
  Membership.mem (γ := Set (Δ[d] _⦋n⦌))
    ((Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map).obj (op ⦋n⦌)) y
⊢ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) y
have refine_1₁ : Membership.mem (γ := Set (Δ[d] _⦋n⦌))
  (Set.preimage (β := (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋n⦌))) :
      (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)))
  y
Tactic: rwa [← c.preimage_map, Subcomplex.preimage_obj, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d) = ⊤
have rw : ⊤ ≤ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d)
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (hypothesis)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
x : Y.obj (op n)
hx :
  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)
⊢ Membership.mem (γ :=
    Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
    ((Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d)).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)
have hx₁ : Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) x ∨
  ∃ i_1 ∈ Y.nonDegenerate d,
    (∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (FC := TypeCat.Fun) (i.app (op ⦋d⦌)) : (a : X _⦋d⦌) → Y _⦋d⦌) x = i_1) ∧
      Membership.mem (γ := Set (Y.obj (op n))) ((Subcomplex.ofSimplex i_1).obj (op n)) x
Tactic: simp only [skeletonOfMono_succ, Subfunctor.range_obj, Set.mem_range, not_exists,
    Subfunctor.max_obj, Subfunctor.iSup_obj, Set.iUnion_coe_set, Set.mem_union, Set.mem_iUnion,
    exists_prop] at hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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⦌))
⊢ ∃ (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
have 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⦌))
Tactic: obtain ⟨c, s, rfl⟩ := ιSigmaStdSimplex_jointly_surjective y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (hypothesis)
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⦌))
⊢ ∃ (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⦌))
have hs : s ∉ ∂Δ[d].obj (op ⦋n⦌)
Tactic: have hs : s ∉ ∂Δ[d].obj _ :=
    fun hs ↦ hy (⟨c.ιSigmaBoundary.app _ ⟨s, hs⟩, congr($(c.ι_l).app _ ⟨s, _⟩)⟩)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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⦌)
⊢ ∃ (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⦌))
have refine : Epi (C := SimplexCategory) (X := ⦋n⦌) (Y := ⦋d⦌)
  (((stdSimplex.objEquiv : Δ[d] _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ ⦋d⦌)) : (a : Δ[d] _⦋n⦌) → unop (op ⦋n⦌) ⟶ ⦋d⦌) s)
Tactic: refine ⟨c, stdSimplex.objEquiv s, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ 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) ⋯))
have 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))
Tactic: refine (isColimitMapCoconePushoutCoconeEquiv _ _).2
      (IsPushout.isColimit ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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))
have 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))
Tactic: refine Types.isPushout_of_isPullback_of_mono' ?_ ?_ ?_
-- 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))
⊢ 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_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
Tactic: refine Types.isPushout_of_isPullback_of_mono' ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
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⦌)
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w_1 : 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 (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f₁.op) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        c₁.simplex :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f₂.op) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        c₂.simplex :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
⊢ c₁ = c₂
have simplex : c₁.simplex = c₂.simplex
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Splitting (goal)
Goal:
X : SSet
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ Nonempty.{u + 2}
    (IsColimit (J := Discrete (SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌))) (F :=
      Discrete.functor
        (SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)))
      (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
        (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
have rw : Functor.CoconeTypes.IsColimit (J := Discrete (SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌))) (F :=
  Discrete.functor
    (SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)))
  (Cofan.cofanTypes (F :=
    SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
    (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
      (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
Tactic: rw [← Limits.Cofan.isColimit_cofanTypes_iff]