awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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⦌)
⊢ (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

Tactic:
obtain rfl := SimplexCategory.eq_id_of_mono f

Premises used: SimplexCategory.eq_id_of_mono, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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
⊢ y = x

Tactic:
simpa using hf
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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
⊢ y ∈ X.nonDegenerate d

Tactic:
obtain rfl : y = x := by simpa using hf

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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) y hx₁) : X _⦋d⦌) ⋯ <
    mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hy) : X _⦋d⦌) ⋯

Tactic:
obtain rfl : y = x := by simpa using hf

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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⦌) ⋯
⊢ Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) y hx₁) : X _⦋d⦌) ⋯).dim⦌)

Tactic:
obtain rfl : y = x := by simpa using hf

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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⦌)
⊢ (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⦌) ⋯).dim⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, 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) y hx₁) : X _⦋d⦌) ⋯).simplex

Tactic:
obtain rfl : y = x := by simpa using hf

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
d : ℕ
y : X _⦋d⦌
hy 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⦌)
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⦌) ⋯).dim⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, hy⟩ : X _⦋d⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨y, 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) y hx) : X _⦋d⦌) ⋯).simplex
⊢ (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) y hy) : X _⦋d⦌) ⋯).dim

Tactic:
simp at h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x₁ x₂ : X.N
h : x₁ ≤ x₂
h' : x₂ ≤ x₁
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₁⦌) ⋯ ≤ 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₂
⊢ x₁ = x₂

Tactic:
obtain ⟨n₁, ⟨x₁, hx₁⟩, rfl⟩ := x₁.mk_surjective

Premises used: SSet.N.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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₁⦌) ⋯
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₁⦌) ⋯ ≤
        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₂⦌) ⋯
⊢ mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ = x₂

Tactic:
obtain ⟨n₂, ⟨x₂, hx₂⟩, rfl⟩ := x₂.mk_surjective

Premises used: SSet.N.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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₁⦌) ⋯
⊢ n₁ = n₂

Tactic:
le_antisymm (dim_le_of_le h) (dim_le_of_le h')

Premises used: SSet.N.dim_le_of_le, le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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₁⦌) ⋯
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₁⦌) ⋯ ≤
        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₁⦌) ⋯
⊢ 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₂⦌) ⋯

Tactic:
obtain rfl : n₁ = n₂ := le_antisymm (dim_le_of_le h) (dim_le_of_le h')

Premises used: SSet.N.dim_le_of_le, le_antisymm, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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₁⦌) ⋯
⊢ ∃ (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

Tactic:
rw [le_iff_exists_mono] at h

Premises used: SSet.N.le_iff_exists_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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₁⦌) ⋯
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
⊢ 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₁⦌) ⋯

Tactic:
rw [le_iff_exists_mono] at h

Premises used: SSet.N.le_iff_exists_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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₁⦌) ⋯
obtain :
  ∀
    (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₁⦌) ⋯
⊢ 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₁⦌) ⋯

Tactic:
obtain ⟨f, hf, h⟩ := h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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
⊢ Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).dim⦌)

Tactic:
obtain rfl := SimplexCategory.eq_id_of_mono f

Premises used: SimplexCategory.eq_id_of_mono, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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
hf₁ : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).dim⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).dim⦌))) :
        (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

Tactic:
obtain rfl := SimplexCategory.eq_id_of_mono f

Premises used: SimplexCategory.eq_id_of_mono, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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₁⦌) ⋯
hf : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).dim⦌)
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (Quiver.Hom.op
              (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).dim⦌))) :
        (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₁⦌) ⋯

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
a : x ≤ y
a₁ : y ≤ x
⊢ x = y

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
a : x.subcomplex ≤ y.subcomplex
a₁ a₂ : y.subcomplex ≤ y.subcomplex
⊢ x ≤ y

Tactic:
rw [le_iff, h]

Premises used: SSet.N.le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
a : y.subcomplex ≤ x.subcomplex
a₁ a₂ : y.subcomplex ≤ y.subcomplex
⊢ y ≤ x

Tactic:
rw [le_iff, h]

Premises used: SSet.N.le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.N
⊢ x.subcomplex = x.subcomplex

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ x = y

Tactic:
simp [le_antisymm_iff, le_iff, h]

Premises used: le_antisymm_iff, SSet.N.le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
s : X.N
d : ℕ
hd : s.dim = d
subst : Membership.mem (γ := Set (X _⦋(s.cast ⋯).dim⦌)) (X.nonDegenerate (s.cast ⋯).dim) (s.cast ⋯).simplex
⊢ Membership.mem (γ := Set (X _⦋(s.cast hd).dim⦌)) (X.nonDegenerate (s.cast hd).dim) (s.cast hd).simplex

Tactic:
subst hd