awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
f : j ⟶ ⦋m⦌
i : Fin (j.len + 1)
⊢ Eq (α := Fin (⦋m⦌.len + 1))
    ((Hom.toOrderHom
            ((fun (x : (face S).toSSet.obj (op j)) ↦
                (match (motive := (face S).toSSet.obj (op j) → (j ⟶ ⦋m⦌)) x with
                  | ⟨x, hx⟩ =>
                    Hom.mk
                      {
                        toFun := fun (i : Fin (j.len + 1)) ↦
                          (e.symm : (a : ↥S) → Fin (m + 1))
                            (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S)
                              ((Hom.toOrderHom
                                    (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) :
                                        (a : Δ[n].obj (op j)) → unop (op j) ⟶ ⦋n⦌)
                                      x) :
                                  (a : Fin ((unop (op j)).len + 1)) → Fin (⦋n⦌.len + 1))
                                i)
                              ⋯),
                        monotone' := ⋯ } :
                  j ⟶ ⦋m⦌))
              ((fun (f : j ⟶ ⦋m⦌) ↦
                  (Subtype.mk (p := fun (x : Δ[n].obj (op j)) ↦
                      Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x)
                      (objMk
                        (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                          (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))))
                      ⋯ :
                    { x : Δ[n].obj (op j) // Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x }))
                f)) :
          (a : Fin (j.len + 1)) → Fin (⦋m⦌.len + 1))
        i :
      Fin (⦋m⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (j.len + 1)) → Fin (⦋m⦌.len + 1)) i : Fin (⦋m⦌.len + 1))

