awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
refine_1 :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op ≫ X.map f.op) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₁ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((section_ f).op ≫ f.op)) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₂ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op ≫ X.map ((section_ f).op ≫ f.op)) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₃ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f.op ≫ (section_ f).op ≫ f.op)) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
⊢ Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) : (a : X _⦋n⦌) → X _⦋m⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
          X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
have refine_1₄ : Eq (α := X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f.op ≫ (f ≫ section_ f).op)) : (a : X _⦋m⦌) → X _⦋n⦌)
      (↑y : X _⦋m⦌) :
    X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
refine_1 :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op ≫ X.map f.op) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₁ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((section_ f).op ≫ f.op)) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₂ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op ≫ X.map ((section_ f).op ≫ f.op)) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₃ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f.op ≫ (section_ f).op ≫ f.op)) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₄ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f.op ≫ (f ≫ section_ f).op)) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
⊢ Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) : (a : X _⦋n⦌) → X _⦋m⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
          X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
have refine_1₅ : Eq (α := X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((f ≫ section_ f) ≫ f).op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) :
    X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
⊢ subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑y : X _⦋m⦌))) ≤
    (N.mk (↑y : X _⦋m⦌) ⋯).subcomplex
have refine_2 : Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) ((N.mk (↑y : X _⦋m⦌) sorry).subcomplex.obj (Opposite.op ⦋n⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
Tactic: simp only [Subcomplex.ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x : X.S
y₁ y₂ : X.N
h₁ : y₁.subcomplex = x.subcomplex
h₂ : y₂.subcomplex = x.subcomplex
⊢ y₁.subcomplex = y₂.subcomplex
have rw : x.subcomplex = y₂.subcomplex
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x : X.S
y₁ y₂ : X.N
h₁ : y₁.subcomplex = x.subcomplex
h₂ : y₂.subcomplex = x.subcomplex
rw : x.subcomplex = y₂.subcomplex
⊢ y₁.subcomplex = y₂.subcomplex
have rw₁ : x.subcomplex = x.subcomplex
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x : X.S
y : X.N
hy : x.toN = y
⊢ ∃! f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌,
    Epi f ∧
      (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
have obtain : ∀ (n : ℕ) (x : X _⦋n⦌) (hy : { dim := n, simplex := x : X.S }.toN = y),
  ∃! f : ⦋{ dim := n, simplex := x : X.S }.dim⦌ ⟶ ⦋y.dim⦌,
    Epi f ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋{ dim := n, simplex := x }.dim⦌))
          y.simplex =
        { dim := n, simplex := x : X.S }.simplex
Tactic: obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective
Cleared hypotheses: x, hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
y : X.N
n : ℕ
x : X _⦋n⦌
hy : { dim := n, simplex := x : X.S }.toN = y
⊢ ∃! f : ⦋{ dim := n, simplex := x : X.S }.dim⦌ ⟶ ⦋y.dim⦌,
    Epi f ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋{ dim := n, simplex := x }.dim⦌))
          y.simplex =
        { dim := n, simplex := x : X.S }.simplex
have obtain : ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌),
  Epi f →
    ∀ (z : (↑(X.nonDegenerate m) : Type u))
      (hy :
        toN
            (mk (dim := n)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                (↑z : X _⦋m⦌))) =
          y),
      ∃! f_1 :
        ⦋dim.{u} (X := X)
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  (↑z : X _⦋m⦌)))⦌ ⟶
          ⦋y.dim⦌,
        Epi f_1 ∧
          Eq (α :=
            (fun (X : Type u) ↦ X)
              (X _⦋dim.{u} (X := X)
                  (mk (dim := n)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                      (↑z : X _⦋m⦌)))⦌))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) →
                    (fun (X : Type u) ↦ X)
                      (X _⦋{ dim := n,
                            simplex :=
                              (ConcreteCategory.hom (X.map f.op) :
                                  (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                                (↑z : X _⦋m⦌) }.dim⦌))
                y.simplex :
              (fun (X : Type u) ↦ X)
                (X _⦋dim.{u} (X := X)
                    (mk (dim := n)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                        (↑z : X _⦋m⦌)))⦌))
            (simplex
                (mk (dim := n)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                    (↑z : X _⦋m⦌))) :
              X _⦋dim.{u} (X := X)
                  (mk (dim := n)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                      (↑z : X _⦋m⦌)))⦌)
Tactic: obtain ⟨m, f, _, z, rfl⟩ := X.exists_nonDegenerate x
Cleared hypotheses: x, hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
z : (↑(X.nonDegenerate m) : Type u)
hy :
  toN
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌))) =
    y
⊢ y = N.mk (↑z : X _⦋m⦌) ⋯
have hy₁ : y.subcomplex =
  subcomplex
    (mk (dim := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (↑z : X _⦋m⦌)))
Tactic: rw [toN_eq_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
z : (↑(X.nonDegenerate m) : Type u)
hy :
  y.subcomplex =
    subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌)))
