awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w : Epi f
y : (↑(X.nonDegenerate j) : Type u)
⊢ Subcomplex.ofSimplex (↑y : X _⦋j⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) n

Tactic:
exact le_trans (by exact le_trans (by rfl) (le_iSup _ y))
    (le_iSup _ ⟨j, lt_of_le_of_lt
      (SimplexCategory.len_le_of_epi f) hi⟩)

Premises used: le_iSup, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d n : ℕ
h : d < n
rw : LE.le.{u} (α := Set (X _⦋d⦌)) ⊤ (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌))
⊢ Eq.{u + 1} (α := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌)) ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d n : ℕ
h : d < n
x : X _⦋d⦌
_ :
  Membership.mem (γ := Set (X _⦋d⦌)) ⊤ x →
    Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌)) x
⊢ Membership.mem (γ := Set (X _⦋d⦌)) ⊤ x →
    Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌)) x

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d n : ℕ
h : d < n
x : X _⦋d⦌
h_1 : Membership.mem (γ := Set (X _⦋d⦌)) ⊤ x
⊢ Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌)) x

Tactic:
mem_skeleton _ _ h

Premises used: SSet.mem_skeleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d n : ℕ
h : d < n
x : X _⦋d⦌
h_1 : Membership.mem (γ := Set (X _⦋d⦌)) ⊤ x
⊢ Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌)) x

Tactic:
exact mem_skeleton _ _ h

Premises used: SSet.mem_skeleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
i : ℕ
x : X _⦋i⦌
n : ℕ
hi : i < n
⊢ Subcomplex.ofSimplex x ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) n

Tactic:
simpa using X.mem_skeleton x hi

Premises used: SSet.mem_skeleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d : ℕ
x : (↑(X.nonDegenerate d) : Type u)
n : ℕ
⊢ Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌)) (↑x : X _⦋d⦌) ↔
    d < n

Tactic:
⟨fun h ↦ ?_, fun _ ↦ X.mem_skeleton _⟩

Premises used: SSet.mem_skeleton, Iff.intro, Subtype.val
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d : ℕ
x : (↑(X.nonDegenerate d) : Type u)
n : ℕ
refine :
  ∀
    (h :
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌))
        (↑x : X _⦋d⦌)),
    d < n
⊢ Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌)) (↑x : X _⦋d⦌) ↔
    d < n

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ X.mem_skeleton _⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d : ℕ
x : (↑(X.nonDegenerate d) : Type u)
n : ℕ
h : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌)) (↑x : X _⦋d⦌)
obtain :
  ∀ (x : X _⦋d⦌) (hx : x ∈ X.nonDegenerate d)
    (h :
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌))
        (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌)),
    d < n
⊢ d < n

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d n : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
h :
  Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌))
    (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌)
⊢ ∃ (i : Fin n) (i_1 : X _⦋(↑i : ℕ)⦌),
    Membership.mem (γ := Set (X _⦋(↑i : ℕ)⦌)) (X.nonDegenerate (↑i : ℕ)) i_1 ∧
      Membership.mem (γ := Set (X _⦋d⦌)) ((Subcomplex.ofSimplex i_1).obj (op ⦋d⦌)) x

Tactic:
simp only [skeleton, OrderHom.coe_mk, Subfunctor.iSup_obj,
    Set.iUnion_coe_set, Set.mem_iUnion, exists_prop] at h

Premises used: Set.mem_iUnion, SSet.skeleton, Set.iUnion_coe_set, exists_prop, OrderHom.coe_mk, CategoryTheory.Subfunctor.iSup_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d n : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
h :
  ∃ (i : Fin n) (i_1 : X _⦋(↑i : ℕ)⦌),
    Membership.mem (γ := Set (X _⦋(↑i : ℕ)⦌)) (X.nonDegenerate (↑i : ℕ)) i_1 ∧
      Membership.mem (γ := Set (X _⦋d⦌)) ((Subcomplex.ofSimplex i_1).obj (op ⦋d⦌)) x
obtain :
  ∀ (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⦌))),
    d < n
⊢ d < n

