awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (hypothesis)
Goal:
X : SSet
d n i : ℕ
hi : i < n
y : X _⦋(↑(⟨i, hi⟩ : Fin n) : ℕ)⦌
hy : Membership.mem (γ := Set (X _⦋(↑(⟨i, hi⟩ : Fin n) : ℕ)⦌)) (X.nonDegenerate (↑(⟨i, hi⟩ : Fin n) : ℕ)) y
f : unop (op ⦋d⦌) ⟶ unop (op ⦋(↑(⟨i, hi⟩ : Fin n) : ℕ)⦌)
hx :
  Membership.mem (α := X _⦋d⦌) (X.nonDegenerate d)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (op f)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(↑⟨i, hi⟩ : ℕ)⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
        y :
      (fun (X : Type u) ↦ X) (X _⦋d⦌))
this : Mono f
⊢ d < n
have this₁ : d ≤ i
Tactic: have : d ≤ i := SimplexCategory.len_le_of_mono f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
⊢ LE.le.{u} (α := X.Subcomplex) ⊤ (⨆ (n : ℕ), (X.skeleton : (a : ℕ) → X.Subcomplex) n)
have rw : ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
  Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj ⊤ (op ⦋n⦌)) (↑x : X _⦋n⦌) →
    Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj (⨆ (n : ℕ), (X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋n⦌))
      (↑x : X _⦋n⦌)
Tactic: rw [Subcomplex.le_iff_contains_nonDegenerate]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
h : Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj ⊤ (op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj (⨆ (n : ℕ), (X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋n⦌))
    (↑x : X _⦋n⦌)
have simp : ∃ (i : ℕ),
  Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) i) (op ⦋n⦌)) (↑x : X _⦋n⦌)
Tactic: simp only [Subfunctor.iSup_obj, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n : ℕ
⊢ Eq (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex)
    ((X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
        ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌) :
      X.Subcomplex)
have a : LE.le (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex)
  ((X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
      ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌) :
    X.Subcomplex)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n : ℕ
a :
  LE.le (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex)
    ((X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
        ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌) :
      X.Subcomplex)
⊢ Eq (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex)
    ((X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
        ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌) :
      X.Subcomplex)
have a₁ : LE.le (α := X.Subcomplex)
  ((X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
      ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌) :
    X.Subcomplex)
  ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n : ℕ
⊢ LE.le (α := X.Subcomplex)
    (⨆ (i : Fin (n + 1)), ⨆ (x : (↑(X.nonDegenerate (↑i : ℕ)) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋(↑i : ℕ)⦌) :
      X.Subcomplex)
    ((X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
        ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌) :
      X.Subcomplex)
have a : ∀ (i : Fin (n + 1)) (i_1 : (↑(X.nonDegenerate (↑i : ℕ)) : Type u)),
  Subcomplex.ofSimplex (↑i_1 : X _⦋(↑i : ℕ)⦌) ≤
    (X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
      ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌)
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n d : ℕ
hd : d < n + 1
x : (↑(X.nonDegenerate (↑(⟨d, hd⟩ : Fin (n + 1)) : ℕ)) : Type u)
⊢ Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd⟩ : ℕ)⦌) ≤
    (X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
      ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌)
have a : ∀ (hd_1 : d ≤ n) (x : (↑(X.nonDegenerate (↑(⟨d, hd⟩ : Fin (n + 1)) : ℕ)) : Type u)),
  Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd⟩ : ℕ)⦌) ≤
    (X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
      ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌)
Tactic: rw [Nat.lt_succ_iff] at hd
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n d : ℕ
hd_1 : d < n + 1
hd : d ≤ n
x : (↑(X.nonDegenerate (↑(⟨d, hd_1⟩ : Fin (n + 1)) : ℕ)) : Type u)
⊢ Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd_1⟩ : ℕ)⦌) ≤
    (X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
      ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌)
have a : ∀ (hd : d < n),
  Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd_1⟩ : ℕ)⦌) ≤
    (X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
      ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌)
Tactic: obtain hd | rfl := hd.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n d : ℕ
hd_1 : d < n + 1
hd : d ≤ n
x : (↑(X.nonDegenerate (↑(⟨d, hd_1⟩ : Fin (n + 1)) : ℕ)) : Type u)
a :
  ∀ (hd : d < n),
    Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd_1⟩ : ℕ)⦌) ≤
      (X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
        ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌)
⊢ Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd_1⟩ : ℕ)⦌) ≤
    (X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
      ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌)
have a₁ : ∀ (hd : d < d + 1) (hd_2 : d ≤ d) (x : (↑(X.nonDegenerate (↑(⟨d, hd⟩ : Fin (d + 1)) : ℕ)) : Type u)),
  Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd⟩ : ℕ)⦌) ≤
    (X.skeleton : (a : ℕ) → X.Subcomplex) d ⊔
      ⨆ (x : (↑(X.nonDegenerate d) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋d⦌)
Tactic: obtain hd | rfl := hd.lt_or_eq
Cleared hypotheses: n, hd_1, hd, x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n : ℕ
⊢ LE.le (α := X.Subcomplex)
    ((X.skeleton : (a : ℕ) → X.Subcomplex) n ⊔
        ⨆ (x : (↑(X.nonDegenerate n) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋n⦌) :
      X.Subcomplex)
    ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex)
have a : LE.le (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) n : X.Subcomplex)
    ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex) ∧
  ∀ (i : (↑(X.nonDegenerate n) : Type u)),
    Subcomplex.ofSimplex (↑i : X _⦋n⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1)
