awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s.obj i.castSucc = s.obj i.succ
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hi :
      Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
        (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
            (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
        s),
    Membership.mem (γ := Set (ComposableArrows X (n + 1)))
      (Set.range (ι := ComposableArrows X n)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : ComposableArrows X n) → ComposableArrows X (n + 1)))
      s
⊢ Membership.mem (γ := Set (ComposableArrows X (n + 1)))
    (Set.range (ι := ComposableArrows X n)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
        (a : ComposableArrows X n) → ComposableArrows X (n + 1)))
    s

Tactic:
rwa [← mem_range_nerve_σ_iff] at hi

Premises used: PartialOrder.mem_range_nerve_σ_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s.obj i.castSucc = s.obj i.succ
⊢ ∃ (i : Fin (n + 1)),
    Membership.mem (γ := Set (ComposableArrows X (n + 1)))
      (Set.range (ι := ComposableArrows X n)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : ComposableArrows X n) → ComposableArrows X (n + 1)))
      s

Tactic:
exact ⟨i, by rwa [← mem_range_nerve_σ_iff] at hi⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
zero : ∀ (s : nerve X _⦋0⦌), Membership.mem (γ := Set (nerve X _⦋0⦌)) ((nerve X).nonDegenerate 0) s ↔ StrictMono s.obj
succ :
  ∀ (n : ℕ) (s : nerve X _⦋n + 1⦌),
    Membership.mem (γ := Set (nerve X _⦋n + 1⦌)) ((nerve X).nonDegenerate (n + 1)) s ↔ StrictMono s.obj
⊢ Membership.mem (γ := Set (nerve X _⦋n⦌)) ((nerve X).nonDegenerate n) s ↔ StrictMono s.obj

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
s : nerve X _⦋0⦌
⊢ Membership.mem (γ := Set (nerve X _⦋0⦌)) ((nerve X).nonDegenerate 0) s ↔ StrictMono s.obj

Tactic:
simpa using Subsingleton.strictMono _

