awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
t : X.S
w : ℕ
w_1 : X _⦋w⦌
h :
  ∃ (h : { dim := w, simplex := w_1 : X.S }.dim = t.dim),
    ({ dim := w, simplex := w_1 : X.S }.cast h).simplex = t.simplex
h₁ : { dim := w, simplex := w_1 : X.S }.dim = t.dim
h₂ : ({ dim := w, simplex := w_1 : X.S }.cast h₁).simplex = t.simplex
obtain :
  ∀ (w_2 : ℕ) (w_3 : X _⦋w_2⦌),
    (∃ (h : { dim := w, simplex := w_1 : X.S }.dim = { dim := w_2, simplex := w_3 : X.S }.dim),
        ({ dim := w, simplex := w_1 : X.S }.cast h).simplex = { dim := w_2, simplex := w_3 }.simplex) →
      ∀ (h₁ : { dim := w, simplex := w_1 : X.S }.dim = { dim := w_2, simplex := w_3 : X.S }.dim)
        (h₂ : ({ dim := w, simplex := w_1 : X.S }.cast h₁).simplex = { dim := w_2, simplex := w_3 }.simplex),
        { dim := w, simplex := w_1 : X.S } = { dim := w_2, simplex := w_3 }
⊢ { dim := w, simplex := w_1 : X.S } = t

Tactic:
obtain ⟨_, _, rfl⟩ := t.mk_surjective

Premises used: SSet.S.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
w : ℕ
w_1 : X _⦋w⦌
w_2 : ℕ
w_3 : X _⦋w_2⦌
h :
  ∃ (h : { dim := w, simplex := w_1 : X.S }.dim = { dim := w_2, simplex := w_3 : X.S }.dim),
    ({ dim := w, simplex := w_1 : X.S }.cast h).simplex = { dim := w_2, simplex := w_3 }.simplex
h₁ : { dim := w, simplex := w_1 : X.S }.dim = { dim := w_2, simplex := w_3 : X.S }.dim
h₂ : ({ dim := w, simplex := w_1 : X.S }.cast h₁).simplex = { dim := w_2, simplex := w_3 }.simplex
⊢ { dim := w, simplex := w_1 : X.S } = { dim := w_2, simplex := w_3 }

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
n : ℕ
x y : X _⦋n⦌
⊢ { dim := n, simplex := x : X.S } = { dim := n, simplex := y } ↔ x = y

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ Subcomplex.ofSimplex x = { dim := n, simplex := x }.subcomplex

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s : X.S
d : ℕ
hd : s.dim = d
rw rw₁ : s.subcomplex = s.subcomplex
⊢ (s.cast hd).subcomplex = s.subcomplex

Tactic:
rw [cast_eq_self]

Premises used: SSet.S.cast_eq_self
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s t : X.S
⊢ s ≤ t ↔ s.subcomplex ≤ t.subcomplex

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s t : X.S
rw :
  (∃ (f : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex) ↔
    ∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex
⊢ s ≤ t ↔
    ∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex

Tactic:
rw [le_def, Subcomplex.ofSimplex_le_iff, Subfunctor.ofSection_obj, Set.mem_setOf_eq]

Premises used: CategoryTheory.Subfunctor.ofSection_obj, Set.mem_setOf_eq, SSet.Subcomplex.ofSimplex_le_iff, SSet.S.le_def
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
rw :
  ∃ (f_1 :
    ⦋dim.{u} (X := X)
          (mk (dim := m)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
              x))⦌ ⟶
      ⦋{ dim := n, simplex := x : X.S }.dim⦌),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (X _⦋dim.{u} (X := X)
            (mk (dim := m)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
                x))⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := n, simplex := x }.dim⦌)) →
              (fun (X : Type u) ↦ X)
                (X _⦋{ dim := m,
                      simplex :=
                        (ConcreteCategory.hom (X.map f.op) :
                            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
                          x }.dim⦌))
          { dim := n, simplex := x : X.S }.simplex :
        (fun (X : Type u) ↦ X)
          (X _⦋dim.{u} (X := X)
              (mk (dim := m)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
                  x))⦌))
      (simplex
          (mk (dim := m)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
              x)) :
        X _⦋dim.{u} (X := X)
            (mk (dim := m)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
                x))⦌)
⊢ mk (dim := m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) ≤
    { dim := n, simplex := x : X.S }

Tactic:
rw [le_iff]