Tactic:
apply e.symm_apply_apply

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : ℕ
x_1 : (face S).toSSet _⦋j⦌
x : Δ[n] _⦋j⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x
mk :
  Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
      (objMk
        (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
          (e.toOrderEmbedding.toOrderHom.comp
            {
              toFun := fun (i : Fin (j + 1)) ↦
                (e.symm : (a : ↥S) → Fin (m + 1))
                  (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (j + 1)) → Fin (n + 1)) i) ⋯),
              monotone' := ⋯ : Fin (j + 1) →o Fin (m + 1) })))
      ⋯ =
    Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx
⊢ (fun (f : ⦋j⦌ ⟶ ⦋m⦌) ↦
        (Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
            (objMk
              (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))))
            ⋯ :
          { x : Δ[n] _⦋j⦌ // Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x }))
      ((fun (x : (face S).toSSet _⦋j⦌) ↦
          (match (motive := (face S).toSSet _⦋j⦌ → (⦋j⦌ ⟶ ⦋m⦌)) x with
            | ⟨x, hx⟩ =>
              Hom.mk
                {
                  toFun := fun (i : Fin (⦋j⦌.len + 1)) ↦
                    (e.symm : (a : ↥S) → Fin (m + 1))
                      (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S)
                        ((Hom.toOrderHom
                              (((objEquiv : Δ[n] _⦋j⦌ ≃ (unop (op ⦋j⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋j⦌) → unop (op ⦋j⦌) ⟶ ⦋n⦌)
                                x) :
                            (a : Fin ((unop (op ⦋j⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
                          i)
                        ⋯),
                  monotone' := ⋯ } :
            ⦋j⦌ ⟶ ⦋m⦌))
        (Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x
          hx)) =
    Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : ℕ
x_1 : (face S).toSSet _⦋j⦌
x : Δ[n] _⦋j⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x
mk :
  ∀ (i : Fin (j + 1)),
    Eq (α := Fin (n + 1))
      (((↑(Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
                  (objMk
                    (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                      (e.toOrderEmbedding.toOrderHom.comp
                        {
                          toFun := fun (i : Fin (j + 1)) ↦
                            (e.symm : (a : ↥S) → Fin (m + 1))
                              (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (j + 1)) → Fin (n + 1)) i)
                                ⋯),
                          monotone' := ⋯ : Fin (j + 1) →o Fin (m + 1) })))
                  ⋯) :
              Δ[n] _⦋j⦌) :
            (a : Fin (j + 1)) → Fin (n + 1))
          i :
        Fin (n + 1))
      (((↑(Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x
                  hx) :
              Δ[n] _⦋j⦌) :
            (a : Fin (j + 1)) → Fin (n + 1))
          i :
        Fin (n + 1))
⊢ Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
      (objMk
        (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
          (e.toOrderEmbedding.toOrderHom.comp
            {
              toFun := fun (i : Fin (j + 1)) ↦
                (e.symm : (a : ↥S) → Fin (m + 1))
                  (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (j + 1)) → Fin (n + 1)) i) ⋯),
              monotone' := ⋯ : Fin (j + 1) →o Fin (m + 1) })))
      ⋯ =
    Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx

Tactic:
ext i : 2
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : ℕ
x_1 : (face S).toSSet _⦋j⦌
x : Δ[n] _⦋j⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x
i : Fin (j + 1)
⊢ Eq (α := Fin (n + 1))
    (((↑(Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
                (objMk
                  (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                    (e.toOrderEmbedding.toOrderHom.comp
                      {
                        toFun := fun (i : Fin (j + 1)) ↦
                          (e.symm : (a : ↥S) → Fin (m + 1))
                            (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (j + 1)) → Fin (n + 1)) i)
                              ⋯),
                        monotone' := ⋯ : Fin (j + 1) →o Fin (m + 1) })))
                ⋯) :
            Δ[n] _⦋j⦌) :
          (a : Fin (j + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
    (((↑(Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx) :
            Δ[n] _⦋j⦌) :
          (a : Fin (j + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))

Tactic:
congr_arg Subtype.val
          (e.apply_symm_apply ⟨(objEquiv x).toOrderHom i, _⟩)

Premises used: OrderIso.apply_symm_apply, Subtype.mk, congr_arg, SimplexCategory.Hom.toOrderHom, Subtype.val, DFunLike.coe, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : ℕ
x_1 : (face S).toSSet _⦋j⦌
x : Δ[n] _⦋j⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x
i : Fin (j + 1)
⊢ Eq (α := Fin (n + 1))
    (((↑(Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
                (objMk
                  (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                    (e.toOrderEmbedding.toOrderHom.comp
                      {
                        toFun := fun (i : Fin (j + 1)) ↦
                          (e.symm : (a : ↥S) → Fin (m + 1))
                            (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (j + 1)) → Fin (n + 1)) i)
                              ⋯),
                        monotone' := ⋯ : Fin (j + 1) →o Fin (m + 1) })))
                ⋯) :
            Δ[n] _⦋j⦌) :
          (a : Fin (j + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
    (((↑(Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx) :
            Δ[n] _⦋j⦌) :
          (a : Fin (j + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))

Tactic:
exact congr_arg Subtype.val
          (e.apply_symm_apply ⟨(objEquiv x).toOrderHom i, _⟩)

Premises used: OrderIso.apply_symm_apply, Subtype.mk, congr_arg, SimplexCategory.Hom.toOrderHom, Subtype.val, DFunLike.coe, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
m : ℕ
h : Functor.RepresentableBy X ⦋m⦌
X_1 Y : SimplexCategoryᵒᵖ
x : X_1 ⟶ Y
h₁ :
  ∀ (x_1 : Δ[m].obj X_1),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Δ[m].map x ≫
            Iso.hom
              ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n))
                Y)))
        x_1 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n))
                X_1) ≫
            X.map x))
        x_1
⊢ Δ[m].map x ≫
      Iso.hom
        ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n)) Y) =
    Iso.hom
        ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n)) X_1) ≫
      X.map x

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
m : ℕ
h : Functor.RepresentableBy X ⦋m⦌
X_1 Y : SimplexCategoryᵒᵖ
x : X_1 ⟶ Y
x_1 : Δ[m].obj X_1
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Δ[m].map x ≫
          Iso.hom
            ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n)) Y)))
      x_1 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (n : SimplexCategoryᵒᵖ) ↦ (Equiv.toIso (Equiv.trans objEquiv h.homEquiv) : Δ[m].obj n ≅ X.obj n))
              X_1) ≫
          X.map x))
      x_1

Tactic:
apply h.homEquiv_comp

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Eq.{u + 1} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.δ i))) (face {i}ᶜ)

Tactic:
(face_eq_ofSimplex _ _ (Fin.succAboveOrderIso i)).symm

