awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ 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) ⋯

Tactic:
exact fun _ _ h ↦ this (by simpa using h)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
j : Fin (n + 1)
hj :
  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:
rw [nonDegenerateEquiv'_iff] at hj

Premises used: SSet.stdSimplex.nonDegenerateEquiv'_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
j : Fin (n + 1)
hj_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)))
    j
hj : ∃ (i : Fin (d + 1)), ((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i = j
⊢ ∃ (a : Fin (d + 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) ⋯ :
            ↥(↑(((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)))))
        a =
      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)
        j hj_1

Tactic:
aesop
-- 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))
a b : Fin (d + 1)
simp :
  LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1)) ↔
    a ≤ b
⊢ LE.le (α :=
      ↥(↑(((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))))
      (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)) → { x : Finset (Fin (n + 1)) // #x = d + 1 })
                  x) :
              Finset (Fin (n + 1)))
            x_1)
          (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a) ⋯ :
        ↥(↑(((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))))
      (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)) → { x : Finset (Fin (n + 1)) // #x = d + 1 })
                  x) :
              Finset (Fin (n + 1)))
            x_1)
          (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b) ⋯ :
        ↥(↑(((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)))) ↔
    a ≤ b

Tactic:
simp only [Subtype.mk_le_mk]

Premises used: Subtype.mk_le_mk
-- 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))
a b : Fin (d + 1)
mp :
  LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1)) →
    a ≤ b
mpr :
  a ≤ b →
    LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
⊢ LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1)) ↔
    a ≤ b

Tactic:
constructor
-- 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))
a b : Fin (d + 1)
mp :
  ¬LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
        (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1)) →
    ¬b < a
⊢ LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1)) →
    a ≤ b

Tactic:
rw [← not_lt, ← not_lt]

Premises used: not_lt
-- 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))
a b : Fin (d + 1)
h :
  ¬LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
h' : b < a
mp :
  LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
⊢ False

Tactic:
apply h
-- 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))
a b : Fin (d + 1)
h :
  ¬LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
h' : b < a
mp :
  ∀
    (h'' :
      LT.lt (α := Fin (n + 1))
        ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) b)
        ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) a)),
    LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
mp₁ :
  ∀
    (h'' :
      Eq (α := Fin (n + 1))
        ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) b)
        ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) a)),
    LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
⊢ LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))

Tactic:
obtain h'' | h'' := (monotone_apply x.val h'.le).lt_or_eq

Premises used: LE.le.lt_or_eq, LT.lt.le, SSet.stdSimplex.monotone_apply, Subtype.val
-- 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))
a b : Fin (d + 1)
h :
  ¬LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
h' : b < a
h'' :
  LT.lt (α := Fin (n + 1))
    ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) b)
    ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) a)
⊢ LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))

Tactic:
assumption
-- 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))
a b : Fin (d + 1)
h :
  ¬LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
h' : b < a
h'' :
  Eq (α := Fin (n + 1))
    ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) b)
    ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) a)
⊢ LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))

Tactic:
simp only [this h'', lt_self_iff_false] at h'

Premises used: lt_self_iff_false
-- 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))
a b : Fin (d + 1)
h : a ≤ b
⊢ LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))

Tactic:
monotone_apply _ h

Premises used: SSet.stdSimplex.monotone_apply
-- 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))
a b : Fin (d + 1)
h : a ≤ b
⊢ LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))

Tactic:
exact monotone_apply _ h