Premises used: SSet.S.le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
⊢ ∃ (f_1 :
    ⦋dim.{u} (X := X)
          (mk (dim := m)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
              x))⦌ ⟶
      ⦋{ dim := n, simplex := x : X.S }.dim⦌),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (X _⦋dim.{u} (X := X)
            (mk (dim := m)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
                x))⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := n, simplex := x }.dim⦌)) →
              (fun (X : Type u) ↦ X)
                (X _⦋{ dim := m,
                      simplex :=
                        (ConcreteCategory.hom (X.map f.op) :
                            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
                          x }.dim⦌))
          { dim := n, simplex := x : X.S }.simplex :
        (fun (X : Type u) ↦ X)
          (X _⦋dim.{u} (X := X)
              (mk (dim := m)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
                  x))⦌))
      (simplex
          (mk (dim := m)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
              x)) :
        X _⦋dim.{u} (X := X)
            (mk (dim := m)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
                x))⦌)

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst : Mono f
mp :
  mk (dim := m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
          x) =
      { dim := n, simplex := x : X.S } →
    IsIso f
mpr :
  IsIso f →
    mk (dim := m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
          x) =
      { dim := n, simplex := x : X.S }
⊢ mk (dim := m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
          x) =
      { dim := n, simplex := x : X.S } ↔
    IsIso f

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst : Mono f
h :
  mk (dim := m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) =
    { dim := n, simplex := x : X.S }
mp :
  ∀ (x : X _⦋m⦌) (f : ⦋m⦌ ⟶ ⦋m⦌) [Mono f]
    (h :
      mk (dim := m)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
            x) =
        { dim := m, simplex := x : X.S }),
    IsIso f
⊢ IsIso f

Tactic:
obtain rfl := S.dim_eq_of_mk_eq h

Premises used: SSet.S.dim_eq_of_mk_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
m : ℕ
x : X _⦋m⦌
f : ⦋m⦌ ⟶ ⦋m⦌
inst : Mono f
h :
  mk (dim := m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) =
    { dim := m, simplex := x : X.S }
mp :
  ∀ [Mono (𝟙 ⦋m⦌)]
    (h :
      mk (dim := m)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋m⦌))) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
            x) =
        { dim := m, simplex := x : X.S }),
    IsIso (𝟙 ⦋m⦌)
⊢ IsIso f

Tactic:
obtain rfl := SimplexCategory.eq_id_of_mono f

Premises used: SimplexCategory.eq_id_of_mono, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
m : ℕ
x : X _⦋m⦌
inst : Mono (𝟙 ⦋m⦌)
h :
  mk (dim := m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋m⦌))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) =
    { dim := m, simplex := x : X.S }
⊢ IsIso (𝟙 ⦋m⦌)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst : Mono f
hf : IsIso f
mpr :
  ∀ (x : X _⦋m⦌) (f : ⦋m⦌ ⟶ ⦋m⦌) [Mono f] (hf : IsIso f),
    mk (dim := m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
          x) =
      { dim := m, simplex := x : X.S }
⊢ mk (dim := m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) =
    { dim := n, simplex := x : X.S }

Tactic:
obtain rfl := SimplexCategory.eq_of_isIso f

Premises used: SimplexCategory.eq_of_isIso, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
m : ℕ
x : X _⦋m⦌
f : ⦋m⦌ ⟶ ⦋m⦌
inst : Mono f
hf : IsIso f
mpr :
  ∀ [Mono (𝟙 ⦋m⦌)] (hf : IsIso (𝟙 ⦋m⦌)),
    mk (dim := m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋m⦌))) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
          x) =
      { dim := m, simplex := x : X.S }
⊢ mk (dim := m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) =
    { dim := m, simplex := x : X.S }

Tactic:
obtain rfl := SimplexCategory.eq_id_of_isIso f

Premises used: SimplexCategory.eq_id_of_isIso, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
m : ℕ
x : X _⦋m⦌
inst : Mono (𝟙 ⦋m⦌)
hf : IsIso (𝟙 ⦋m⦌)
⊢ mk (dim := m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋m⦌))) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) =
    { dim := m, simplex := x : X.S }

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ X.S

Tactic:
exact S.mk x

Premises used: SSet.S.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
x y : X.S
rw :
  (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
          y.simplex =
        x.simplex) ↔
    Nonempty
      (Quiver.Hom (V := Functor.Elements X) ((equivElements : (a : X.S) → Functor.Elements X) y : Functor.Elements X)
        ((equivElements : (a : X.S) → Functor.Elements X) x : Functor.Elements X))
⊢ x ≤ y ↔
    Nonempty
      (Quiver.Hom (V := Functor.Elements X) ((equivElements : (a : X.S) → Functor.Elements X) y : Functor.Elements X)
        ((equivElements : (a : X.S) → Functor.Elements X) x : Functor.Elements X))

