awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
⊢ Eq (α := Δ[0] ⟶ Δ[HAdd.hAdd (α := ℕ) 0 1]) (stdSimplex.δ 0)
    (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1 + 1)) → Δ[0 + 1] _⦋0⦌) 1))

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
refine : Monotone ![a, b]
⊢ Δ[n] _⦋1⦌

Tactic:
refine objMk ⟨![a, b], ?_⟩

Premises used: SSet.stdSimplex.objMk, OrderHom.mk, Matrix.vecCons
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
rw : ∀ (i : Fin (unop (op ⦋1⦌)).len), ![a, b] i.castSucc ≤ ![a, b] i.succ
⊢ Monotone ![a, b]

Tactic:
rw [Fin.monotone_iff_le_succ]

Premises used: Fin.monotone_iff_le_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
simp : ![a, b] (Fin.castSucc 0) ≤ ![a, b] (Fin.succ 0)
⊢ ∀ (i : Fin (unop (op ⦋1⦌)).len), ![a, b] i.castSucc ≤ ![a, b] i.succ

Tactic:
simp only [unop_op, len_mk, Fin.forall_fin_one]

Premises used: SimplexCategory.len_mk, Fin.forall_fin_one, Opposite.unop_op
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ ![a, b] (Fin.castSucc 0) ≤ ![a, b] (Fin.succ 0)

Tactic:
apply Fin.mk_le_mk.mpr hab

Premises used: Iff.mpr, Fin.mk_le_mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ (⇑(Hom.toOrderHom (ULift.down.{u_1, 0} (edge n a b hab))) : (a : Fin ((unop (op ⦋1⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) =
    ![a, b]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
refine : Monotone ![a, b, c]
⊢ Δ[n] _⦋2⦌

Tactic:
refine objMk ⟨![a, b, c], ?_⟩

Premises used: SSet.stdSimplex.objMk, OrderHom.mk, Matrix.vecCons
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
rw : ∀ (i : Fin (unop (op ⦋2⦌)).len), ![a, b, c] i.castSucc ≤ ![a, b, c] i.succ
⊢ Monotone ![a, b, c]

Tactic:
rw [Fin.monotone_iff_le_succ]

Premises used: Fin.monotone_iff_le_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
simp : ![a, b, c] (Fin.castSucc 0) ≤ ![a, b, c] (Fin.succ 0) ∧ ![a, b, c] (Fin.castSucc 1) ≤ ![a, b, c] (Fin.succ 1)
⊢ ∀ (i : Fin (unop (op ⦋2⦌)).len), ![a, b, c] i.castSucc ≤ ![a, b, c] i.succ

Tactic:
simp only [unop_op, len_mk, Fin.forall_fin_two]

Premises used: Fin.forall_fin_two, SimplexCategory.len_mk, Opposite.unop_op
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
dsimp : a ≤ b ∧ b ≤ c
⊢ ![a, b, c] (Fin.castSucc 0) ≤ ![a, b, c] (Fin.succ 0) ∧ ![a, b, c] (Fin.castSucc 1) ≤ ![a, b, c] (Fin.succ 1)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ b ∧ b ≤ c

Tactic:
simp only [*, true_and]

Premises used: true_and
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ (⇑(Hom.toOrderHom (ULift.down.{u_1, 0} (triangle a b c hab hbc))) :
      (a : Fin ((unop (op ⦋2⦌)).len + 1)) → Fin (⦋n⦌.len + 1)) =
    ![a, b, c]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
U V : SimplexCategoryᵒᵖ
i : U ⟶ V
⊢ Subset (α := Set (Δ[n].obj U))
    {f : Δ[n].obj U |
      Finset.image (α := Fin ((unop U).len + 1))
          (⇑(Hom.toOrderHom (((objEquiv : Δ[n].obj U ≃ (unop U ⟶ ⦋n⦌)) : (a : Δ[n].obj U) → unop U ⟶ ⦋n⦌) f)) :
            (a : Fin ((unop U).len + 1)) → Fin (⦋n⦌.len + 1))
          ⊤ ≤
        S}
    (Set.preimage (β := (fun (X : Type u) ↦ X) (Δ[n].obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map i)) :
        (a : (fun (X : Type u) ↦ X) (Δ[n].obj U)) → (fun (X : Type u) ↦ X) (Δ[n].obj V))
      {f : Δ[n].obj V |
        Finset.image (α := Fin ((unop V).len + 1))
            (⇑(Hom.toOrderHom (((objEquiv : Δ[n].obj V ≃ (unop V ⟶ ⦋n⦌)) : (a : Δ[n].obj V) → unop V ⟶ ⦋n⦌) f)) :
              (a : Fin ((unop V).len + 1)) → Fin (⦋n⦌.len + 1))
            ⊤ ≤
          S})

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
x : Δ[n] _⦋d⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) ((face S).obj (op ⦋d⦌)) x ↔
    ∀ (i : Fin (d + 1)), Membership.mem (α := Fin (n + 1)) S ((x : (a : Fin (d + 1)) → Fin (n + 1)) i : Fin (n + 1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
⊢ face S₁ ⊓ face S₂ = face (S₁ ⊓ S₂)

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
obj :
  ∀ (x : SimplexCategoryᵒᵖ) (x_1 : Δ[n].obj x),
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face ∅) x) x_1 ↔
      Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊥ x) x_1
⊢ Eq.{u + 1} (α := Δ[n].Subcomplex) (face ∅) ⊥

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
⊢ Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face ∅) x) x_1 ↔
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊥ x) x_1

