awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Splitting
Goal:
X : SSet
x_1 : SimplexCategoryᵒᵖ
n : ℕ
x_2 : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property : Epi f
x y :
  SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α })
      (Opposite.op ⦋m⦌)
      (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) f
        property))
h :
  Eq (α :=
    Functor.CoconeTypes.pt (J := Discrete (SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌))) (F :=
      Discrete.functor
        (SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌))))
    (CofanTypes.inj (F :=
      SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
        { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α }) (Opposite.op ⦋m⦌)
        (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) f
          property))
      x)
    (CofanTypes.inj (F :=
      SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
        { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α }) (Opposite.op ⦋m⦌)
        (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) f
          property))
      y)
⊢ x = y

Tactic:
unique_nonDegenerate_simplex _ _ _ _ rfl _ _ h

Premises used: CategoryTheory.SimplicialObject.Splitting.summand, SSet.unique_nonDegenerate_simplex, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Splitting
Goal:
X : SSet
x_1 : SimplexCategoryᵒᵖ
n : ℕ
x_2 : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property : Epi f
x y :
  SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α })
      (Opposite.op ⦋m⦌)
      (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) f
        property))
h :
  Eq (α :=
    Functor.CoconeTypes.pt (J := Discrete (SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌))) (F :=
      Discrete.functor
        (SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌))))
    (CofanTypes.inj (F :=
      SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
        { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α }) (Opposite.op ⦋m⦌)
        (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) f
          property))
      x)
    (CofanTypes.inj (F :=
      SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
        { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α }) (Opposite.op ⦋m⦌)
        (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) f
          property))
      y)
⊢ x = y

Tactic:
exact unique_nonDegenerate_simplex _ _ _ _ rfl _ _ h

Premises used: SSet.unique_nonDegenerate_simplex, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
⊢ stdSimplex.map (Hom.mk OrderHom.id) = 𝟙 (stdSimplex.obj n)

Tactic:
CategoryTheory.Functor.map_id _ _

Premises used: OrderHom.id, SimplexCategory.Hom.id, CategoryTheory.Functor.map_id, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
m : SimplexCategoryᵒᵖ
a b : (stdSimplex.obj n).obj m
⊢ Eq (α := unop m ⟶ n)
      (((objEquiv : (stdSimplex.obj n).obj m ≃ (unop m ⟶ n)) : (a : (stdSimplex.obj n).obj m) → unop m ⟶ n) a :
        unop m ⟶ n)
      (((objEquiv : (stdSimplex.obj n).obj m ≃ (unop m ⟶ n)) : (a : (stdSimplex.obj n).obj m) → unop m ⟶ n) b :
        unop m ⟶ n) ↔
    a = b

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
x x_1 : Δ[n] _⦋i⦌
h :
  Eq (α := (a : Fin (i + 1)) → Fin (n + 1))
    ((fun (x : Δ[n] _⦋i⦌) (j : Fin (i + 1)) ↦
        ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x) :
              (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
            j :
          Fin (⦋n⦌.len + 1)))
      x)
    ((fun (x : Δ[n] _⦋i⦌) (j : Fin (i + 1)) ↦
        ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x) :
              (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
            j :
          Fin (⦋n⦌.len + 1)))
      x_1)
a :
  ∀ (x_2 : Fin ((unop (op ⦋i⦌)).len + 1)),
    Eq (α := Fin (⦋n⦌.len + 1))
      ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x) :
            (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
          x_2 :
        Fin (⦋n⦌.len + 1))
      ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x_1) :
            (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
          x_2 :
        Fin (⦋n⦌.len + 1))
⊢ Eq (α := unop (op ⦋i⦌) ⟶ ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x : unop (op ⦋i⦌) ⟶ ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x_1 : unop (op ⦋i⦌) ⟶ ⦋n⦌)

Tactic:
ext : 3
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
x x_1 : Δ[n] _⦋i⦌
h :
  Eq (α := (a : Fin (i + 1)) → Fin (n + 1))
    ((fun (x : Δ[n] _⦋i⦌) (j : Fin (i + 1)) ↦
        ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x) :
              (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
            j :
          Fin (⦋n⦌.len + 1)))
      x)
    ((fun (x : Δ[n] _⦋i⦌) (j : Fin (i + 1)) ↦
        ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x) :
              (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
            j :
          Fin (⦋n⦌.len + 1)))
      x_1)