Premises used: SSet.stdSimplex.face_eq_ofSimplex, OrderHom.comp, SimplexCategory.Hom.comp, Fin.succAboveOrderIso, Eq.symm, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i : Fin (n + 2)
rw :
  Eq.{u + 1} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.δ i))) (face {i}ᶜ)
⊢ Subcomplex.range (stdSimplex.δ i) = face {i}ᶜ

Tactic:
rw [Subcomplex.range_eq_ofSimplex]

Premises used: SSet.Subcomplex.range_eq_ofSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Eq.{u + 1} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.δ i))) (face {i}ᶜ)

Tactic:
ofSimplex_yonedaEquiv_δ i

Premises used: SSet.stdSimplex.ofSimplex_yonedaEquiv_δ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Eq.{u + 1} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.δ i))) (face {i}ᶜ)

Tactic:
exact ofSimplex_yonedaEquiv_δ i

Premises used: SSet.stdSimplex.ofSimplex_yonedaEquiv_δ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
d : SimplexCategoryᵒᵖ
x : unop d ⟶ ⦋n⦌
⊢ (fun (f : (nerve (ULift.{u, 0} (Fin (n + 1)))).obj d) ↦
        (Hom.mk
            (OrderHom.comp (OrderEmbedding.toOrderHom (OrderIso.toOrderEmbedding ULift.orderIso.{u, 0}))
              (Functor.toOrderHom f)) :
          (unop d).Hom ⦋n⦌))
      ((fun (f : unop d ⟶ ⦋n⦌) ↦
          (Monotone.functor (f :=
              Function.comp (β := Fin (⦋n⦌.len + 1))
                (⇑(OrderIso.symm ULift.orderIso.{u, 0}) : (a : Fin (⦋n⦌.len + 1)) → ULift.{u, 0} (Fin (n + 1)))
                (⇑(Hom.toOrderHom f) : (a : Fin ((unop d).len + 1)) → Fin (⦋n⦌.len + 1)))
              ⋯ :
            Fin ((unop d).len + 1) ⥤ ULift.{u, 0} (Fin (n + 1))))
        x) =
    x

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
i : Fin (d + 1)
⊢ Eq.{u + 1} (α := ULift.{u, 0} (Fin (n + 1)))
    (Functor.obj
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve.{u} n).hom.app (op ⦋d⦌)) :
            (a : Δ[n] _⦋d⦌) → ComposableArrows (ULift.{u, 0} (Fin (n + 1))) d)
          s)
        i :
      ULift.{u, 0} (Fin (n + 1)))
    ({ down := (s : (a : Fin (d + 1)) → Fin (n + 1)) i } : ULift.{u, 0} (Fin (n + 1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
F : nerve (ULift.{u, 0} (Fin (n + 1))) _⦋d⦌
i : Fin (d + 1)
⊢ (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((isoNerve.{u} n).inv.app (op ⦋d⦌)) :
              (a : ComposableArrows (ULift.{u, 0} (Fin (n + 1))) d) → Δ[n] _⦋d⦌)
            F :
          Δ[n] _⦋d⦌) :
        (a : Fin (d + 1)) → Fin (n + 1))
      i =
    ULift.down.{u, 0} (F.obj i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
rw :
  StrictMono.{0, u} (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := ULift.{u, 0} (Fin (n + 1)))
      (Functor.obj
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve.{u} n).hom.app (op ⦋d⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋d⦌)) → (fun (X : Type u) ↦ X) (nerve (ULift.{u, 0} (Fin (n + 1))) _⦋d⦌))
          s)) ↔
    StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) s ↔
    StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))

Tactic:
rw [← nonDegenerate_iff_of_mono (isoNerve n).hom,
    PartialOrder.mem_nerve_nonDegenerate_iff_strictMono]

Premises used: SSet.nonDegenerate_iff_of_mono, PartialOrder.mem_nerve_nonDegenerate_iff_strictMono, SSet.stdSimplex.isoNerve, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ StrictMono.{0, u} (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := ULift.{u, 0} (Fin (n + 1)))
      (Functor.obj
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve.{u} n).hom.app (op ⦋d⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋d⦌)) → (fun (X : Type u) ↦ X) (nerve (ULift.{u, 0} (Fin (n + 1))) _⦋d⦌))
          s)) ↔
    StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