Tactic:
simpa using Finset.univ_neq_empty _

Premises used: Finset.univ_neq_empty
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
obj :
  ∀ (x : SimplexCategoryᵒᵖ) (x_1 : Δ[n].obj x),
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face univ) x) x_1 ↔
      Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊤ x) x_1
⊢ Eq.{u + 1} (α := Δ[n].Subcomplex) (face univ) ⊤

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
obj : Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face univ) x) x_1
⊢ Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face univ) x) x_1 ↔
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊤ x) x_1

Tactic:
simp only [Subfunctor.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]

Premises used: iff_true, Set.top_eq_univ, Set.mem_univ, CategoryTheory.Subfunctor.top_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
⊢ Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face univ) x) x_1

Tactic:
apply Finset.subset_univ

Premises used: Finset.subset_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X Y : SSet
n : SimplexCategory
f : stdSimplex.obj n ⟶ X
g : X ⟶ Y
⊢ Eq (α := Y.obj (op n)) ((yonedaEquiv : (a : stdSimplex.obj n ⟶ Y) → Y.obj (op n)) (f ≫ g) : Y.obj (op n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app (op n)) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op n))) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
        ((yonedaEquiv : (a : stdSimplex.obj n ⟶ X) → X.obj (op n)) f : X.obj (op n)) :
      (fun (X : Type u) ↦ X) (Y.obj (op n)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x) (op ⦋n⦌)) :
        (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n]) → Δ[n] _⦋n⦌) (𝟙 Δ[n]) : Δ[n] _⦋n⦌) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
n : ℕ
f : Δ[n] ⟶ X
⊢ range f = ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ X) → X _⦋n⦌) f)

Tactic:
Subfunctor.range_eq_ofSection' _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Subfunctor.range_eq_ofSection'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
A : X.Subcomplex
n : SimplexCategory
f : stdSimplex.obj n ⟶ A.toSSet
⊢ Eq (α := X.obj (op n))
    ((↑((yonedaEquiv : (a : stdSimplex.obj n ⟶ A.toSSet) → A.toSSet.obj (op n)) f) : X.obj (op n)) : X.obj (op n))
    ((yonedaEquiv : (a : stdSimplex.obj n ⟶ X) → X.obj (op n)) (f ≫ A.ι) : X.obj (op n))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
i : Fin (n + 1)
h :
  Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S).obj (op ⦋0⦌))
    ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)
⊢ i ∈ S

Tactic:
simpa using h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
i : Fin (n + 1)
⊢ i ∈ S →
    Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S).obj (op ⦋0⦌))
      ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
⊢ face S₁ ≤ face S₂ ↔ S₁ ≤ S₂

Tactic:
⟨fun h i hi ↦ ?_, fun h d a ha ↦ ha.trans h⟩

Premises used: Iff.intro, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
refine : ∀ (h : face S₁ ≤ face S₂) (i : Fin (n + 1)) (hi : i ∈ S₁), i ∈ S₂
⊢ face S₁ ≤ face S₂ ↔ S₁ ≤ S₂

Tactic:
refine ⟨fun h i hi ↦ ?_, fun h d a ha ↦ ha.trans h⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
h : face S₁ ≤ face S₂
i : Fin (n + 1)
hi : i ∈ S₁
simp :
  ∀
    (hi :
      Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S₁).obj (op ⦋0⦌))
        ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)),
    Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S₂).obj (op ⦋0⦌))
      ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)
⊢ i ∈ S₂