⊢ y = N.mk (↑z : X _⦋m⦌) ⋯
have rw : subcomplex
    (mk (dim := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (↑z : X _⦋m⦌))) =
  (N.mk (↑z : X _⦋m⦌) sorry).subcomplex
Tactic: rw [← N.subcomplex_injective_iff, hy]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex (goal)
Goal:
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
⊢ motive s
have pos : ∀ (hs : s.subcomplex ≤ A), motive s
Tactic: by_cases hs : s.subcomplex ≤ A
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex (goal)
Goal:
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
pos : ∀ (hs : s.subcomplex ≤ A), motive s
⊢ motive s
have neg : ∀ (hs : ¬s.subcomplex ≤ A), motive s
Tactic: by_cases hs : s.subcomplex ≤ A
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex (goal)
Goal:
X : SSet
A : X.Subcomplex
x y : A.N
⊢ x = y ↔ { dim := x.dim, simplex := x.simplex : X.S } = { dim := y.dim, simplex := y.simplex }
have rw : x.toN = y.toN ↔ { dim := x.dim, simplex := x.simplex : X.S } = { dim := y.dim, simplex := y.simplex }
Tactic: rw [N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex (goal)
Goal:
X : SSet
A : X.Subcomplex
x y : A.N
rw : x.toN = y.toN ↔ { dim := x.dim, simplex := x.simplex : X.S } = { dim := y.dim, simplex := y.simplex }
⊢ x = y ↔ { dim := x.dim, simplex := x.simplex : X.S } = { dim := y.dim, simplex := y.simplex }
have rw₁ : x.toS = y.toS ↔ { dim := x.dim, simplex := x.simplex : X.S } = { dim := y.dim, simplex := y.simplex }
Tactic: rw [N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex (goal)
Goal:
X : SSet
A : X.Subcomplex
s : A.N
d : ℕ
hd : s.dim = d
⊢ s.cast hd = s
have subst : s.cast sorry = s
Tactic: subst hd
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex (goal)
Goal:
X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
x : A.N
⊢ S.simplex (N.toS ((SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN)) ∉
    B.obj (Opposite.op ⦋S.dim.{u} (X := Y) (N.toS ((SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN))⦌)
have subst : ∀ (x : (B.preimage e.hom).N),
  S.simplex (N.toS ((SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN)) ∉
    B.obj (Opposite.op ⦋S.dim.{u} (X := Y) (N.toS ((SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN))⦌)
Tactic: subst hA
Cleared hypotheses: A, hA, x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex (goal)
Goal:
X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
y : B.N
⊢ S.simplex (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN)) ∉
    A.obj (Opposite.op ⦋S.dim.{u} (X := X) (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN))⦌)
have obtain : ∀ (hA : (A.preimage e.inv).preimage e.hom = A) (y : (A.preimage e.inv).N),
  S.simplex (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN)) ∉
    A.obj (Opposite.op ⦋S.dim.{u} (X := X) (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN))⦌)
Tactic: obtain rfl : A.preimage e.inv = B := by aesop
Cleared hypotheses: B, hA, y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex (goal)
Goal:
X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
⊢ ∃ (x : A.N) (f : ⦋n⦌ ⟶ ⦋x.dim⦌),
    Epi f ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          x.simplex =
        s
have refine : ∀
  (h :
    Membership.mem (γ := Set (X _⦋{ dim := n, simplex := s : X.S }.toN.dim⦌))
      (A.obj (Opposite.op ⦋{ dim := n, simplex := s : X.S }.toN.dim⦌)) { dim := n, simplex := s : X.S }.toN.simplex),
  Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) s
Tactic: refine ⟨⟨(S.mk s).toN, fun h ↦ hs ?_⟩, ⟨(S.mk s).toNπ, inferInstance, S.map_toNπ_op_apply _⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex (goal)
Goal:
X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
h :
  Membership.mem (γ := Set (X _⦋{ dim := n, simplex := s : X.S }.toN.dim⦌))
    (A.obj (Opposite.op ⦋{ dim := n, simplex := s : X.S }.toN.dim⦌)) { dim := n, simplex := s : X.S }.toN.simplex
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) s
have simp : ∀ (h : ofSimplex { dim := n, simplex := s : X.S }.toN.simplex ≤ A), ofSimplex s ≤ A
Tactic: simp only [← ofSimplex_le_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonempty (goal)
Goal:
X : SSet
⊢ ¬X.Nonempty ↔ X.HasDimensionLT 0
have simp : IsEmpty.{u + 1} (X _⦋0⦌) ↔ X.HasDimensionLT 0
Tactic: simp only [not_nonempty_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonempty (goal)
Goal:
X : SSet
⊢ IsEmpty.{u + 1} (X _⦋0⦌) ↔ X.HasDimensionLT 0
have refine_1 : IsEmpty.{u + 1} (X _⦋0⦌) → ∀ (n : ℕ) (hn : 0 ≤ n), X.degenerate n = ⊤
Tactic: refine ⟨fun _ ↦ ⟨fun n hn ↦ ?_⟩, fun _ ↦ ⟨fun x ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonempty (goal)
Goal:
X : SSet
refine_1 : IsEmpty.{u + 1} (X _⦋0⦌) → ∀ (n : ℕ) (hn : 0 ≤ n), X.degenerate n = ⊤
⊢ IsEmpty.{u + 1} (X _⦋0⦌) ↔ X.HasDimensionLT 0
have refine_2 : X.HasDimensionLT 0 → ∀ (x : X _⦋0⦌), False
Tactic: refine ⟨fun _ ↦ ⟨fun n hn ↦ ?_⟩, fun _ ↦ ⟨fun x ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonempty (hypothesis)
Goal:
X : SSet
h : IsEmpty.{u + 1} (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
⊢ X.degenerate n = ⊤
have this : IsEmpty.{u + 1} ((fun (X : Type u) ↦ X) (X _⦋n⦌))
Tactic: have := Function.isEmpty (X.map (⦋0⦌.const ⦋n⦌ 0).op)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonempty (hypothesis)
Goal:
X : SSet
hX : ¬X.Nonempty
⊢ IsInitial X
have hX₁ : IsEmpty.{u + 1} (X _⦋0⦌)
Tactic: simp only [not_nonempty_iff] at hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonempty (hypothesis)
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
⊢ IsInitial X
have this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
Tactic: have (n : SimplexCategoryᵒᵖ) : IsEmpty (X.obj n) :=
    Function.isEmpty (X.map (⦋0⦌.const n.unop 0).op)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonempty (goal)
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
x : SSet
x_1 x_2 : SimplexCategoryᵒᵖ
x_3 : x_1 ⟶ x_2
⊢ (X.map x_3 ≫ ↾fun (x_4 : X.obj x_2) ↦ isEmptyElim (p := fun (x_5 : X.obj x_2) ↦ x.obj x_2) x_4) =
    (↾fun (x_4 : X.obj x_1) ↦ isEmptyElim (p := fun (x_5 : X.obj x_1) ↦ x.obj x_1) x_4) ≫ x.map x_3
have h : ∀ (x_4 : X.obj x_1),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map x_3 ≫ ↾fun (x_5 : X.obj x_2) ↦ isEmptyElim (p := fun (x_6 : X.obj x_2) ↦ x.obj x_2) x_5))
      x_4 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_5 : X.obj x_1) ↦ isEmptyElim (p := fun (x_6 : X.obj x_1) ↦ x.obj x_1) x_5) ≫ x.map x_3))
      x_4
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonempty (goal)
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
x : SSet
x_1 : X ⟶ x
⊢ x_1 =
    (fun (x : SSet.{u}) ↦
        ({
            app := fun (x_2 : SimplexCategoryᵒᵖ) ↦
              ↾fun (x_3 : X.obj x_2) ↦ isEmptyElim (p := fun (x_4 : X.obj x_2) ↦ x.obj x_2) x_3,
            naturality := ⋯ } :
          NatTrans X x))
      x
