awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
a :
  Subcomplex.range i ≤
      Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
        ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
          ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ∧
    (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤
        Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
          ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
            ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ∧
      ∀ (i_1 : (↑(Y.nonDegenerate n) : Type u)),
        Subcomplex.ofSimplex (↑i_1 : Y _⦋n⦌) ≤
          Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
            ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
              ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)
⊢ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) (n + 1) ≤
    Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
      ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
        ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)

Tactic:
simp only [sup_le_iff, iSup_le_iff, skeleton_succ]

Premises used: SSet.skeleton_succ, sup_le_iff, iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ≤
      Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
        ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
          ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ∧
    (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤
        Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
          ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
            ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ∧
      ∀ (i_1 : (↑(Y.nonDegenerate n) : Type u)),
        Subcomplex.ofSimplex (↑i_1 : Y _⦋n⦌) ≤
          Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
            ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
              ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)

Tactic:
⟨le_sup_left.trans le_sup_left,
      le_sup_right.trans le_sup_left, fun x ↦ ?_⟩

Premises used: le_sup_left, le_sup_right, And.intro, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
a :
  ∀ (x : (↑(Y.nonDegenerate n) : Type u)),
    Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤
      Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
        ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
          ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)
⊢ Subcomplex.range i ≤
      Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
        ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
          ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ∧
    (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤
        Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
          ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
            ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ∧
      ∀ (i_1 : (↑(Y.nonDegenerate n) : Type u)),
        Subcomplex.ofSimplex (↑i_1 : Y _⦋n⦌) ≤
          Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
            ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
              ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)

Tactic:
refine ⟨le_sup_left.trans le_sup_left,
      le_sup_right.trans le_sup_left, fun x ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
x : (↑(Y.nonDegenerate n) : Type u)
pos :
  ∀ (hx : Membership.mem (γ := Set (Y _⦋n⦌)) ((Subcomplex.range i).obj (op ⦋n⦌)) (↑x : Y _⦋n⦌)),
    Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤
      Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
        ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
          ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)
neg :
  ∀ (hx : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)),
    Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤
      Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
        ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
          ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)
⊢ Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤
    Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
      ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
        ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)

Tactic:
by_cases hx : x.1 ∈ (Subcomplex.range i).obj _

Premises used: SSet.Subcomplex.range, CategoryTheory.Subfunctor.obj, Subtype.val
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
x : (↑(Y.nonDegenerate n) : Type u)
hx : Membership.mem (γ := Set (Y _⦋n⦌)) ((Subcomplex.range i).obj (op ⦋n⦌)) (↑x : Y _⦋n⦌)
⊢ Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤ Subcomplex.range i

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
x : (↑(Y.nonDegenerate n) : Type u)
hx : Membership.mem (γ := Set (Y _⦋n⦌)) ((Subcomplex.range i).obj (op ⦋n⦌)) (↑x : Y _⦋n⦌)
⊢ Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤
    Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
      ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
        ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)

Tactic:
exact le_trans (le_trans (by simpa) le_sup_left) le_sup_left

Premises used: le_sup_left, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
x : (↑(Y.nonDegenerate n) : Type u)
hx : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤ Subcomplex.ofSimplex (↑x : Y _⦋n⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
x : (↑(Y.nonDegenerate n) : Type u)
hx : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤
    ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)

Tactic:
exact le_trans (by rfl) (le_iSup _ hx)

Premises used: le_iSup, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
x : (↑(Y.nonDegenerate n) : Type u)
hx : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤
    Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
      ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
        ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌)

Tactic:
exact (le_trans (by exact le_trans (by rfl) (le_iSup _ hx))
        (le_iSup _ x)).trans le_sup_right

Premises used: le_iSup, le_sup_right, LE.le.trans, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
a :
  (Subcomplex.range i ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) (n + 1) ∧
      (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) (n + 1)) ∧
    ∀ (i_1 : (↑(Y.nonDegenerate n) : Type u)) (i_2 : (↑i_1 : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)),
      Subcomplex.ofSimplex (↑i_1 : Y _⦋n⦌) ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) (n + 1)