rw :
  StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1)) ↔
    Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
      (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
        (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) s ↔
    Mono (C := SimplexCategory) (X := unop (op ⦋d⦌)) (Y := ⦋n⦌)
      (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)

Tactic:
rw [mem_nonDegenerate_iff_strictMono,
    SimplexCategory.mono_iff_injective]

Premises used: SSet.stdSimplex.mem_nonDegenerate_iff_strictMono, SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1)) ↔
    Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
      (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
        (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))

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

Premises used: StrictMono.injective, Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
refine :
  ∀
    (h :
      Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
        (⇑(Hom.toOrderHom
              (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
          (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))),
    StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))
⊢ StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1)) ↔
    Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
      (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
        (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))

Tactic:
refine ⟨fun h ↦ h.injective, fun h ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
h :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
rw :
  ∀ (i : Fin d),
    LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
      ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))
⊢ StrictMono (α := Fin (d + 1)) (β := Fin (n + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))

Tactic:
rw [Fin.strictMono_iff_lt_succ]

Premises used: Fin.strictMono_iff_lt_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
h :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
i : Fin d
inl :
  ∀
    (h' :
      LT.lt (α := Fin (n + 1))
        ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.castSucc)
        ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.succ)),
    LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
      ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))
inr :
  ∀
    (h' :
      Eq (α := Fin (n + 1))
        ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.castSucc)
        ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.succ)),
    LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
      ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))
⊢ LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
    ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))

Tactic:
obtain h' | h' := (stdSimplex.monotone_apply s i.castSucc_le_succ).lt_or_eq

Premises used: Fin.castSucc_le_succ, LE.le.lt_or_eq, SSet.stdSimplex.monotone_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
h :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
i : Fin d
h' :
  LT.lt (α := Fin (n + 1))
    ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.castSucc)
    ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.succ)
⊢ LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
    ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))

Tactic:
h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
h :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
i : Fin d
h' :
  LT.lt (α := Fin (n + 1))
    ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.castSucc)
    ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.succ)
⊢ LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
    ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))

Tactic:
exact h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
h :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) s)) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
i : Fin d
h' :
  Eq (α := Fin (n + 1)) ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.castSucc)
    ((fun (j : Fin (d + 1)) ↦ ((s : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) i.succ)
⊢ LT.lt (α := Fin (n + 1)) ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.castSucc : Fin (n + 1))
    ((s : (a : Fin (d + 1)) → Fin (n + 1)) i.succ : Fin (n + 1))

Tactic:
simpa [Fin.ext_iff] using h h'

Premises used: Fin.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
f : ⦋d⦌ ⟶ ⦋n⦌
⊢ Membership.mem.{u, u} (α := Δ[n] _⦋d⦌) (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d)
      ((Equiv.symm objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋n⦌) → Δ[n] _⦋d⦌) f : Δ[n] _⦋d⦌) ↔
    Mono f

Tactic:
simp [mem_nonDegenerate_iff_mono]

Premises used: SSet.stdSimplex.mem_nonDegenerate_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
s : Fin (d + 1) ↪o Fin (n + 1)
⊢ Membership.mem.{u, u} (α := Δ[n] _⦋d⦌) (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d)
    ((Equiv.symm objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋n⦌) → Δ[n] _⦋d⦌) (Hom.mk s.toOrderHom) : Δ[n] _⦋d⦌)

Tactic:
simpa [mem_nonDegenerate_iff_strictMono] using s.strictMono

Premises used: SSet.stdSimplex.mem_nonDegenerate_iff_strictMono, OrderEmbedding.strictMono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
⊢ (fun (s : Fin (d + 1) ↪o Fin (n + 1)) ↦
        (Subtype.mk (p := fun (x : Δ[n] _⦋d⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) x)
            ((Equiv.symm objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋n⦌) → Δ[n] _⦋d⦌) (Hom.mk s.toOrderHom)) ⋯ :
          { x : Δ[n] _⦋d⦌ // Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) x }))
      ((fun (s : (↑(Δ[n].nonDegenerate d) : Type u)) ↦
          OrderEmbedding.ofStrictMono (⇑(↑s : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) ⋯)
        x) =
    x

Tactic:
aesop