awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x < y
h' : x.dim = y.dim
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
w : Mono f
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
⊢ x.dim < y.dim
have inr : ∀ (d : ℕ) (x : X _⦋d⦌) (hx : x ∈ X.nonDegenerate d)
  (h : mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry < y)
  (h' : (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim = y.dim)
  (f : ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim⦌ ⟶ ⦋y.dim⦌),
  Mono f →
    ∀
      (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 _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) sorry).dim⦌))
            y.simplex =
          (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).simplex),
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim < y.dim
Tactic: obtain ⟨d, ⟨x, hx⟩, rfl⟩ := x.mk_surjective
Cleared hypotheses: x, h, h', f, w, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
y : X.N
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
h : mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯ < y
h' : (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim = y.dim
f : ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌ ⟶ ⦋y.dim⦌
w : Mono f
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 _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) ⋯).dim⦌))
      y.simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).simplex
⊢ (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim < y.dim
have inr : ∀ (d' : ℕ) (y : X _⦋d'⦌) (hy : y ∈ X.nonDegenerate d')
  (h :
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry <
      mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) sorry)
  (h' :
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim =
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) sorry).dim)
  (f :
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim⦌ ⟶
      ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) sorry).dim⦌),
  Mono f →
    ∀
      (hf :
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d'⦌) sorry).dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) sorry).dim⦌))
            (mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) sorry).simplex =
          (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).simplex),
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim <
        (mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) sorry).dim
Tactic: obtain ⟨d', ⟨y, hy⟩, rfl⟩ := y.mk_surjective
Cleared hypotheses: y, h, h', f, w, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
d' : ℕ
y : X _⦋d'⦌
hy : y ∈ X.nonDegenerate d'
h :
  mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯ <
    mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) ⋯
h' :
  (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) ⋯).dim
f :
  ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌ ⟶
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) ⋯).dim⦌
w : Mono f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d'⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) ⋯).dim⦌))
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) ⋯).simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).simplex
⊢ (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim <
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d'⦌) ↦ x ∈ X.nonDegenerate d') y hy) : X _⦋d'⦌) ⋯).dim
have inr : ∀ (y : X _⦋d⦌) (hy : y ∈ X.nonDegenerate d)
  (h :
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry <
      mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) sorry)
  (f :
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim⦌ ⟶
      ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) sorry).dim⦌),
  Mono f →
    ∀
      (hf :
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) sorry).dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) sorry).dim⦌))
            (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) sorry).simplex =
          (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).simplex),
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim <
        (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) sorry).dim
Tactic: obtain rfl : d = d' := h'
Cleared hypotheses: d', y, hy, h, h', f, w, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
y : X _⦋d⦌
hy : y ∈ X.nonDegenerate d
h :
  mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯ <
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯
f :
  ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌ ⟶
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).dim⦌
w : Mono f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) ⋯).dim⦌))
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).simplex
⊢ (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim <
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).dim
have w : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim⦌)
Tactic: obtain rfl := SimplexCategory.eq_id_of_mono f
Cleared hypotheses: f, w, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
y : X _⦋d⦌
hy : y ∈ X.nonDegenerate d
h :
  mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯ <
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯
f :
  ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌ ⟶
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).dim⦌
w_1 : Mono f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) ⋯).dim⦌))
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).simplex
w : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌)
⊢ (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim <
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).dim
have hf₁ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map
          (Quiver.Hom.op
            (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).dim⦌))) :
      (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) sorry).dim⦌)) →
        (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) sorry).dim⦌))
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) sorry).simplex =
  (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) sorry).simplex
Tactic: obtain rfl := SimplexCategory.eq_id_of_mono f
Cleared hypotheses: f, w_1, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
y : X _⦋d⦌
hy : y ∈ X.nonDegenerate d
h :
  mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯ <
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯
w : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌)
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) ⋯).dim⦌))
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).simplex
hx₁ : y ∈ X.nonDegenerate d
⊢ (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim <
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).dim
have h₁ : mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hx₁) : X _⦋d⦌) sorry <
  mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) sorry
Tactic: obtain rfl : y = x := by simpa using hf
Cleared hypotheses: x, hx, h, w, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
y : X _⦋d⦌
hy : y ∈ X.nonDegenerate d
h :
  mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯ <
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯
w : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌)
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) ⋯).dim⦌))
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).simplex
hx₁ : y ∈ X.nonDegenerate d
h₁ :
  mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hx₁) : X _⦋d⦌) ⋯ <
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯
⊢ (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim <
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).dim
have w : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hx₁) : X _⦋d⦌) sorry).dim⦌)
Tactic: obtain rfl : y = x := by simpa using hf
Cleared hypotheses: x, hx, h, w, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
y : X _⦋d⦌
hy : y ∈ X.nonDegenerate d
h :
  mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯ <
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯
w_1 : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌)
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x, hx⟩ : X _⦋d⦌) ⋯).dim⦌))
      (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).simplex