⊢ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ⊔
      ⨆ (x : (↑(Y.nonDegenerate n) : Type u)),
        ⨆ (_ : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex (↑x : Y _⦋n⦌) ≤
    Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) (n + 1)

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Premises used: sup_le_iff, iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ n ≤ n + 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
x : (↑(Y.nonDegenerate n) : Type u)
h : (↑x : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ n < n + 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ (Subcomplex.range i ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) (n + 1) ∧
      (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) (n + 1)) ∧
    ∀ (i_1 : (↑(Y.nonDegenerate n) : Type u)) (i_2 : (↑i_1 : Y _⦋n⦌) ∉ (Subcomplex.range i).obj (op ⦋n⦌)),
      Subcomplex.ofSimplex (↑i_1 : Y _⦋n⦌) ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) (n + 1)

Tactic:
exact ⟨⟨le_sup_left, (Y.skeleton.monotone (by simp)).trans le_sup_right⟩,
      fun _ _ ↦ (Y.ofSimplex_le_skeleton _ (by simp)).trans le_sup_right⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
d' : ℕ
⊢ Membership.mem (γ := Set (Y _⦋d⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d') (op ⦋d⦌))
      c.simplex ↔
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (Y _⦋d⦌)))
        (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⦌)))
        c.simplex ∨
      d < d'

Tactic:
simp [skeletonOfMono, Y.mem_skeleton_obj_iff_of_nonDegenerate ⟨_, c.nonDegenerate⟩ d']

Premises used: SSet.mem_skeleton_obj_iff_of_nonDegenerate, Subtype.mk, SSet.relativeCellComplexOfMono.Cell.nonDegenerate, SSet.skeletonOfMono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ Subcomplex.range c.map ≤ (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)

Tactic:
simp [map, Subcomplex.range_eq_ofSimplex, mem_skeletonOfMono_obj_iff]

Premises used: SSet.Subcomplex.range_eq_ofSimplex, SSet.relativeCellComplexOfMono.Cell.mem_skeletonOfMono_obj_iff, SSet.relativeCellComplexOfMono.Cell.map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
rw :
  ∂Δ[d] ≤ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ∧
    Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ≠ ⊤
⊢ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map = ∂Δ[d]

Tactic:
rw [stdSimplex.eq_boundary_iff]

Premises used: SSet.stdSimplex.eq_boundary_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∂Δ[d] ≤ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ∧
    Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ≠ ⊤

Tactic:
⟨?_, fun h ↦ c.notMem ?_⟩

Premises used: SSet.relativeCellComplexOfMono.Cell.notMem, And.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
refine_1 : ∂Δ[d] ≤ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map
refine_2 :
  ∀ (h : Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map = ⊤),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (Y _⦋d⦌)))
      (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⦌)))
      c.simplex
⊢ ∂Δ[d] ≤ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ∧
    Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ≠ ⊤

Tactic:
refine ⟨?_, fun h ↦ c.notMem ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
refine_1 :
  ∀ (n : ℕ) (x : (↑(Δ[d].nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) (↑x : Δ[d] _⦋n⦌) →
      Membership.mem (γ := Set (Δ[d] _⦋n⦌))
        ((Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map).obj (op ⦋n⦌)) (↑x : Δ[d] _⦋n⦌)
⊢ ∂Δ[d] ≤ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

Premises used: SSet.Subcomplex.le_iff_contains_nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : ℕ
y : Δ[d] _⦋n⦌
hy₁ : Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (Δ[d].nonDegenerate n) y
hy₂ :
  Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌))
    (↑(Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (Δ[d].nonDegenerate n) x) y hy₁) :
      Δ[d] _⦋n⦌)
⊢ Membership.mem (γ := Set (∂Δ[d].toSSet _⦋n⦌)) (∂Δ[d].toSSet.nonDegenerate n)
    (Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) x) y hy₂)

Tactic:
simpa [Subcomplex.mem_nonDegenerate_iff]