x_2 : Fin ((unop (op ⦋i⦌)).len + 1)
⊢ Eq (α := Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x) :
          (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
        x_2 :
      Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x_1) :
          (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
        x_2 :
      Fin (⦋n⦌.len + 1))

Tactic:
apply congr_fun h

Premises used: congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
x : Δ[n] _⦋i⦌
⊢ Monotone (β := Fin (n + 1)) fun (j : Fin (i + 1)) ↦ (x : (a : Fin (i + 1)) → Fin (n + 1)) j

Tactic:
(objEquiv x).toOrderHom.monotone

Premises used: OrderHom.monotone, SimplexCategory.Hom.toOrderHom, DFunLike.coe, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
x y : Δ[n] _⦋d⦌
h :
  ∀ (i : Fin (d + 1)),
    Eq (α := Fin (n + 1)) ((x : (a : Fin (d + 1)) → Fin (n + 1)) i : Fin (n + 1))
      ((y : (a : Fin (d + 1)) → Fin (n + 1)) i : Fin (n + 1))
⊢ x = y

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
x : Δ[n] _⦋i⦌
j : Fin (i + 1)
⊢ Eq (α := Fin (n + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → ⦋i⦌ ⟶ ⦋n⦌) x) :
          (a : Fin (i + 1)) → Fin (n + 1))
        j :
      Fin (n + 1))
    ((x : (a : Fin (i + 1)) → Fin (n + 1)) j : Fin (n + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n n' : SimplexCategory
m : SimplexCategoryᵒᵖ
f : unop m ⟶ n
g : n ⟶ n'
⊢ Eq.{u + 1} (α := (stdSimplex.obj n').obj m)
    ((Equiv.symm objEquiv : (a : unop m ⟶ n') → (stdSimplex.obj n').obj m) (f ≫ g) : (stdSimplex.obj n').obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.map g).app m) :
          (a : (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj m)) → (fun (X : Type u) ↦ X) ((stdSimplex.obj n').obj m))
        ((Equiv.symm objEquiv : (a : unop m ⟶ n) → (stdSimplex.obj n).obj m) f : (stdSimplex.obj n).obj m) :
      (fun (X : Type u) ↦ X) ((stdSimplex.obj n').obj m))

Tactic:
rfl

Premises used: OrderHom.comp, SimplexCategory.Hom.comp, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
m m' : SimplexCategoryᵒᵖ
f : unop m ⟶ n
g : m ⟶ m'
⊢ Eq (α := (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj m'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map g) :
          (a : (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj m)) → (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj m'))
        ((Equiv.symm objEquiv : (a : unop m ⟶ n) → (stdSimplex.obj n).obj m) f : (stdSimplex.obj n).obj m) :
      (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj m'))
    ((Equiv.symm objEquiv : (a : unop m' ⟶ n) → (stdSimplex.obj n).obj m') (g.unop ≫ f) : (stdSimplex.obj n).obj m')

Tactic:
rfl

Premises used: OrderHom.comp, SimplexCategory.Hom.comp, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
f : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ Eq (α := Fin (n + 1))
    ((((Equiv.symm objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) : (a : Fin (m + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) i : Fin (⦋n⦌.len + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
m : SimplexCategory
f : ⦋n + 1⦌ ⟶ m
i : Fin (n + 2)
⊢ Eq (α := stdSimplex.obj m _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (stdSimplex.obj m) i) :
          (a : stdSimplex.obj m _⦋n + 1⦌) → stdSimplex.obj m _⦋n⦌)
        ((Equiv.symm objEquiv : (a : ⦋n + 1⦌ ⟶ m) → stdSimplex.obj m _⦋n + 1⦌) f : stdSimplex.obj m _⦋n + 1⦌) :
      stdSimplex.obj m _⦋n⦌)
    ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ m) → stdSimplex.obj m _⦋n⦌) (δ i ≫ f) : stdSimplex.obj m _⦋n⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
m : SimplexCategory
f : ⦋n⦌ ⟶ m
i : Fin (n + 1)
⊢ Eq (α := stdSimplex.obj m _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (stdSimplex.obj m) i) :
          (a : stdSimplex.obj m _⦋n⦌) → stdSimplex.obj m _⦋n + 1⦌)
        ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ m) → stdSimplex.obj m _⦋n⦌) f : stdSimplex.obj m _⦋n⦌) :
      stdSimplex.obj m _⦋n + 1⦌)
    ((Equiv.symm objEquiv : (a : ⦋n + 1⦌ ⟶ m) → stdSimplex.obj m _⦋n + 1⦌) (σ i ≫ f) : stdSimplex.obj m _⦋n + 1⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
f : Fin (m + 1) →o Fin (n + 1)
i : Fin (m + 1)
⊢ Eq (α := Fin (n + 1)) ((objMk f : (a : Fin (m + 1)) → Fin (n + 1)) i : Fin (n + 1))
    ((f : (a : Fin (m + 1)) → Fin (n + 1)) i : Fin (n + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
m : SimplexCategoryᵒᵖ
⊢ Function.Bijective.{1, u_1 + 1} (α := Fin ((unop m).len + 1) →o Fin (n.len + 1)) objMk

Tactic:
(objEquiv.trans homEquivOrderHom).symm.bijective

Premises used: Equiv.bijective, Equiv.trans, SimplexCategory.homEquivOrderHom, Equiv.symm, SSet.stdSimplex.objEquiv, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
n : SimplexCategory
x : (stdSimplex.obj n).obj m₁
⊢ Eq (α := (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj m₂))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.obj n).map f) :
          (a : (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj m₁)) → (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj m₂))
        x :
      (fun (X : Type u) ↦ X) ((stdSimplex.obj n).obj m₂))
    ((Equiv.symm objEquiv : (a : unop m₂ ⟶ n) → (stdSimplex.obj n).obj m₂)
        (f.unop ≫
          ((objEquiv : (stdSimplex.obj n).obj m₁ ≃ (unop m₁ ⟶ n)) : (a : (stdSimplex.obj n).obj m₁) → unop m₁ ⟶ n) x) :
      (stdSimplex.obj n).obj m₂)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
α : ⦋n⦌ ⟶ ⦋m⦌
⊢ Eq (α := (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (m + 1))
    (⇑(asOrderHom.{u} ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋m⦌) → Δ[m] _⦋n⦌) α)) :
      (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (m + 1))
    (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) α) :
      (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋m⦌)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
n : SimplexCategory
inst : DecidableEq (X.obj (op n))
a b : stdSimplex.obj n ⟶ X
⊢ Eq (α := X.obj (op n)) ((yonedaEquiv : (a : stdSimplex.obj n ⟶ X) → X.obj (op n)) a : X.obj (op n))
      ((yonedaEquiv : (a : stdSimplex.obj n ⟶ X) → X.obj (op n)) b : X.obj (op n)) ↔
    a = b

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X Y : SSet
n : SimplexCategory
x : X.obj (op n)
f : X ⟶ Y
⊢ Eq (α := stdSimplex.obj n ⟶ Y) ((Equiv.symm yonedaEquiv : (a : X.obj (op n)) → stdSimplex.obj n ⟶ X) x ≫ f)
    ((Equiv.symm yonedaEquiv : (a : Y.obj (op n)) → stdSimplex.obj n ⟶ Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op n)) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op n))) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
          x :
        (fun (X : Type u) ↦ X) (Y.obj (op n))))

Tactic:
uliftYonedaEquiv_symm_comp ..

Premises used: CategoryTheory.uliftYonedaEquiv_symm_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
x : X _⦋0⦌
⊢ (yonedaEquiv : (a : Δ[0] ⟶ X) → X _⦋0⦌) (const x) = x

Tactic:
simp [yonedaEquiv, uliftYonedaEquiv]

Premises used: SSet.yonedaEquiv, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
x : X _⦋0⦌
a :
  Eq (α := X _⦋0⦌)
    ((yonedaEquiv : (a : Δ[0] ⟶ X) → X _⦋0⦌) ((Equiv.symm yonedaEquiv : (a : X _⦋0⦌) → Δ[0] ⟶ X) x : Δ[0] ⟶ X) : X _⦋0⦌)
    ((yonedaEquiv : (a : Δ[0] ⟶ X) → X _⦋0⦌) (const x) : X _⦋0⦌)
⊢ Eq (α := Δ[0] ⟶ X) ((Equiv.symm yonedaEquiv : (a : X _⦋0⦌) → Δ[0] ⟶ X) x : Δ[0] ⟶ X) (const x : Δ[0] ⟶ X)

Tactic:
apply yonedaEquiv.injective

Premises used: SSet.yonedaEquiv, Equiv.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
x : X _⦋0⦌
⊢ Eq (α := X _⦋0⦌)
    ((yonedaEquiv : (a : Δ[0] ⟶ X) → X _⦋0⦌) ((Equiv.symm yonedaEquiv : (a : X _⦋0⦌) → Δ[0] ⟶ X) x : Δ[0] ⟶ X) : X _⦋0⦌)
    ((yonedaEquiv : (a : Δ[0] ⟶ X) → X _⦋0⦌) (const x) : X _⦋0⦌)

Tactic:
simp [yonedaEquiv_const]

Premises used: SSet.yonedaEquiv_const
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : SimplexCategory
f : n ⟶ m
⊢ Eq (α := (stdSimplex.obj m).obj (op n))
    ((yonedaEquiv : (a : stdSimplex.obj n ⟶ stdSimplex.obj m) → (stdSimplex.obj m).obj (op n)) (stdSimplex.map f) :
      (stdSimplex.obj m).obj (op n))
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op n) ⟶ m) → (stdSimplex.obj m).obj (op n)) f :
      (stdSimplex.obj m).obj (op n))