have w : ∀ (n : SimplexCategoryᵒᵖ) (x_2 : X.obj n),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app n)).toFun x_2 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : SSet.{u}) ↦
              ({
                  app := fun (x_3 : SimplexCategoryᵒᵖ) ↦
                    ↾fun (x_4 : X.obj x_3) ↦ isEmptyElim (p := fun (x_5 : X.obj x_3) ↦ x.obj x_3) x_4,
                  naturality := sorry } :
                NatTrans X x))
            x)
          n))
      x_2
Tactic: ext _ x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (goal)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
inst_1 : Y.Nonsingular
n : ℕ
⊢ ∀ (x : (↑(X.nonDegenerate n) : Type u)),
    Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) (↑x : X _⦋n⦌))
have this : ∀ (x : X _⦋n⦌) (hx : x ∈ X.nonDegenerate n),
  Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X)
    ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
      (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌))
Tactic: ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (hypothesis)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
inst_1 : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X)
    ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
      (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌))
have hx₁ : Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.nonDegenerate n)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      x :
    (fun (X : Type u) ↦ X) (Y _⦋n⦌))
Tactic: rw [← nonDegenerate_iff_of_mono f] at hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (hypothesis)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
inst_1 : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.nonDegenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
⊢ Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X)
    ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
      (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌))
have this : Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := Y)
  ((Equiv.symm yonedaEquiv : (a : Y _⦋n⦌) → Δ[n] ⟶ Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌)))
Tactic: have := mono' _ hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (hypothesis)
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
inst_1 : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.nonDegenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
this :
  Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := Y)
    ((Equiv.symm yonedaEquiv : (a : Y _⦋n⦌) → Δ[n] ⟶ Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)))
⊢ Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X)
    ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
      (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌))
have this₁ : Mono (X := Δ[n]) ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ≫ f)
Tactic: rw [← SSet.yonedaEquiv_symm_comp] at this
Cleared hypotheses: this