Premises used: Subsingleton.strictMono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
succ :
  (∃ (i : Fin (n + 1)),
      Membership.mem (γ := Set (nerve X _⦋n + 1⦌))
        (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
            (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
        s) ↔
    ¬∀ (i : Fin (Opposite.unop (Opposite.op ⦋n + 1⦌)).len), s.obj i.castSucc < s.obj i.succ
⊢ Membership.mem (γ := Set (nerve X _⦋n + 1⦌)) ((nerve X).nonDegenerate (n + 1)) s ↔ StrictMono s.obj

Tactic:
rw [← not_iff_not, ← SSet.mem_degenerate_iff_notMem_nonDegenerate,
      Fin.strictMono_iff_lt_succ, SSet.degenerate_eq_iUnion_range_σ, Set.mem_iUnion]

Premises used: not_iff_not, SSet.mem_degenerate_iff_notMem_nonDegenerate, Set.mem_iUnion, Fin.strictMono_iff_lt_succ, SSet.degenerate_eq_iUnion_range_σ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
succ : (∃ (i : Fin (n + 1)), s.obj i.castSucc = s.obj i.succ) ↔ ∃ (x : Fin (n + 1)), ¬s.obj x.castSucc < s.obj x.succ
⊢ (∃ (i : Fin (n + 1)),
      Membership.mem (γ := Set (nerve X _⦋n + 1⦌))
        (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
            (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
        s) ↔
    ¬∀ (i : Fin (Opposite.unop (Opposite.op ⦋n + 1⦌)).len), s.obj i.castSucc < s.obj i.succ

Tactic:
simp only [mem_range_nerve_σ_iff, not_forall]

Premises used: PartialOrder.mem_range_nerve_σ_iff, Classical.not_forall
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
succ : ∀ (a : Fin (n + 1)), s.obj a.castSucc = s.obj a.succ ↔ ¬s.obj a.castSucc < s.obj a.succ
⊢ (∃ (i : Fin (n + 1)), s.obj i.castSucc = s.obj i.succ) ↔ ∃ (x : Fin (n + 1)), ¬s.obj x.castSucc < s.obj x.succ

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s.obj i.castSucc ≤ s.obj i.succ

Tactic:
have := s.monotone i.castSucc_le_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
this : s.obj i.castSucc ≤ s.obj i.succ
⊢ s.obj i.castSucc = s.obj i.succ ↔ ¬s.obj i.castSucc < s.obj i.succ

Tactic:
grind [lt_self_iff_false, LE.le.lt_or_eq]

Premises used: LE.le.lt_or_eq, lt_self_iff_false
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
rw : StrictMono s.obj ↔ Function.Injective s.obj
⊢ Membership.mem (γ := Set (nerve X _⦋n⦌)) ((nerve X).nonDegenerate n) s ↔ Function.Injective s.obj

Tactic:
rw [mem_nerve_nonDegenerate_iff_strictMono]

Premises used: PartialOrder.mem_nerve_nonDegenerate_iff_strictMono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ StrictMono s.obj ↔ Function.Injective s.obj

Tactic:
⟨fun h ↦ h.injective, fun h i j hij ↦ ?_⟩

Premises used: StrictMono.injective, Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
refine :
  ∀ (h : Function.Injective s.obj) (i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) (hij : i < j),
    s.obj i < s.obj j
⊢ StrictMono s.obj ↔ Function.Injective s.obj

Tactic:
refine ⟨fun h ↦ h.injective, fun h i j hij ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
inl : ∀ (h' : s.obj i < s.obj j), s.obj i < s.obj j
inr : ∀ (h' : s.obj i = s.obj j), s.obj i < s.obj j
⊢ s.obj i < s.obj j

Tactic:
obtain h' | h' := (s.monotone hij.le).lt_or_eq

Premises used: LE.le.lt_or_eq, CategoryTheory.Functor.monotone, LT.lt.le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i < s.obj j
⊢ s.obj i < s.obj j

Tactic:
h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i < s.obj j
⊢ s.obj i < s.obj j

Tactic:
exact h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i = s.obj j
⊢ s.obj i < s.obj j

Tactic:
((h h').not_lt hij).elim

Premises used: False.elim, Eq.not_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i = s.obj j
⊢ s.obj i < s.obj j

Tactic:
exact ((h h').not_lt hij).elim

Premises used: False.elim, Eq.not_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
s : X.N
⊢ ∃ (t : X.S) (ht : Membership.mem (γ := Set (X _⦋t.dim⦌)) (X.nonDegenerate t.dim) t.simplex),
    s = { toS := t, nonDegenerate := ht }

Tactic:
⟨s.toS, s.nonDegenerate, rfl⟩

Premises used: SSet.N.toS, Exists.intro, SSet.N.nonDegenerate, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.N
⊢ ∃ (n : ℕ) (y : (↑(X.nonDegenerate n) : Type u)), x = mk (↑y : X _⦋n⦌) ⋯

Tactic:
⟨x.dim, ⟨_, x.nonDegenerate⟩, rfl⟩

Premises used: Subtype.mk, SSet.N.toS, SSet.S.dim, Exists.intro, SSet.N.nonDegenerate, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
motive : X.N → Sort u_1
mk : (n : ℕ) → (x : (↑(X.nonDegenerate n) : Type u)) → motive (N.mk (↑x : X _⦋n⦌) ⋯)
n : ℕ
s : (↑(X.nonDegenerate n) : Type u)
⊢ induction (motive := motive) mk (N.mk (↑s : X _⦋n⦌) ⋯) = mk n s

Tactic:
rfl

Premises used: SSet.N.induction, Set.Mem, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
⊢ x = y ↔ x.toS = y.toS

Tactic:
grind [cases SSet.N]

Premises used: SSet.N
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
⊢ x ≤ y ↔ x.subcomplex ≤ y.subcomplex

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
⊢ x < y ↔ x.subcomplex < y.subcomplex

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
simp :
  (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex) ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
⊢ x ≤ y ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono 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

Tactic:
simp only [le_iff, CategoryTheory.Subfunctor.ofSection_le_iff,
    Subcomplex.mem_ofSimplex_obj_iff]

Premises used: SSet.Subcomplex.mem_ofSimplex_obj_iff, SSet.N.le_iff, CategoryTheory.Subfunctor.ofSection_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
    Mono w →
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex →
        ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
⊢ (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex) →
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
⊢ (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex) ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex

Tactic:
exact ⟨fun ⟨f, hf⟩ ↦ ⟨f, X.mono_of_nonDegenerate ⟨_, x.nonDegenerate⟩ f _ hf, hf⟩, by tauto⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h : x ≤ y
⊢ ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono 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

Tactic:
rw [le_iff_exists_mono] at h

Premises used: SSet.N.le_iff_exists_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h :
  ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono 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
obtain :
  ∀ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (hf : Mono 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 →
      x.dim ≤ y.dim
⊢ x.dim ≤ y.dim

Tactic:
obtain ⟨f, hf, _⟩ := h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf : Mono f
h :
  (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

Tactic:
SimplexCategory.len_le_of_mono f

Premises used: SimplexCategory.len_le_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf : Mono f
h :
  (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

Tactic:
exact SimplexCategory.len_le_of_mono f

Premises used: SimplexCategory.len_le_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h : x < y
inl : ∀ (h' : x.dim < y.dim), x.dim < y.dim
inr : ∀ (h' : x.dim = y.dim), x.dim < y.dim
⊢ x.dim < y.dim

Tactic:
obtain h' | h' := (dim_le_of_le h.le).lt_or_eq

Premises used: SSet.N.dim_le_of_le, LE.le.lt_or_eq, LT.lt.le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h : x < y
h' : x.dim < y.dim
⊢ x.dim < y.dim

Tactic:
h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h : x < y
h' : x.dim < y.dim
⊢ x.dim < y.dim

Tactic:
exact h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.N
h : x < y
h' : x.dim = y.dim
inr :
  ∀ (f : ⦋x.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 _⦋x.dim⦌))
              y.simplex =
            x.simplex),
        x.dim < y.dim
⊢ x.dim < y.dim

Tactic:
obtain ⟨f, _, hf⟩ := le_iff_exists_mono.1 h.le

Premises used: LT.lt.le, SSet.N.le_iff_exists_mono, Iff.mp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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
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⦌) ⋯ < 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⦌),
    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
⊢ x.dim < y.dim

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

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

Tactic:
obtain ⟨d', ⟨y, hy⟩, rfl⟩ := y.mk_surjective

Premises used: SSet.N.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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
⊢ d = d'

Tactic:
h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
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
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⦌) ⋯ <
        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⦌),
    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
⊢ (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

Tactic:
obtain rfl : d = d' := h'

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⦌) ⋯
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
⊢ Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) x hx) : X _⦋d⦌) ⋯).dim⦌)

Tactic:
obtain rfl := SimplexCategory.eq_id_of_mono f

Premises used: SimplexCategory.eq_id_of_mono, rfl