Tactic:
yonedaEquiv.symm.injective rfl

Premises used: SSet.yonedaEquiv, Equiv.injective, Equiv.symm, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
S : SSet
n : SimplexCategory
x : S.obj (op n)
α : (stdSimplex.obj n).obj (op n)
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S.obj (op n)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : S.obj (op n)) → stdSimplex.obj n ⟶ S) x) (op n)) :
          (a : (fun (X : Type u_1) ↦ X) ((stdSimplex.obj n).obj (op n))) → (fun (X : Type u_1) ↦ X) (S.obj (op n)))
        α :
      (fun (X : Type u_1) ↦ X) (S.obj (op n)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (S.map
              (Quiver.Hom.op
                (((stdSimplex.objEquiv : (stdSimplex.obj n).obj (op n) ≃ (unop (op n) ⟶ n)) :
                    (a : (stdSimplex.obj n).obj (op n)) → unop (op n) ⟶ n)
                  α))) :
          (a : (fun (X : Type u_1) ↦ X) (S.obj (op n))) → (fun (X : Type u_1) ↦ X) (S.obj (op (unop (op n)))))
        x :
      (fun (X : Type u_1) ↦ X) (S.obj (op (unop (op n)))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
⊢ Eq.{u_1 + 1} (α := stdSimplex.obj n ⟶ stdSimplex.obj n)
    ((Equiv.symm yonedaEquiv : (a : (stdSimplex.obj n).obj (op n)) → stdSimplex.obj n ⟶ stdSimplex.obj n)
        ((Equiv.symm stdSimplex.objEquiv : (a : n ⟶ n) → (stdSimplex.obj n).obj (op n)) (𝟙 n) :
          (stdSimplex.obj n).obj (op n)) :
      stdSimplex.obj n ⟶ stdSimplex.obj n)
    (𝟙 (stdSimplex.obj n) : stdSimplex.obj n ⟶ stdSimplex.obj n)

Tactic:
yonedaEquiv.symm_apply_eq.mpr rfl

Premises used: SSet.yonedaEquiv, Iff.mpr, Equiv.symm_apply_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
n : SimplexCategory
x : X.obj (op n)
m : SimplexCategoryᵒᵖ
f : unop m ⟶ n
⊢ Eq (α := X.obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X.obj (op n)) → stdSimplex.obj n ⟶ X) x) m) :
          (a : (stdSimplex.obj n).obj m) → X.obj m)
        ((Equiv.symm stdSimplex.objEquiv : (a : unop m ⟶ n) → (stdSimplex.obj n).obj m) f : (stdSimplex.obj n).obj m) :
      X.obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X.obj (op n)) → X.obj m) x : X.obj m)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