Tactic:
simp only [← obj₀Equiv_symm_mem_face_iff.{u}] at hi ⊢
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
h : face S₁ ≤ face S₂
i : Fin (n + 1)
hi :
  Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S₁).obj (op ⦋0⦌))
    ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)
⊢ Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S₂).obj (op ⦋0⦌))
    ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)

Tactic:
h _ hi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
h : face S₁ ≤ face S₂
i : Fin (n + 1)
hi :
  Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S₁).obj (op ⦋0⦌))
    ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)
⊢ Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S₂).obj (op ⦋0⦌))
    ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)

Tactic:
exact h _ hi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
a :
  face S ≤
    Subcomplex.ofSimplex
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))
a₁ :
  Subcomplex.ofSimplex
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) ≤
    face S
⊢ face S =
    Subcomplex.ofSimplex
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : SimplexCategory
x : Δ[n].obj (op k)
hx : Membership.mem (γ := Set (Δ[n].obj (op k))) ((face S).obj (op k)) x
a :
  ∀ (k : ℕ) ⦃x : Δ[n] _⦋k⦌⦄ (hx : Membership.mem (γ := Set (Δ[n] _⦋k⦌)) ((face S).obj (op ⦋k⦌)) x),
    Membership.mem (γ := Set (Δ[n] _⦋k⦌))
      ((Subcomplex.ofSimplex
            (objMk
              (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))).obj
        (op ⦋k⦌))
      x
⊢ Membership.mem (γ := Set (Δ[n].obj (op k)))
    ((Subcomplex.ofSimplex
          (objMk
            (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))).obj
      (op k))
    x

Tactic:
induction k using SimplexCategory.rec with | _ k
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋k⦌)) ((face S).obj (op ⦋k⦌)) x
⊢ ∀ (i : Fin (k + 1)), Membership.mem (α := Fin (n + 1)) S ((x : (a : Fin (k + 1)) → Fin (n + 1)) i : Fin (n + 1))

Tactic:
rw [mem_face_iff] at hx

Premises used: SSet.stdSimplex.mem_face_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : ∀ (i : Fin (k + 1)), Membership.mem (α := Fin (n + 1)) S ((x : (a : Fin (k + 1)) → Fin (n + 1)) i : Fin (n + 1))
φ : Fin (k + 1) →o ↥S :=
  {
    toFun := fun (i : Fin (k + 1)) ↦
      Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (k + 1)) → Fin (n + 1)) i) ⋯,
    monotone' := ⋯ }
⊢ Membership.mem (γ := Set (Δ[n] _⦋k⦌))
    ((Subcomplex.ofSimplex
          (objMk
            (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))).obj
      (op ⦋k⦌))
    x

Tactic:
⟨Quiver.Hom.op
      (SimplexCategory.Hom.mk ((e.symm.toOrderEmbedding.toOrderHom.comp φ))), ?_⟩

Premises used: OrderIso.toOrderEmbedding, Set.Mem, Quiver.Hom.op, setOf, OrderHom.comp, OrderIso.symm, Exists.intro, OrderEmbedding.toOrderHom, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : ∀ (i : Fin (k + 1)), Membership.mem (α := Fin (n + 1)) S ((x : (a : Fin (k + 1)) → Fin (n + 1)) i : Fin (n + 1))
φ : Fin (k + 1) →o ↥S :=
  {
    toFun := fun (i : Fin (k + 1)) ↦
      Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (k + 1)) → Fin (n + 1)) i) ⋯,
    monotone' := ⋯ }
a :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Δ[n].map (Quiver.Hom.op (Hom.mk (e.symm.toOrderEmbedding.toOrderHom.comp φ)))) :
        (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌))
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) =
    x
⊢ Membership.mem (γ := Set (Δ[n] _⦋k⦌))
    ((Subcomplex.ofSimplex
          (objMk
            (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))).obj
      (op ⦋k⦌))
    x

Tactic:
refine ⟨Quiver.Hom.op
      (SimplexCategory.Hom.mk ((e.symm.toOrderEmbedding.toOrderHom.comp φ))), ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : ∀ (i : Fin (k + 1)), Membership.mem (α := Fin (n + 1)) S ((x : (a : Fin (k + 1)) → Fin (n + 1)) i : Fin (n + 1))
φ : Fin (k + 1) →o ↥S :=
  {
    toFun := fun (i : Fin (k + 1)) ↦
      Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (k + 1)) → Fin (n + 1)) i) ⋯,
    monotone' := ⋯ }