Premises used: SSet.Subcomplex.mem_nonDegenerate_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : ℕ
y : Δ[d] _⦋n⦌
hy₁ : Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (Δ[d].nonDegenerate n) y
hy₂ :
  Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌))
    (↑(Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (Δ[d].nonDegenerate n) x) y hy₁) :
      Δ[d] _⦋n⦌)
⊢ n < d

Tactic:
have : n < d := dim_lt_of_nonDegenerate (X := ∂Δ[d])
      ⟨⟨y, hy₂⟩, by simpa [Subcomplex.mem_nonDegenerate_iff]⟩ d
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : ℕ
y : Δ[d] _⦋n⦌
hy₁ : Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (Δ[d].nonDegenerate n) y
hy₂ :
  Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌))
    (↑(Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (Δ[d].nonDegenerate n) x) y hy₁) :
      Δ[d] _⦋n⦌)
this : n < d
⊢ Membership.mem (γ := Set (Δ[d] _⦋n⦌))
    ((Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map).obj (op ⦋n⦌))
    (↑(Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (Δ[d].nonDegenerate n) x) y hy₁) :
      Δ[d] _⦋n⦌)

Tactic:
simp [skeletonOfMono_obj_eq_top i this]

Premises used: SSet.skeletonOfMono_obj_eq_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
h : Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map = ⊤
⊢ Membership.mem.{u, u} (α := Δ[d] _⦋d⦌) (γ := Set (Δ[d] _⦋d⦌)) (Subfunctor.obj ⊤ (op ⦋d⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋d⦌) → Δ[d] _⦋d⦌) (𝟙 ⦋d⦌) : Δ[d] _⦋d⦌)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
h : Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map = ⊤
⊢ Membership.mem (α := Δ[d] _⦋d⦌) (γ := Set (Δ[d] _⦋d⦌))
    ((Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map).obj (op ⦋d⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋d⦌) → Δ[d] _⦋d⦌) (𝟙 ⦋d⦌) : Δ[d] _⦋d⦌)

Tactic:
have := h.symm.le _ (show stdSimplex.objEquiv.symm (𝟙 ⦋d⦌) ∈ _ by simp)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
h : Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map = ⊤
this :
  Membership.mem (α := Δ[d] _⦋d⦌) (γ := Set (Δ[d] _⦋d⦌))
    ((Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map).obj (op ⦋d⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋d⦌) → Δ[d] _⦋d⦌) (𝟙 ⦋d⦌) : Δ[d] _⦋d⦌)
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (Y _⦋d⦌)))
    (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⦌)))
    c.simplex

Tactic:
simpa [mem_skeletonOfMono_obj_iff]

Premises used: SSet.relativeCellComplexOfMono.Cell.mem_skeletonOfMono_obj_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
a : sigmaStdSimplex i d _⦋n⦌
⊢ ∃ (c : Cell i d) (x : Δ[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⦌))
        x =
      a

Tactic:
Cofan.inj_jointly_surjective_of_isColimit
    (isColimitCofanMkObjOfIsColimit ((CategoryTheory.evaluation _ _).obj _) _ _
      (coproductIsCoproduct _)) a

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.Cofan.inj_jointly_surjective_of_isColimit, CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ Subcomplex.range (∂Δ[d].ι ≫ c.map) ≤ (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d

Tactic:
simp [Subcomplex.range_comp, Subcomplex.image_le_iff]

Premises used: SSet.Subcomplex.image_le_iff, SSet.Subcomplex.range_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ d ≤ d + 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
h :
  ∀ (c : Cell i d),
    Sigma.ι (C := SSet) (fun (x : Cell i d) ↦ ∂Δ[d].toSSet) c ≫ t i d ≫ r i d =
      Sigma.ι (C := SSet) (fun (x : Cell i d) ↦ ∂Δ[d].toSSet) c ≫ l i d ≫ b i d
⊢ t i d ≫ r i d = l i d ≫ b i d

Tactic:
ext c : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ Sigma.ι (C := SSet) (fun (x : Cell i d) ↦ ∂Δ[d].toSSet) c ≫ t i d ≫ r i d =
    Sigma.ι (C := SSet) (fun (x : Cell i d) ↦ ∂Δ[d].toSSet) c ≫ l i d ≫ b i d

Tactic:
simp [← cancel_mono (Subcomplex.ι _), Sigma.ι_desc_assoc]

Premises used: CategoryTheory.Limits.Sigma.ι_desc_assoc, CategoryTheory.cancel_mono, SSet.Subcomplex.ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ c.ιSigmaBoundary ≫ t i d ≫ Subcomplex.ι ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) =
    ∂Δ[d].ι ≫ c.ιSigmaStdSimplex ≫ b i d ≫ Subcomplex.ι ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))