⊢ Eq (α := ⦋n⦌ ⟶ ⦋n⦌)
    (((objEquiv : Δ[n] _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋n⦌) → ⦋n⦌ ⟶ ⦋n⦌)
        ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n]) → Δ[n] _⦋n⦌) (𝟙 Δ[n])) :
      ⦋n⦌ ⟶ ⦋n⦌)
    (𝟙 ⦋n⦌ : ⦋n⦌ ⟶ ⦋n⦌)

Tactic:
rfl

Premises used: OrderHom.id, SimplexCategory.Hom.id, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
n : SimplexCategory
x : X.obj (op n)
m : SimplexCategoryᵒᵖ
y : (stdSimplex.obj n).obj m
⊢ Eq (α := X.obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op
                (((objEquiv : (stdSimplex.obj n).obj m ≃ (unop m ⟶ n)) : (a : (stdSimplex.obj n).obj m) → unop m ⟶ n)
                  y))) :
          (a : X.obj (op n)) → X.obj m)
        x :
      X.obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X.obj (op n)) → stdSimplex.obj n ⟶ X) x) m) :
          (a : (stdSimplex.obj n).obj m) → X.obj m)
        y :
      X.obj m)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
k : Fin (n + 1)
m : SimplexCategoryᵒᵖ
⊢ Hom.toOrderHom (ULift.down.{u_1, 0} (const n k m)) =
    (OrderHom.const (Fin ((unop m).len + 1)) : (a : Fin (n + 1)) → Fin ((unop m).len + 1) →o Fin (n + 1)) k