Tactic:
obtain ⟨⟨i, hi⟩, y, hy, ⟨f⟩, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
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⦌))
⊢ Mono f

Tactic:
have := X.mono_of_nonDegenerate ⟨_, hx⟩ f y rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
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 ≤ i

Tactic:
have : d ≤ i := SimplexCategory.len_le_of_mono f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
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_1 : Mono f
this : d ≤ i
⊢ d < n

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
⊢ Eq (α := X.Subcomplex) ((X.skeleton : (a : ℕ) → X.Subcomplex) 0 : X.Subcomplex) (⊥ : X.Subcomplex)

Tactic:
simp [skeleton]

Premises used: SSet.skeleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
⊢ LE.le.{u} (α := X.Subcomplex) (⨆ (n : ℕ), (X.skeleton : (a : ℕ) → X.Subcomplex) n) ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
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⦌)
⊢ LE.le.{u} (α := X.Subcomplex) ⊤ (⨆ (n : ℕ), (X.skeleton : (a : ℕ) → X.Subcomplex) n)

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

Premises used: SSet.Subcomplex.le_iff_contains_nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
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⦌)
⊢ 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:
_
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
h : Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj ⊤ (op ⦋n⦌)) (↑x : X _⦋n⦌)
simp :
  ∃ (i : ℕ),
    Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) i) (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:
simp only [Subfunctor.iSup_obj, Set.mem_iUnion]

Premises used: Set.mem_iUnion, CategoryTheory.Subfunctor.iSup_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
h : Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj ⊤ (op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ n < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
h : Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj ⊤ (op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ ∃ (i : ℕ),
    Membership.mem (γ := Set (X _⦋n⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) i) (op ⦋n⦌)) (↑x : X _⦋n⦌)

Tactic:
exact ⟨n + 1, mem_skeleton _ _ (by lia)⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
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)
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)
⊢ 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)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n : ℕ
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⦌)
⊢ 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)

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n d : ℕ
hd : d < n + 1
x : (↑(X.nonDegenerate (↑(⟨d, hd⟩ : Fin (n + 1)) : ℕ)) : Type u)
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⦌)
⊢ 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

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
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⦌)
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⦌)
⊢ 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

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n d : ℕ
hd_1 : d < n + 1
hd_2 : d ≤ n
x : (↑(X.nonDegenerate (↑(⟨d, hd_1⟩ : Fin (n + 1)) : ℕ)) : Type u)
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:
(X.ofSimplex_le_skeleton _ hd).trans le_sup_left

Premises used: SSet.ofSimplex_le_skeleton, le_sup_left, setOf, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n d : ℕ
hd_1 : d < n + 1
hd_2 : d ≤ n
x : (↑(X.nonDegenerate (↑(⟨d, hd_1⟩ : Fin (n + 1)) : ℕ)) : Type u)
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:
exact (X.ofSimplex_le_skeleton _ hd).trans le_sup_left

Premises used: SSet.ofSimplex_le_skeleton, le_sup_left, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d : ℕ
hd_1 : d < d + 1
hd : d ≤ d
x : (↑(X.nonDegenerate (↑(⟨d, hd_1⟩ : Fin (d + 1)) : ℕ)) : Type u)
⊢ Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd_1⟩ : ℕ)⦌) ≤ Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd_1⟩ : ℕ)⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
d : ℕ
hd_1 : d < d + 1
hd : d ≤ d
x : (↑(X.nonDegenerate (↑(⟨d, hd_1⟩ : Fin (d + 1)) : ℕ)) : Type u)
⊢ Subcomplex.ofSimplex (↑x : X _⦋(↑⟨d, hd_1⟩ : ℕ)⦌) ≤
    (X.skeleton : (a : ℕ) → X.Subcomplex) d ⊔
      ⨆ (x : (↑(X.nonDegenerate d) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋d⦌)

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

Premises used: le_iSup, le_sup_right, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
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) ∧
    ∀ (i : (↑(X.nonDegenerate n) : Type u)),
      Subcomplex.ofSimplex (↑i : X _⦋n⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1)
⊢ 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:
simp only [sup_le_iff, iSup_le_iff]