Tactic: simp only [sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n : ℕ
⊢ LE.le (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) n : X.Subcomplex)
      ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex) ∧
    ∀ (i : (↑(X.nonDegenerate n) : Type u)),
      Subcomplex.ofSimplex (↑i : X _⦋n⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1)
have a : LE.le (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) n : X.Subcomplex)
  ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
n : ℕ
a :
  LE.le (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) n : X.Subcomplex)
    ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex)
⊢ LE.le (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) n : X.Subcomplex)
      ((X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1) : X.Subcomplex) ∧
    ∀ (i : (↑(X.nonDegenerate n) : Type u)),
      Subcomplex.ofSimplex (↑i : X _⦋n⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1)
have a₁ : ∀ (i : (↑(X.nonDegenerate n) : Type u)),
  Subcomplex.ofSimplex (↑i : X _⦋n⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
n m : ℕ
h : n ≤ m
⊢ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤
    Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) m
have simp : (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) m
Tactic: simp only [sup_le_iff, le_sup_left, true_and]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
⊢ Eq.{u + 1} (α := Y.Subcomplex) (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n) ⊤
have apply : LE.le.{u} (α := Y.Subcomplex) ⊤ (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n)
Tactic: apply le_antisymm (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
⊢ LE.le.{u} (α := Y.Subcomplex) ⊤ (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n)
have rw : ∀ (i_1 : ℕ),
  LE.le (α := Y.Subcomplex) ((Y.skeleton : (a : ℕ) → Y.Subcomplex) i_1 : Y.Subcomplex)
    (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n : Y.Subcomplex)
Tactic: rw [← Y.iSup_skeleton, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ Eq.{u + 1} (α := Set (Y _⦋d⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n) (op ⦋d⦌)) ⊤
have rw : LE.le.{u} (α := Set (Y _⦋d⦌)) (Subfunctor.obj ((Y.skeleton : (a : ℕ) → Y.Subcomplex) n) (op ⦋d⦌))
  (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n) (op ⦋d⦌))
Tactic: rw [← top_le_iff, ← Y.skeleton_obj_eq_top h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : 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⦌)
have a : 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: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
a :
  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) =
    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⦌)
have a₁ : 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: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : 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⦌)
have 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⦌)
Tactic: simp only [sup_le_iff, iSup_le_iff, skeleton_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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⦌)
have 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⦌)
Tactic: refine ⟨le_sup_left.trans le_sup_left,
      le_sup_right.trans le_sup_left, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
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⦌)
have 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⦌)
Tactic: by_cases hx : x.1 ∈ (Subcomplex.range i).obj _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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⦌)
⊢ 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⦌)
have 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⦌)
Tactic: by_cases hx : x.1 ∈ (Subcomplex.range i).obj _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : 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 ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) (n + 1)
have 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)
Tactic: simp only [sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map = ∂Δ[d]
have rw : ∂Δ[d] ≤ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ∧
  Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ≠ ⊤
Tactic: rw [stdSimplex.eq_boundary_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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 ≠ ⊤
have refine_1 : ∂Δ[d] ≤ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map
Tactic: refine ⟨?_, fun h ↦ c.notMem ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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
⊢ ∂Δ[d] ≤ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ∧
    Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map ≠ ⊤
have 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
Tactic: refine ⟨?_, fun h ↦ c.notMem ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∂Δ[d] ≤ Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map
have 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⦌)
Tactic: rw [Subcomplex.le_iff_contains_nonDegenerate]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (hypothesis)
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] _⦋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⦌)
have this : n < d
Tactic: have : n < d := dim_lt_of_nonDegenerate (X := ∂Δ[d])
      ⟨⟨y, hy₂⟩, by simpa [Subcomplex.mem_nonDegenerate_iff]⟩ d
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (hypothesis)
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 (γ := 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
have 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⦌)
Tactic: have := h.symm.le _ (show stdSimplex.objEquiv.symm (𝟙 ⦋d⦌) ∈ _ by simp)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ t i d ≫ r i d = l i d ≫ b i d
have 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
Tactic: ext c : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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) (Y.map f.op) : (a : Y _⦋d⦌) → Y.obj (op n)) c.simplex : Y.obj (op n))
have 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))
Tactic: simp only [← yonedaEquiv_symm_app_objEquiv_symm, ← ι_b_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ 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) ⋯))
have 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))
Tactic: refine (isLimitMapConePullbackConeEquiv _ _).2
      (IsPullback.isLimit ?_)