Tactic:
rfl

Premises used: SimplexCategory.Hom.toOrderHom, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : Δ[n] _⦋0⦌
h :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
    Eq (α := Fin (n + 1))
      (((fun (i : Fin (n + 1)) ↦ (const n i (op ⦋0⦌) : Δ[n] _⦋0⦌))
              ((fun (x : Δ[n] _⦋0⦌) ↦ ((x : (a : Fin (0 + 1)) → Fin (n + 1)) 0 : Fin (n + 1))) x) :
            (a : Fin (0 + 1)) → Fin (n + 1))
          i :
        Fin (n + 1))
      ((x : (a : Fin (0 + 1)) → Fin (n + 1)) i : Fin (n + 1))
⊢ (fun (i : Fin (n + 1)) ↦ (const n i (op ⦋0⦌) : Δ[n] _⦋0⦌))
      ((fun (x : Δ[n] _⦋0⦌) ↦ ((x : (a : Fin (0 + 1)) → Fin (n + 1)) 0 : Fin (n + 1))) x) =
    x

Tactic:
ext i : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : Δ[n] _⦋0⦌
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
h :
  Eq (α := Fin (n + 1))
    (((fun (i : Fin (n + 1)) ↦ (const n i (op ⦋0⦌) : Δ[n] _⦋0⦌))
          ((fun (x : Δ[n] _⦋0⦌) ↦ ((x : (a : Fin (0 + 1)) → Fin (n + 1)) 0 : Fin (n + 1))) x) :
        (a : Fin (0 + 1)) → Fin (n + 1))
      ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((x : (a : Fin (0 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
⊢ Eq (α := Fin (n + 1))
    (((fun (i : Fin (n + 1)) ↦ (const n i (op ⦋0⦌) : Δ[n] _⦋0⦌))
            ((fun (x : Δ[n] _⦋0⦌) ↦ ((x : (a : Fin (0 + 1)) → Fin (n + 1)) 0 : Fin (n + 1))) x) :
          (a : Fin (0 + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
    ((x : (a : Fin (0 + 1)) → Fin (n + 1)) i : Fin (n + 1))

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : Δ[n] _⦋0⦌
⊢ Eq (α := Fin (n + 1))
    (((fun (i : Fin (n + 1)) ↦ (const n i (op ⦋0⦌) : Δ[n] _⦋0⦌))
          ((fun (x : Δ[n] _⦋0⦌) ↦ ((x : (a : Fin (0 + 1)) → Fin (n + 1)) 0 : Fin (n + 1))) x) :
        (a : Fin (0 + 1)) → Fin (n + 1))
      ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((x : (a : Fin (0 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
⊢ Eq (α := Δ[0] ⟶ Δ[HAdd.hAdd (α := ℕ) 0 1]) (stdSimplex.δ 1)
    (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1 + 1)) → Δ[0 + 1] _⦋0⦌) 0))

Tactic:
decide