Tactic:
rw [le_iff]

Premises used: SSet.S.le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
x y : X.S
mp :
  (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
          y.simplex =
        x.simplex) →
    Nonempty
      (Quiver.Hom (V := Functor.Elements X) ((equivElements : (a : X.S) → Functor.Elements X) y : Functor.Elements X)
        ((equivElements : (a : X.S) → Functor.Elements X) x : Functor.Elements X))
mpr :
  Nonempty
      (Quiver.Hom (V := Functor.Elements X) ((equivElements : (a : X.S) → Functor.Elements X) y : Functor.Elements X)
        ((equivElements : (a : X.S) → Functor.Elements X) x : Functor.Elements X)) →
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
          y.simplex =
        x.simplex
⊢ (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
          y.simplex =
        x.simplex) ↔
    Nonempty
      (Quiver.Hom (V := Functor.Elements X) ((equivElements : (a : X.S) → Functor.Elements X) y : Functor.Elements X)
        ((equivElements : (a : X.S) → Functor.Elements X) x : Functor.Elements X))

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
      y.simplex =
    x.simplex
⊢ Nonempty
    (Quiver.Hom (V := Functor.Elements X) ((equivElements : (a : X.S) → Functor.Elements X) y : Functor.Elements X)
      ((equivElements : (a : X.S) → Functor.Elements X) x : Functor.Elements X))

Tactic:
⟨⟨f.op, hf⟩⟩

Premises used: Quiver.Hom.op, Nonempty.intro, Subtype.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
      y.simplex =
    x.simplex
⊢ Nonempty
    (Quiver.Hom (V := Functor.Elements X) ((equivElements : (a : X.S) → Functor.Elements X) y : Functor.Elements X)
      ((equivElements : (a : X.S) → Functor.Elements X) x : Functor.Elements X))

Tactic:
exact ⟨⟨f.op, hf⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
x y : X.S
f :
  Quiver.Hom (V := SimplexCategoryᵒᵖ)
    (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) y))
    (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) x))
hf :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (X.obj
        (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) x))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) :
          (a : (fun (X : Type u) ↦ X) (X.obj ((equivElements : (a : X.S) → Functor.Elements X) y).fst)) →
            (fun (X : Type u) ↦ X) (X.obj ((equivElements : (a : X.S) → Functor.Elements X) x).fst))
        (Sigma.snd (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) y)) :
      (fun (X : Type u) ↦ X)
        (X.obj
          (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c)
            ((equivElements : (a : X.S) → Functor.Elements X) x))))
    (Sigma.snd (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) x) :
      X.obj
        (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) x)))
⊢ ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
        y.simplex =
      x.simplex

Tactic:
⟨f.unop, hf⟩

Premises used: Quiver.Hom.unop, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
x y : X.S
f :
  Quiver.Hom (V := SimplexCategoryᵒᵖ)
    (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) y))
    (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) x))
hf :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (X.obj
        (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) x))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) :
          (a : (fun (X : Type u) ↦ X) (X.obj ((equivElements : (a : X.S) → Functor.Elements X) y).fst)) →
            (fun (X : Type u) ↦ X) (X.obj ((equivElements : (a : X.S) → Functor.Elements X) x).fst))
        (Sigma.snd (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) y)) :
      (fun (X : Type u) ↦ X)
        (X.obj
          (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c)
            ((equivElements : (a : X.S) → Functor.Elements X) x))))
    (Sigma.snd (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) x) :
      X.obj
        (Sigma.fst (β := fun (c : SimplexCategoryᵒᵖ) ↦ X.obj c) ((equivElements : (a : X.S) → Functor.Elements X) x)))
⊢ ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
        y.simplex =
      x.simplex

Tactic:
exact ⟨f.unop, hf⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X Y : SSet
e : X ≅ Y
x : X.S
⊢ (fun (s : Y.S) ↦
        (mk (dim := s.dim)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (Opposite.op ⦋s.dim⦌)) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋s.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
              s.simplex) :
          X.S))
      ((fun (s : X.S) ↦
          (mk (dim := s.dim)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋s.dim⦌)) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋s.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋s.dim⦌))
                s.simplex) :
            Y.S))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X Y : SSet