hx₁ : y ∈ X.nonDegenerate d
h₁ :
  mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hx₁) : X _⦋d⦌) ⋯ <
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯
w : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hx₁) : X _⦋d⦌) ⋯).dim⦌)
⊢ (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim <
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯).dim
have hf₁ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map
          (Quiver.Hom.op
            (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hx₁) : X _⦋d⦌) sorry).dim⦌))) :
      (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) sorry).dim⦌)) →
        (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hx₁⟩ : X _⦋d⦌) sorry).dim⦌))
    (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) sorry).simplex =
  (mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hx₁) : X _⦋d⦌) sorry).simplex
Tactic: obtain rfl : y = x := by simpa using hf
Cleared hypotheses: x, hx, h, w_1, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x₁ x₂ : X.N
h : x₁ ≤ x₂
h' : x₂ ≤ x₁
⊢ x₁ = x₂
have obtain : ∀ (n₁ : ℕ) (x₁ : X _⦋n₁⦌) (hx₁ : x₁ ∈ X.nonDegenerate n₁)
  (h : mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry ≤ x₂)
  (h' : x₂ ≤ mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry),
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry = x₂
Tactic: obtain ⟨n₁, ⟨x₁, hx₁⟩, rfl⟩ := x₁.mk_surjective
Cleared hypotheses: x₁, h, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x₂ : X.N
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
h : mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ ≤ x₂
h' : x₂ ≤ mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯
⊢ mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ = x₂
have obtain : ∀ (n₂ : ℕ) (x₂ : X _⦋n₂⦌) (hx₂ : x₂ ∈ X.nonDegenerate n₂)
  (h :
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry ≤
      mk (↑(Subtype.mk (p := fun (x : X _⦋n₂⦌) ↦ x ∈ X.nonDegenerate n₂) x₂ hx₂) : X _⦋n₂⦌) sorry)
  (h' :
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₂⦌) ↦ x ∈ X.nonDegenerate n₂) x₂ hx₂) : X _⦋n₂⦌) sorry ≤
      mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry),
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry =
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₂⦌) ↦ x ∈ X.nonDegenerate n₂) x₂ hx₂) : X _⦋n₂⦌) sorry
Tactic: obtain ⟨n₂, ⟨x₂, hx₂⟩, rfl⟩ := x₂.mk_surjective
Cleared hypotheses: x₂, h, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
n₂ : ℕ
x₂ : X _⦋n₂⦌
hx₂ : x₂ ∈ X.nonDegenerate n₂
h :
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ ≤
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₂⦌) ↦ x ∈ X.nonDegenerate n₂) x₂ hx₂) : X _⦋n₂⦌) ⋯
h' :
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₂⦌) ↦ x ∈ X.nonDegenerate n₂) x₂ hx₂) : X _⦋n₂⦌) ⋯ ≤
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯
⊢ mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ =
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₂⦌) ↦ x ∈ X.nonDegenerate n₂) x₂ hx₂) : X _⦋n₂⦌) ⋯
have obtain : ∀ (x₂ : X _⦋n₁⦌) (hx₂ : x₂ ∈ X.nonDegenerate n₁)
  (h :
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry ≤
      mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) sorry)
  (h' :
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) sorry ≤
      mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry),
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry =
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) sorry
Tactic: obtain rfl : n₁ = n₂ := le_antisymm (dim_le_of_le h) (dim_le_of_le h')
Cleared hypotheses: n₂, x₂, hx₂, h, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h :
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ ≤
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯
h' :
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯ ≤
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯
⊢ mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ =
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯
have h₁ : ∃ (f :
  ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry).dim⦌ ⟶
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) sorry).dim⦌)
  (_ : Mono f),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₂, hx₂⟩ : X _⦋n₁⦌) sorry).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₁, hx₁⟩ : X _⦋n₁⦌) sorry).dim⦌))
      (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) sorry).simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry).simplex
Tactic: rw [le_iff_exists_mono] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h :
  ∃ (f :
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).dim⦌ ⟶
      ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯).dim⦌)
    (_ : Mono f),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₂, hx₂⟩ : X _⦋n₁⦌) ⋯).dim⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₁, hx₁⟩ : X _⦋n₁⦌) ⋯).dim⦌))
        (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯).simplex =
      (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).simplex
h' :
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯ ≤
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯
⊢ mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ =
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯
have obtain : ∀
  (f :
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry).dim⦌ ⟶
      ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) sorry).dim⦌)
  (hf : Mono f)
  (h :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₂, hx₂⟩ : X _⦋n₁⦌) sorry).dim⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₁, hx₁⟩ : X _⦋n₁⦌) sorry).dim⦌))
        (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) sorry).simplex =
      (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry).simplex),
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry =
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) sorry
Tactic: obtain ⟨f, hf, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h' :
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯ ≤
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯
f :
  ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).dim⦌ ⟶
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯).dim⦌
hf : Mono f
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₂, hx₂⟩ : X _⦋n₁⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₁, hx₁⟩ : X _⦋n₁⦌) ⋯).dim⦌))
      (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯).simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).simplex
⊢ mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ =
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯
have hf₁ : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry).dim⦌)
Tactic: obtain rfl := SimplexCategory.eq_id_of_mono f
Cleared hypotheses: f, hf, h