a :
  ∀ (j : Fin (k + 1)),
    Eq (α := Fin (n + 1))
      ((((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Δ[n].map (Quiver.Hom.op (Hom.mk (e.symm.toOrderEmbedding.toOrderHom.comp φ)))) :
                  (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌))
                (objMk
                  (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) :
              (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌)) :
            (a : Fin (k + 1)) → Fin (n + 1))
          j :
        Fin (n + 1))
      ((x : (a : Fin (k + 1)) → Fin (n + 1)) j : Fin (n + 1))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Δ[n].map (Quiver.Hom.op (Hom.mk (e.symm.toOrderEmbedding.toOrderHom.comp φ)))) :
        (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌))
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) =
    x

Tactic:
ext j : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : ∀ (i : Fin (k + 1)), Membership.mem (α := Fin (n + 1)) S ((x : (a : Fin (k + 1)) → Fin (n + 1)) i : Fin (n + 1))
φ : Fin (k + 1) →o ↥S :=
  {
    toFun := fun (i : Fin (k + 1)) ↦
      Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (k + 1)) → Fin (n + 1)) i) ⋯,
    monotone' := ⋯ }
j : Fin (k + 1)
⊢ Eq (α := Fin (n + 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Δ[n].map (Quiver.Hom.op (Hom.mk (e.symm.toOrderEmbedding.toOrderHom.comp φ)))) :
                (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌))
              (objMk
                (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) :
            (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌)) :
          (a : Fin (k + 1)) → Fin (n + 1))
        j :
      Fin (n + 1))
    ((x : (a : Fin (k + 1)) → Fin (n + 1)) j : Fin (n + 1))

Tactic:
simpa only [Subtype.ext_iff] using e.apply_symm_apply ⟨_, hx j⟩

Premises used: OrderIso.apply_symm_apply, Subtype.ext_iff, Subtype.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ Subcomplex.ofSimplex
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) ≤
    face S

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
f : j ⟶ ⦋m⦌
x : Fin (⦋n⦌.len + 1)
⊢ Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1)))
      (Finset.image (α := Fin ((unop (op j)).len + 1))
        (⇑(Hom.toOrderHom
              (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → unop (op j) ⟶ ⦋n⦌)
                (objMk
                  (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                    (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f)))))) :
          (a : Fin ((unop (op j)).len + 1)) → Fin (⦋n⦌.len + 1))
        ⊤)
      x →
    x ∈ S

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x_1 : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x
i : Fin (j.len + 1)
⊢ Membership.mem (α := Fin (⦋n⦌.len + 1)) (γ := Finset (Fin (⦋n⦌.len + 1)))
    (Finset.image (α := Fin ((unop (op j)).len + 1))
      (⇑(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))
      ⊤)
    ((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 :
      Fin (⦋n⦌.len + 1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x_1 : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x
i₁ i₂ : Fin (j.len + 1)
h : i₁ ≤ i₂
simp :
  LE.le (α := Fin (n + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → j ⟶ ⦋n⦌) x) :
          (a : Fin (j.len + 1)) → Fin (n + 1))
        i₁ :
      Fin (n + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → j ⟶ ⦋n⦌) x) :
          (a : Fin (j.len + 1)) → Fin (n + 1))
        i₂ :
      Fin (n + 1))
⊢ LE.le (α := ↥S)
    (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₁)
        ⋯ :
      ↥S)
    (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₂)
        ⋯ :
      ↥S)

Tactic:
simp only [Subtype.mk_le_mk]

Premises used: Subtype.mk_le_mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x_1 : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x
i₁ i₂ : Fin (j.len + 1)
h : i₁ ≤ i₂
⊢ LE.le (α := Fin (n + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → j ⟶ ⦋n⦌) x) :
          (a : Fin (j.len + 1)) → Fin (n + 1))
        i₁ :
      Fin (n + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → j ⟶ ⦋n⦌) x) :
          (a : Fin (j.len + 1)) → Fin (n + 1))
        i₂ :
      Fin (n + 1))

Tactic:
OrderHom.monotone _ h

Premises used: OrderHom.monotone
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x_1 : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x
i₁ i₂ : Fin (j.len + 1)
h : i₁ ≤ i₂
⊢ LE.le (α := Fin (n + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → j ⟶ ⦋n⦌) x) :
          (a : Fin (j.len + 1)) → Fin (n + 1))
        i₁ :
      Fin (n + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → j ⟶ ⦋n⦌) x) :
          (a : Fin (j.len + 1)) → Fin (n + 1))
        i₂ :
      Fin (n + 1))

Tactic:
exact OrderHom.monotone _ h

Premises used: OrderHom.monotone