e : X ≅ Y
x : Y.S
⊢ (fun (s : X.S) ↦
        (mk (dim := s.dim)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋s.dim⦌)) :
                (a : (fun (X : Type u) ↦ X) (X _⦋s.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋s.dim⦌))
              s.simplex) :
          Y.S))
      ((fun (s : Y.S) ↦
          (mk (dim := s.dim)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (Opposite.op ⦋s.dim⦌)) :
                  (a : (fun (X : Type u) ↦ X) (Y _⦋s.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
                s.simplex) :
            X.S))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
i j : ℕ
h : i ≤ j
simp :
  ∀ (i_1 : Fin i) (i_2 : (↑(X.nonDegenerate (↑i_1 : ℕ)) : Type u)),
    Subcomplex.ofSimplex (↑i_2 : X _⦋(↑i_1 : ℕ)⦌) ≤
      ⨆ (i : Fin j), ⨆ (x : (↑(X.nonDegenerate (↑i : ℕ)) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋(↑i : ℕ)⦌)
⊢ LE.le.{u} (α := X.Subcomplex)
    ((fun (n : ℕ) ↦
        (⨆ (i : Fin n), ⨆ (x : (↑(X.nonDegenerate (↑i : ℕ)) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋(↑i : ℕ)⦌) :
          X.Subcomplex))
      i)
    ((fun (n : ℕ) ↦
        (⨆ (i : Fin n), ⨆ (x : (↑(X.nonDegenerate (↑i : ℕ)) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋(↑i : ℕ)⦌) :
          X.Subcomplex))
      j)

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : (↑(X.nonDegenerate (↑k : ℕ)) : Type u)
⊢ Subcomplex.ofSimplex (↑x : X _⦋(↑k : ℕ)⦌) ≤ Subcomplex.ofSimplex (↑x : X _⦋(↑k : ℕ)⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : (↑(X.nonDegenerate (↑k : ℕ)) : Type u)
⊢ Subcomplex.ofSimplex (↑x : X _⦋(↑k : ℕ)⦌) ≤
    ⨆ (x : (↑(X.nonDegenerate (↑(⟨(↑k : ℕ), ⋯⟩ : Fin j) : ℕ)) : Type u)),
      Subcomplex.ofSimplex (↑x : X _⦋(↑⟨(↑k : ℕ), ⋯⟩ : ℕ)⦌)

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

Premises used: le_iSup, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : (↑(X.nonDegenerate (↑k : ℕ)) : Type u)
⊢ (↑k : ℕ) < j

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : (↑(X.nonDegenerate (↑k : ℕ)) : Type u)
⊢ Subcomplex.ofSimplex (↑x : X _⦋(↑k : ℕ)⦌) ≤
    ⨆ (i : Fin j), ⨆ (x : (↑(X.nonDegenerate (↑i : ℕ)) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋(↑i : ℕ)⦌)

Tactic:
exact le_trans (by exact le_trans (by rfl) (le_iSup _ x))
      (le_iSup _ ⟨k, by lia⟩)

Premises used: le_iSup, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X : SSet
i : ℕ
x : X _⦋i⦌
n : ℕ
hi : i < n
obtain :
  ∀ (j : ℕ) (f : ⦋i⦌ ⟶ ⦋j⦌),
    Epi f →
      ∀ (y : (↑(X.nonDegenerate j) : Type u)),
        Membership.mem (α := X _⦋i⦌) (γ := Set (X _⦋i⦌))
          (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋i⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋j⦌)) → (fun (X : Type u) ↦ X) (X _⦋i⦌))
              (↑y : X _⦋j⦌) :
            (fun (X : Type u) ↦ X) (X _⦋i⦌))
⊢ Membership.mem (γ := Set (X _⦋i⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋i⦌)) x

Tactic:
obtain ⟨j, f, _, y, rfl⟩ := X.exists_nonDegenerate x

Premises used: SSet.exists_nonDegenerate, rfl
-- 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)
suffices : Subcomplex.ofSimplex (↑y : X _⦋j⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) n
⊢ Membership.mem (α := X _⦋i⦌) (γ := Set (X _⦋i⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋i⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋j⦌)) → (fun (X : Type u) ↦ X) (X _⦋i⦌))
        (↑y : X _⦋j⦌) :
      (fun (X : Type u) ↦ X) (X _⦋i⦌))

Tactic:
suffices Subcomplex.ofSimplex y.1 ≤ X.skeleton n from
    (X.skeleton n).map _ (this _ (Subcomplex.mem_ofSimplex_obj _))
-- 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⦌) ≤ Subcomplex.ofSimplex (↑y : X _⦋j⦌)

Tactic:
rfl
-- 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 : (↑(X.nonDegenerate (↑(⟨j, ⋯⟩ : Fin n) : ℕ)) : Type u)), Subcomplex.ofSimplex (↑x : X _⦋(↑⟨j, ⋯⟩ : ℕ)⦌)

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

Premises used: le_iSup, le_trans