Premises used: sup_le_iff, iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
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)
a₁ :
  ∀ (i : (↑(X.nonDegenerate n) : Type u)),
    Subcomplex.ofSimplex (↑i : X _⦋n⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1)
⊢ 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:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n : ℕ
⊢ n ≤ n + 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
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)

Tactic:
exact X.skeleton.monotone (by simp)

Premises used: OrderHom.monotone, SSet.skeleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
⊢ n < n + 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
⊢ Subcomplex.ofSimplex (↑x : X _⦋n⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) (n + 1)

Tactic:
apply X.ofSimplex_le_skeleton _ (by simp)

Premises used: SSet.ofSimplex_le_skeleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n m : ℕ
h : n ≤ m
simp : (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) m
⊢ Subcomplex.range i ⊔ (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]

Premises used: le_sup_left, sup_le_iff, true_and
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n m : ℕ
h : n ≤ m
⊢ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) m

Tactic:
le_trans (Y.skeleton.monotone h) le_sup_right

Premises used: OrderHom.monotone, SSet.skeleton, le_sup_right, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n m : ℕ
h : n ≤ m
⊢ (Y.skeleton : (a : ℕ) → Y.Subcomplex) n ≤ Subcomplex.range i ⊔ (Y.skeleton : (a : ℕ) → Y.Subcomplex) m

Tactic:
exact le_trans (Y.skeleton.monotone h) le_sup_right

Premises used: OrderHom.monotone, SSet.skeleton, le_sup_right, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ LE.le (α := Y.Subcomplex) ((Y.skeleton : (a : ℕ) → Y.Subcomplex) n : Y.Subcomplex)
    ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n : Y.Subcomplex)

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
⊢ (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) 0 = Subcomplex.range i

Tactic:
simp [skeletonOfMono]

Premises used: SSet.skeletonOfMono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
⊢ LE.le.{u} (α := Y.Subcomplex) (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n) ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
apply : LE.le.{u} (α := Y.Subcomplex) ⊤ (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n)
⊢ Eq.{u + 1} (α := Y.Subcomplex) (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n) ⊤

Tactic:
apply le_antisymm (by simp)

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
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)
⊢ LE.le.{u} (α := Y.Subcomplex) ⊤ (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n)

Tactic:
rw [← Y.iSup_skeleton, iSup_le_iff]

Premises used: SSet.iSup_skeleton, iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ LE.le (α := Y.Subcomplex) ((Y.skeleton : (a : ℕ) → Y.Subcomplex) n : Y.Subcomplex)
    (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n : Y.Subcomplex)

Tactic:
le_trans (skeleton_le_skeletonOfMono i n) (le_iSup _ n)

Premises used: SSet.skeleton_le_skeletonOfMono, le_iSup, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ LE.le (α := Y.Subcomplex) ((Y.skeleton : (a : ℕ) → Y.Subcomplex) n : Y.Subcomplex)
    (⨆ (n : ℕ), (skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n : Y.Subcomplex)

Tactic:
exact le_trans (skeleton_le_skeletonOfMono i n) (le_iSup _ n)

Premises used: SSet.skeleton_le_skeletonOfMono, le_iSup, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : (↑(Y.nonDegenerate d) : Type u)
n : ℕ
⊢ Membership.mem (γ := Set (Y _⦋d⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n) (op ⦋d⦌))
      (↑x : Y _⦋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⦌)))
        (↑x : Y _⦋d⦌) ∨
      d < n

Tactic:
simp [skeletonOfMono, mem_skeleton_obj_iff_of_nonDegenerate]

Premises used: SSet.mem_skeleton_obj_iff_of_nonDegenerate, SSet.skeletonOfMono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
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⦌))
⊢ Eq.{u + 1} (α := Set (Y _⦋d⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) n) (op ⦋d⦌)) ⊤

Tactic:
rw [← top_le_iff, ← Y.skeleton_obj_eq_top h]

Premises used: SSet.skeleton_obj_eq_top, top_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ 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:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ 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:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
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⦌)
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)
⊢ 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

Premises used: le_antisymm