awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
s t : X.S
⊢ 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
have 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
Tactic: rw [le_def, Subcomplex.ofSimplex_le_iff, Subfunctor.ofSection_obj, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
s t : X.S
⊢ (∃ (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
have mp : (∃ (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
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
s t : X.S
mp :
  (∃ (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
⊢ (∃ (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
have mpr : (∃ (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) →
  ∃ (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
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
s t : X.S
mp :
  (∃ (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
mpr :
  (∃ (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) →
    ∃ (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 : 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
have mp₁ : ∀ (w : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w) :
          (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
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
s t : X.S
mp :
  (∃ (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
mpr :
  (∃ (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) →
    ∃ (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
mp₁ mp₂ mp₃ :
  ∀ (w : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w) :
            (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
⊢ (∃ (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
have mpr₁ : ∀ (w : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
        t.simplex =
      s.simplex →
    ∃ (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
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
⊢ 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 }
have 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))⦌)
Tactic: rw [le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst : Mono 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 } ↔
    IsIso f
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
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
⊢ 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
have 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 }
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
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 }
⊢ IsIso f
have 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
Tactic: obtain rfl := S.dim_eq_of_mk_eq h
Cleared hypotheses: n, x, f, inst, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
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 }
⊢ IsIso f
have 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⦌)
Tactic: obtain rfl := SimplexCategory.eq_id_of_mono f
Cleared hypotheses: f, inst, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst : Mono f
hf : 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 }
have 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 }
Tactic: obtain rfl := SimplexCategory.eq_of_isIso f
Cleared hypotheses: n, x, f, inst, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
m : ℕ
x : X _⦋m⦌
f : ⦋m⦌ ⟶ ⦋m⦌
inst : 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 }
have 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 }
Tactic: obtain rfl := SimplexCategory.eq_id_of_isIso f
Cleared hypotheses: f, inst, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
x y : X.S
⊢ 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))
have 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))
Tactic: rw [le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
Goal:
X : SSet
x y : X.S
⊢ (∃ (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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
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))
⊢ (∃ (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))
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
i j : ℕ
h : i ≤ j
⊢ 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)
have 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 : ℕ)⦌)
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
i : ℕ
x : X _⦋i⦌
n : ℕ
hi : i < n
⊢ Membership.mem (γ := Set (X _⦋i⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋i⦌)) x
have 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⦌))
Tactic: obtain ⟨j, f, _, y, rfl⟩ := X.exists_nonDegenerate x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w : 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⦌))
have suffices : Subcomplex.ofSimplex (↑y : X _⦋j⦌) ≤ (X.skeleton : (a : ℕ) → X.Subcomplex) n
Tactic: suffices Subcomplex.ofSimplex y.1 ≤ X.skeleton n from
    (X.skeleton n).map _ (this _ (Subcomplex.mem_ofSimplex_obj _))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X : SSet
d n : ℕ
h : d < n
⊢ Eq.{u + 1} (α := Set (X _⦋d⦌)) (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌)) ⊤
have rw : LE.le.{u} (α := Set (X _⦋d⦌)) ⊤ (Subfunctor.obj ((X.skeleton : (a : ℕ) → X.Subcomplex) n) (op ⦋d⦌))
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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
have refine : ∀
  (h :
    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 _⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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⦌)
⊢ d < n
have 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
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (hypothesis)
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⦌)
⊢ d < n
have 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
Tactic: simp only [skeleton, OrderHom.coe_mk, Subfunctor.iSup_obj,
    Set.iUnion_coe_set, Set.mem_iUnion, exists_prop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
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
⊢ d < n
have 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
Tactic: obtain ⟨⟨i, hi⟩, y, hy, ⟨f⟩, rfl⟩ := h
Cleared hypotheses: x, hx, h
-- 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⦌))
⊢ d < n
have this : Mono f
Tactic: have := X.mono_of_nonDegenerate ⟨_, hx⟩ f y rfl