Premises used: SSet.stdSimplex.monotone_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
⊢ face
      (↑(((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))) =
    Subcomplex.ofSimplex (↑x : Δ[n] _⦋d⦌)

Tactic:
face_eq_ofSimplex.{u} _ _ (orderIsoOfNonDegenerate x)

Premises used: SSet.stdSimplex.face_eq_ofSimplex, OrderHom.comp, SSet.stdSimplex.orderIsoOfNonDegenerate, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
S : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)
i : Fin (d + 1)
obtain :
  ∀ (f : (↑(Δ[n].nonDegenerate d) : Type u)),
    Membership.mem (α := Fin (n + 1)) (γ := 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))
            f) :
        Finset (Fin (n + 1)))
      (((↑((Equiv.symm nonDegenerateEquiv' :
                    (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
                  (((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))
                      f :
                    (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
              Δ[n] _⦋d⦌) :
            (a : Fin (d + 1)) → Fin (n + 1))
          i :
        Fin (n + 1))
⊢ Membership.mem (α := Fin (n + 1)) (↑S : Finset (Fin (n + 1)))
    (((↑((Equiv.symm nonDegenerateEquiv' :
                  (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
                S) :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))

Tactic:
obtain ⟨f, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
i : Fin (d + 1)
f : (↑(Δ[n].nonDegenerate d) : Type u)
dsimp :
  Membership.mem (α := Fin (n + 1)) (γ := Finset (Fin (n + 1)))
    (Finset.image (α := Fin (d + 1))
      (⇑(Hom.toOrderHom
            (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑f : Δ[n] _⦋d⦌))) :
        (a : Fin (d + 1)) → Fin (n + 1))
      univ)
    (((↑(((Equiv.ofBijective
                      (fun (x : { x : Δ[n] _⦋d⦌ // Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) x }) ↦
                        Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦ #x = d + 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)
                          ⋯)
                      ⋯).symm :
                  (a : { x : Finset (Fin (n + 1)) // #x = d + 1 }) → (↑(Δ[n].nonDegenerate d) : Type u))
                (Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦ #x = d + 1)
                  (Finset.image (α := Fin (d + 1))
                    (⇑(Hom.toOrderHom
                          (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌)
                            (↑f : Δ[n] _⦋d⦌))) :
                      (a : Fin (d + 1)) → Fin (n + 1))
                    univ)
                  ⋯)) :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
⊢ Membership.mem (α := Fin (n + 1)) (γ := 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))
          f) :
      Finset (Fin (n + 1)))
    (((↑((Equiv.symm nonDegenerateEquiv' :
                  (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
                (((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))
                    f :
                  (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))

Tactic:
dsimp [nonDegenerateEquiv']

Premises used: SSet.stdSimplex.nonDegenerateEquiv'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
i : Fin (d + 1)
f : (↑(Δ[n].nonDegenerate d) : Type u)
simp :
  ∃ (a : Fin (d + 1)),
    Eq (α := Fin (n + 1))
      ((Hom.toOrderHom
              (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑f : Δ[n] _⦋d⦌)) :
            (a : Fin (d + 1)) → Fin (n + 1))
          a :
        Fin (n + 1))
      (((↑f : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i : Fin (n + 1))
⊢ Membership.mem (α := Fin (n + 1)) (γ := Finset (Fin (n + 1)))
    (Finset.image (α := Fin (d + 1))
      (⇑(Hom.toOrderHom
            (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑f : Δ[n] _⦋d⦌))) :
        (a : Fin (d + 1)) → Fin (n + 1))
      univ)
    (((↑(((Equiv.ofBijective
                      (fun (x : { x : Δ[n] _⦋d⦌ // Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) x }) ↦
                        Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦ #x = d + 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)
                          ⋯)
                      ⋯).symm :
                  (a : { x : Finset (Fin (n + 1)) // #x = d + 1 }) → (↑(Δ[n].nonDegenerate d) : Type u))
                (Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦ #x = d + 1)
                  (Finset.image (α := Fin (d + 1))
                    (⇑(Hom.toOrderHom
                          (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌)
                            (↑f : Δ[n] _⦋d⦌))) :
                      (a : Fin (d + 1)) → Fin (n + 1))
                    univ)
                  ⋯)) :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))

Tactic:
simp only [Equiv.ofBijective_symm_apply_apply, Finset.mem_image, Finset.mem_univ, true_and]

Premises used: Finset.mem_univ, Finset.mem_image, Equiv.ofBijective_symm_apply_apply, true_and
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
i : Fin (d + 1)
f : (↑(Δ[n].nonDegenerate d) : Type u)
⊢ ∃ (a : Fin (d + 1)),
    Eq (α := Fin (n + 1))
      ((Hom.toOrderHom
              (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑f : Δ[n] _⦋d⦌)) :
            (a : Fin (d + 1)) → Fin (n + 1))
          a :
        Fin (n + 1))
      (((↑f : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i : Fin (n + 1))

Tactic:
⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
i : Fin (d + 1)
f : (↑(Δ[n].nonDegenerate d) : Type u)
⊢ ∃ (a : Fin (d + 1)),
    Eq (α := Fin (n + 1))
      ((Hom.toOrderHom
              (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑f : Δ[n] _⦋d⦌)) :
            (a : Fin (d + 1)) → Fin (n + 1))
          a :
        Fin (n + 1))
      (((↑f : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i : Fin (n + 1))

Tactic:
exact ⟨i, rfl⟩