awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
left :
  Function.Injective (β :=
    { x : Finset (Fin (n + 1)) //
      Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
    fun (x : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }) ↦
    match (motive :=
      { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x } →
        { x : Finset (Fin (n + 1)) //
          Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
      x with
    | ⟨x, hx⟩ =>
      Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
        Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x)
        (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(Hom.toOrderHom
                (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
            (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
          univ)
        ⋯
right :
  Function.Surjective (β :=
    { x : Finset (Fin (n + 1)) //
      Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
    fun (x : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }) ↦
    match (motive :=
      { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x } →
        { x : Finset (Fin (n + 1)) //
          Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
      x with
    | ⟨x, hx⟩ =>
      Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
        Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x)
        (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(Hom.toOrderHom
                (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
            (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
          univ)
        ⋯
⊢ Function.Bijective (β :=
    { x : Finset (Fin (n + 1)) //
      Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
    fun (x : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }) ↦
    match (motive :=
      { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x } →
        { x : Finset (Fin (n + 1)) //
          Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
      x with
    | ⟨x, hx⟩ =>
      Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
        Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x)
        (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
          (⇑(Hom.toOrderHom
                (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
            (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
          univ)
        ⋯

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁_1 :
  Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₁ : Δ[n] _⦋m⦌)
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂_1 :
  Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₂ : Δ[n] _⦋m⦌)
h₁ : Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1))
h₂ : Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1))
h₃ :
  Eq (α := Finset (Fin (n + 1)))
    (Finset.image (α := Fin (m + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1)) univ)
    (Finset.image (α := Fin (m + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1)) univ)
left : Hom.toOrderHom f₁ = Hom.toOrderHom f₂
⊢ f₁ = f₂

Tactic:
apply SimplexCategory.Hom.ext

Premises used: SimplexCategory.Hom.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁_1 :
  Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₁ : Δ[n] _⦋m⦌)
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂_1 :
  Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₂ : Δ[n] _⦋m⦌)
h₁ : Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1))
h₂ : Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1))
h₃ :
  Eq (α := Finset (Fin (n + 1)))
    (Finset.image (α := Fin (m + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1)) univ)
    (Finset.image (α := Fin (m + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1)) univ)
left :
  Eq (α := Set (Fin (n + 1))) (Set.range (ι := Fin (m + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1)))
    (Set.range (ι := Fin (m + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1)))
⊢ Hom.toOrderHom f₁ = Hom.toOrderHom f₂

Tactic:
rw [← OrderHom.range_eq_iff h₁ h₂]

Premises used: OrderHom.range_eq_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁_1 :
  Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₁ : Δ[n] _⦋m⦌)
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂_1 :
  Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₂ : Δ[n] _⦋m⦌)
h₁ : Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1))
h₂ : Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1))
h₃ :
  Eq (α := Finset (Fin (n + 1)))
    (Finset.image (α := Fin (m + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1)) univ)
    (Finset.image (α := Fin (m + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1)) univ)
left :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Set (Fin (n + 1)))
        (Set.range (ι := Fin (m + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1))) x ↔
      Membership.mem (γ := Set (Fin (n + 1)))
        (Set.range (ι := Fin (m + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1))) x
⊢ Eq (α := Set (Fin (n + 1))) (Set.range (ι := Fin (m + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1)))
    (Set.range (ι := Fin (m + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1)))

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁_1 :
  Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₁ : Δ[n] _⦋m⦌)
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂_1 :
  Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    ((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f₂ : Δ[n] _⦋m⦌)
h₁ : Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1))
h₂ : Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1))
h₃ :
  Eq (α := Finset (Fin (n + 1)))
    (Finset.image (α := Fin (m + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1)) univ)
    (Finset.image (α := Fin (m + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1)) univ)
x : Fin (n + 1)
⊢ Membership.mem (γ := Set (Fin (n + 1)))
      (Set.range (ι := Fin (m + 1)) (⇑(Hom.toOrderHom f₁) : (a : Fin (m + 1)) → Fin (n + 1))) x ↔
    Membership.mem (γ := Set (Fin (n + 1)))
      (Set.range (ι := Fin (m + 1)) (⇑(Hom.toOrderHom f₂) : (a : Fin (m + 1)) → Fin (n + 1))) x

Tactic:
simpa using congr_fun (congrArg Membership.mem h₃) x