Tactic:
simp [Sigma.ι_desc_assoc]

Premises used: CategoryTheory.Limits.Sigma.ι_desc_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ c.ιSigmaBoundary ≫ l i d = ∂Δ[d].ι ≫ c.ιSigmaStdSimplex

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ c.ιSigmaStdSimplex ≫ b i d ≫ Subcomplex.ι ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) = c.map

Tactic:
simp [Sigma.ι_desc_assoc]

Premises used: CategoryTheory.Limits.Sigma.ι_desc_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : SimplexCategory
f : n ⟶ ⦋d⦌
simp :
  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 : Δ[d].obj (op n)) → (sigmaStdSimplex i d).obj (op n))
              ((Equiv.symm stdSimplex.objEquiv : (a : n ⟶ ⦋d⦌) → Δ[d].obj (op n)) f : Δ[d].obj (op n)))) :
        Y.obj (op n)) :
      Y.obj (op n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((c.ιSigmaStdSimplex ≫ b i d ≫ Subcomplex.ι ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).app
              (op n)) :
          (a : Δ[d].obj (op n)) → Y.obj (op n))
        ((Equiv.symm stdSimplex.objEquiv : (a : n ⟶ ⦋d⦌) → Δ[d].obj (op n)) f : Δ[d].obj (op n)) :
      Y.obj (op n))
⊢ 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 : Δ[d].obj (op n)) → (sigmaStdSimplex i d).obj (op n))
              ((Equiv.symm stdSimplex.objEquiv : (a : n ⟶ ⦋d⦌) → Δ[d].obj (op n)) f : Δ[d].obj (op n)))) :
        Y.obj (op n)) :
      Y.obj (op n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) : (a : Y _⦋d⦌) → Y.obj (op n)) c.simplex : Y.obj (op n))

Tactic:
simp only [← yonedaEquiv_symm_app_objEquiv_symm, ← ι_b_ι]

Premises used: SSet.relativeCellComplexOfMono.Cell.ι_b_ι, SSet.yonedaEquiv_symm_app_objEquiv_symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : SimplexCategory
f : n ⟶ ⦋d⦌
⊢ 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 : Δ[d].obj (op n)) → (sigmaStdSimplex i d).obj (op n))
              ((Equiv.symm stdSimplex.objEquiv : (a : n ⟶ ⦋d⦌) → Δ[d].obj (op n)) f : Δ[d].obj (op n)))) :
        Y.obj (op n)) :
      Y.obj (op n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((c.ιSigmaStdSimplex ≫ b i d ≫ Subcomplex.ι ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).app
              (op n)) :
          (a : Δ[d].obj (op n)) → Y.obj (op n))
        ((Equiv.symm stdSimplex.objEquiv : (a : n ⟶ ⦋d⦌) → Δ[d].obj (op n)) f : Δ[d].obj (op n)) :
      Y.obj (op n))

Tactic:
dsimp +instances
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
refine :
  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))
⊢ IsLimit (F := cospan (r i d) (b i d) ⋙ evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌)
    (Functor.mapCone (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌) (PullbackCone.mk (t i d) (l i d) ⋯))

Tactic:
refine (isLimitMapConePullbackConeEquiv _ _).2
      (IsPullback.isLimit ?_)

Premises used: CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.invFun, CategoryTheory.IsPullback.isLimit