Premises used: congrArg, Membership.mem, congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
⊢ Fintype.card ↥S = m + 1

Tactic:
simpa using hS
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ ∃ (a : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }),
    Eq (α :=
      { x : Finset (Fin (n + 1)) //
        Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
      ((fun (x : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }) ↦
          (match (motive :=
              { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x } →
                { x : Finset (Fin (n + 1)) //
                  Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
              x with
            | ⟨x, hx⟩ =>
              Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
                Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x)
                (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
                  (⇑(Hom.toOrderHom
                        (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
                    (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
                  univ)
                ⋯ :
            { x : Finset (Fin (n + 1)) //
              Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x }))
        a)
      (Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
        Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x) S hS)

Tactic:
⟨⟨objMk ((OrderHom.Subtype.val _).comp e.toOrderEmbedding.toOrderHom), ?_⟩, ?_⟩

Premises used: SSet.stdSimplex.objMk, OrderIso.toOrderEmbedding, OrderHom.comp, Subtype.mk, Exists.intro, OrderHom.Subtype.val, OrderEmbedding.toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
right :
  Function.Injective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom
          (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌)
            (objMk
              (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)))) :
      (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m)
    (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))

Tactic:
rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective]

Premises used: SimplexCategory.mono_iff_injective, SSet.stdSimplex.mem_nonDegenerate_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
a b : Fin ((unop (op ⦋m⦌)).len + 1)
h :
  Eq (α := Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom
            (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌)
              (objMk
                (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))) :
          (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
        a :
      Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom
            (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌)
              (objMk
                (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))) :
          (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
        b :
      Fin (⦋n⦌.len + 1))
⊢ a = b

Tactic:
grind [e.injective, dsimp% h]

Premises used: OrderIso.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ Eq (α :=
    { x : Finset (Fin (n + 1)) //
      Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
    ((fun (x : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }) ↦
        (match (motive :=
            { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x } →
              { x : Finset (Fin (n + 1)) //
                Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x })
            x with
          | ⟨x, hx⟩ =>
            Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
              Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x)
              (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
                (⇑(Hom.toOrderHom
                      (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
                  (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
                univ)
              ⋯ :
          { x : Finset (Fin (n + 1)) //
            Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x }))
      (Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x)
        (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) ⋯))
    (Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦
      Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1} x) S hS)

Tactic:
simp [e, ← Finset.image_image, Finset.image_univ_of_surjective e.surjective]

Premises used: Finset.image_univ_of_surjective, OrderIso.surjective, Finset.image_image
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
j : Fin (n + 1)
simp :
  Membership.mem (γ := Finset (Fin (n + 1)))
      (↑(((nonDegenerateEquiv' :
                (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
              (a : (↑(Δ[n].nonDegenerate d) : Type u)) → { x : Finset (Fin (n + 1)) // #x = d + 1 })
            x) :
        Finset (Fin (n + 1)))
      j ↔
    ∃ (i : Fin (d + 1)), ((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i = j
⊢ Membership.mem (γ := Finset (Fin (n + 1)))
      (↑(((nonDegenerateEquiv' :
                (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
              (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
            x) :
        Finset (Fin (n + 1)))
      j ↔
    ∃ (i : Fin (d + 1)), ((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i = j

Tactic:
simp only [Set.mem_setOf_eq, Set.coe_setOf]

Premises used: Set.mem_setOf_eq, Set.coe_setOf
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
j : Fin (n + 1)
dsimp :
  Membership.mem (γ := Finset (Fin (n + 1)))
      (Finset.image (α := Fin (d + 1))
        (⇑(Hom.toOrderHom
              (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))) :
          (a : Fin (d + 1)) → Fin (n + 1))
        univ)
      j ↔
    ∃ (i : Fin (d + 1)), ((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i = j
⊢ Membership.mem (γ := Finset (Fin (n + 1)))
      (↑(((nonDegenerateEquiv' :
                (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
              (a : (↑(Δ[n].nonDegenerate d) : Type u)) → { x : Finset (Fin (n + 1)) // #x = d + 1 })
            x) :
        Finset (Fin (n + 1)))
      j ↔
    ∃ (i : Fin (d + 1)), ((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i = j

Tactic:
dsimp [nonDegenerateEquiv']

Premises used: SSet.stdSimplex.nonDegenerateEquiv'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
j : Fin (n + 1)
⊢ Membership.mem (γ := Finset (Fin (n + 1)))
      (Finset.image (α := Fin (d + 1))
        (⇑(Hom.toOrderHom
              (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))) :
          (a : Fin (d + 1)) → Fin (n + 1))
        univ)
      j ↔
    ∃ (i : Fin (d + 1)), ((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i = j

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
i : Fin (d + 1)
⊢ Membership.mem (γ := Finset (Fin ((unop (op ⦋d⦌)).len + 1))) univ i

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
left :
  Function.Injective (β :=
    ↥(↑(((nonDegenerateEquiv' :
                (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
              (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
            x) :
        Finset (Fin (n + 1))))
    fun (i : Fin (d + 1)) ↦
    Subtype.mk (p := fun (x_1 : Fin (n + 1)) ↦
      Membership.mem (γ := Finset (Fin (n + 1)))
        (↑(((nonDegenerateEquiv' :
                  (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
              x) :
          Finset (Fin (n + 1)))
        x_1)
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i) ⋯
right :
  Function.Surjective (β :=
    ↥(↑(((nonDegenerateEquiv' :
                (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
              (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
            x) :
        Finset (Fin (n + 1))))
    fun (i : Fin (d + 1)) ↦
    Subtype.mk (p := fun (x_1 : Fin (n + 1)) ↦
      Membership.mem (γ := Finset (Fin (n + 1)))
        (↑(((nonDegenerateEquiv' :
                  (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
              x) :
          Finset (Fin (n + 1)))
        x_1)
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i) ⋯
⊢ Function.Bijective (β :=
    ↥(↑(((nonDegenerateEquiv' :
                (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
              (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
            x) :
        Finset (Fin (n + 1))))
    fun (i : Fin (d + 1)) ↦
    Subtype.mk (p := fun (x_1 : Fin (n + 1)) ↦
      Membership.mem (γ := Finset (Fin (n + 1)))
        (↑(((nonDegenerateEquiv' :
                  (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
              x) :
          Finset (Fin (n + 1)))
        x_1)
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i) ⋯

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
⊢ Mono (C := SimplexCategory) (X := unop (op ⦋d⦌)) (Y := ⦋n⦌)
    (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))

Tactic:
have := (mem_nonDegenerate_iff_mono x.val).1 x.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
this :
  Mono (C := SimplexCategory) (X := unop (op ⦋d⦌)) (Y := ⦋n⦌)
    (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))
⊢ 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⦌) (↑x : Δ[n] _⦋d⦌))) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))

Tactic:
rw [SimplexCategory.mono_iff_injective] at this

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
this :
  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⦌) (↑x : Δ[n] _⦋d⦌))) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
x_1 x_2 : Fin (d + 1)
h :
  Eq (α :=
    ↥(↑(((nonDegenerateEquiv' :
                (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
              (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
            x) :
        Finset (Fin (n + 1))))
    ((fun (i : Fin (d + 1)) ↦
        (Subtype.mk (p := fun (x_3 : Fin (n + 1)) ↦
            Membership.mem (γ := Finset (Fin (n + 1)))
              (↑(((nonDegenerateEquiv' :
                        (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                      (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                    x) :
                Finset (Fin (n + 1)))
              x_3)
            (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i) ⋯ :
          ↥(↑(((nonDegenerateEquiv' :
                      (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                    (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                  x) :
              Finset (Fin (n + 1)))))
      x_1)
    ((fun (i : Fin (d + 1)) ↦
        (Subtype.mk (p := fun (x_3 : Fin (n + 1)) ↦
            Membership.mem (γ := Finset (Fin (n + 1)))
              (↑(((nonDegenerateEquiv' :
                        (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                      (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                    x) :
                Finset (Fin (n + 1)))
              x_3)
            (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i) ⋯ :
          ↥(↑(((nonDegenerateEquiv' :
                      (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                    (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                  x) :
              Finset (Fin (n + 1)))))
      x_2)
⊢ Eq (α := Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom
            (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌)
              (↑x : Δ[n] _⦋d⦌)) :
          (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
        x_1 :
      Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom
            (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌)
              (↑x : Δ[n] _⦋d⦌)) :
          (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
        x_2 :
      Fin (⦋n⦌.len + 1))

Tactic:
simpa using h