awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₂ : Fin (⦋n + 1⦌.len + 1)
hi : 0 ≤ i₂
⊢ LE.le (α := Fin (Δ.len + 1))
    (shiftFun (n := ⦋n + 1⦌.len) (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) 0)
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)

Tactic:
simp only [shiftFun_zero, Fin.zero_le]

Premises used: Fin.zero_le, SSet.Augmented.StandardSimplex.shiftFun_zero
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ : Fin (⦋n + 1⦌.len + 1)
h₁ : ¬i₁ = 0
hi : i₁ ≤ 0
⊢ False

Tactic:
h₁ (le_antisymm hi (Fin.zero_le _))

Premises used: Fin.zero_le, le_antisymm
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ : Fin (⦋n + 1⦌.len + 1)
h₁ : ¬i₁ = 0
hi : i₁ ≤ 0
⊢ False

Tactic:
exact h₁ (le_antisymm hi (Fin.zero_le _))

Premises used: Fin.zero_le, le_antisymm
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
⊢ i₂ ≠ 0

Tactic:
have h₂ : i₂ ≠ 0 := by
            rintro rfl
            exact h₁ (le_antisymm hi (Fin.zero_le _))
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ ≠ 0
neg :
  ∀ (j₁ : Fin ⦋n + 1⦌.len) (hj₁ : i₁ = j₁.succ),
    LE.le (α := Fin (Δ.len + 1))
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₁)
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)
⊢ LE.le (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₁)
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)

Tactic:
obtain ⟨j₁, hj₁⟩ := Fin.eq_succ_of_ne_zero h₁

Premises used: Fin.eq_succ_of_ne_zero
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ ≠ 0
j₁ : Fin ⦋n + 1⦌.len
hj₁ : i₁ = j₁.succ
neg :
  ∀ (j₂ : Fin ⦋n + 1⦌.len) (hj₂ : i₂ = j₂.succ),
    LE.le (α := Fin (Δ.len + 1))
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₁)
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)
⊢ LE.le (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₁)
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)

Tactic:
obtain ⟨j₂, hj₂⟩ := Fin.eq_succ_of_ne_zero h₂

Premises used: Fin.eq_succ_of_ne_zero
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ ≠ 0
j₁ : Fin ⦋n + 1⦌.len
hj₁ : i₁ = j₁.succ
j₂ : Fin ⦋n + 1⦌.len
hj₂ : i₂ = j₂.succ
neg :
  ∀ (h₁ : ¬j₁.succ = 0) (h₂ : j₂.succ ≠ 0) (hi : j₁.succ ≤ j₂.succ),
    LE.le (α := Fin (Δ.len + 1))
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) j₁.succ)
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) j₂.succ)
⊢ LE.le (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₁)
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)

Tactic:
substs hj₁ hj₂
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
j₁ j₂ : Fin ⦋n + 1⦌.len
h₁ : ¬j₁.succ = 0
h₂ : j₂.succ ≠ 0
hi : j₁.succ ≤ j₂.succ
⊢ LE.le (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) j₁.succ)
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) j₂.succ)

Tactic:
simpa only [shiftFun_succ] using f.toOrderHom.monotone (Fin.succ_le_succ_iff.mp hi)

Premises used: OrderHom.monotone, Fin.succ_le_succ_iff, SSet.Augmented.StandardSimplex.shiftFun_succ, SimplexCategory.Hom.toOrderHom, Iff.mp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
⊢ (↾fun (x : ⊤_ Type u_1) ↦ objMk ((OrderHom.const (Fin 1) : (a : Fin (Δ.len + 1)) → Fin 1 →o Fin (Δ.len + 1)) 0)) ≫
      Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) =
    𝟙 (⊤_ Type u_1)

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
h :
  ∀ (x : SSet.stdSimplex.obj Δ _⦋0⦌),
    Eq (α := SSet.stdSimplex.obj Δ _⦋0⦌)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (f : SSet.stdSimplex.obj Δ _⦋0⦌) ↦
              (Equiv.symm objEquiv : (a : ⦋1⦌ ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋1⦌)
                (SimplexCategory.Hom.mk
                  {
                    toFun :=
                      shiftFun
                        (⇑(SimplexCategory.Hom.toOrderHom
                              (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                                  (a : SSet.stdSimplex.obj Δ _⦋0⦌) → ⦋0⦌ ⟶ Δ)
                                f)) :
                          (a : Fin 1) → Fin (Δ.len + 1)),
                    monotone' := ⋯ : Fin 2 →o Fin (Δ.len + 1) })) ≫
            SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := ⊤_ Type u_1) (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌))
            (↾fun (x : ⊤_ Type u_1) ↦
              objMk ((OrderHom.const (Fin 1) : (a : Fin (Δ.len + 1)) → Fin 1 →o Fin (Δ.len + 1)) 0))))
        x)
⊢ Eq (α := SSet.stdSimplex.obj Δ _⦋0⦌ ⟶ SSet.stdSimplex.obj Δ _⦋0⦌)
    ((↾fun (f : SSet.stdSimplex.obj Δ _⦋0⦌) ↦
        (Equiv.symm objEquiv : (a : ⦋1⦌ ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋1⦌)
          (SimplexCategory.Hom.mk
            {
              toFun :=
                shiftFun
                  (⇑(SimplexCategory.Hom.toOrderHom
                        (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                            (a : SSet.stdSimplex.obj Δ _⦋0⦌) → ⦋0⦌ ⟶ Δ)
                          f)) :
                    (a : Fin 1) → Fin (Δ.len + 1)),
              monotone' := ⋯ })) ≫
      SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1)
    (CategoryStruct.comp (Y := ⊤_ Type u_1) (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌))
      (↾fun (x : ⊤_ Type u_1) ↦ objMk ((OrderHom.const (Fin 1) : (a : Fin (Δ.len + 1)) → Fin 1 →o Fin (Δ.len + 1)) 0)))

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
h :
  Eq (α := unop (op ⦋0⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋0⦌) → unop (op ⦋0⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (f : SSet.stdSimplex.obj Δ _⦋0⦌) ↦
                (Equiv.symm objEquiv : (a : ⦋1⦌ ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋1⦌)
                  (SimplexCategory.Hom.mk
                    {
                      toFun :=
                        shiftFun
                          (⇑(SimplexCategory.Hom.toOrderHom
                                (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                                    (a : SSet.stdSimplex.obj Δ _⦋0⦌) → ⦋0⦌ ⟶ Δ)
                                  f)) :
                            (a : Fin 1) → Fin (Δ.len + 1)),
                      monotone' := ⋯ : Fin 2 →o Fin (Δ.len + 1) })) ≫
              SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1))
          x) :
      unop (op ⦋0⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋0⦌) → unop (op ⦋0⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ⊤_ Type u_1) (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌))
              (↾fun (x : ⊤_ Type u_1) ↦
                objMk ((OrderHom.const (Fin 1) : (a : Fin (Δ.len + 1)) → Fin 1 →o Fin (Δ.len + 1)) 0))))
          x) :
      unop (op ⦋0⦌) ⟶ Δ)
⊢ Eq (α := SSet.stdSimplex.obj Δ _⦋0⦌)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (f : SSet.stdSimplex.obj Δ _⦋0⦌) ↦
            (Equiv.symm objEquiv : (a : ⦋1⦌ ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋1⦌)
              (SimplexCategory.Hom.mk
                {
                  toFun :=
                    shiftFun
                      (⇑(SimplexCategory.Hom.toOrderHom
                            (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                                (a : SSet.stdSimplex.obj Δ _⦋0⦌) → ⦋0⦌ ⟶ Δ)
                              f)) :
                        (a : Fin 1) → Fin (Δ.len + 1)),
                  monotone' := ⋯ : Fin 2 →o Fin (Δ.len + 1) })) ≫
          SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := ⊤_ Type u_1) (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌))
          (↾fun (x : ⊤_ Type u_1) ↦
            objMk ((OrderHom.const (Fin 1) : (a : Fin (Δ.len + 1)) → Fin 1 →o Fin (Δ.len + 1)) 0))))
      x)

Tactic:
apply objEquiv.injective

Premises used: Equiv.injective, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
⊢ (↑((SimplexCategory.Hom.toOrderHom
              (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                  (a : SSet.stdSimplex.obj Δ _⦋0⦌) → unop (op ⦋0⦌) ⟶ Δ)
                (TypeCat.Fun.toFun
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((↾fun (f : SSet.stdSimplex.obj Δ _⦋0⦌) ↦
                        (Equiv.symm objEquiv : (a : ⦋1⦌ ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋1⦌)
                          (SimplexCategory.Hom.mk
                            {
                              toFun :=
                                shiftFun
                                  (⇑(SimplexCategory.Hom.toOrderHom
                                        (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                                            (a : SSet.stdSimplex.obj Δ _⦋0⦌) → ⦋0⦌ ⟶ Δ)
                                          f)) :
                                    (a : Fin 1) → Fin (Δ.len + 1)),
                              monotone' := ⋯ : Fin 2 →o Fin (Δ.len + 1) })) ≫
                      SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1))
                  x)) :
            (a : Fin ((unop (op ⦋0⦌)).len + 1)) → Fin (Δ.len + 1))
          ((fun (i : Fin ((unop (op ⦋0⦌)).len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin ((unop (op ⦋0⦌)).len + 1)))) :
      ℕ) =
    (↑((SimplexCategory.Hom.toOrderHom
              (((objEquiv : SSet.stdSimplex.obj Δ _⦋0⦌ ≃ (unop (op ⦋0⦌) ⟶ Δ)) :
                  (a : SSet.stdSimplex.obj Δ _⦋0⦌) → unop (op ⦋0⦌) ⟶ Δ)
                (TypeCat.Fun.toFun
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (CategoryStruct.comp (Y := ⊤_ Type u_1) (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌))
                      (↾fun (x : ⊤_ Type u_1) ↦
                        objMk ((OrderHom.const (Fin 1) : (a : Fin (Δ.len + 1)) → Fin 1 →o Fin (Δ.len + 1)) 0))))
                  x)) :
            (a : Fin ((unop (op ⦋0⦌)).len + 1)) → Fin (Δ.len + 1))
          ((fun (i : Fin ((unop (op ⦋0⦌)).len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
h :
  ∀ (φ : (stdSimplex.obj Δ).left _⦋n⦌),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
              (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
                (shift
                  (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                      (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                    f))) ≫
            (stdSimplex.obj Δ).left.δ 0))
        φ =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((stdSimplex.obj Δ).left _⦋n⦌))).toFun φ
⊢ (↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
        (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
          (shift
            (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
              f))) ≫
      (stdSimplex.obj Δ).left.δ 0 =
    𝟙 ((stdSimplex.obj Δ).left _⦋n⦌)

Tactic:
ext φ
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
φ : (stdSimplex.obj Δ).left _⦋n⦌
h :
  Eq (α := unop (op ⦋n⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
                (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
                  (shift
                    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                        (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                      f))) ≫
              (stdSimplex.obj Δ).left.δ 0))
          φ) :
      unop (op ⦋n⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((stdSimplex.obj Δ).left _⦋n⦌))).toFun φ) :
      unop (op ⦋n⦌) ⟶ Δ)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
            (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
              (shift
                (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                    (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                  f))) ≫
          (stdSimplex.obj Δ).left.δ 0))
      φ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((stdSimplex.obj Δ).left _⦋n⦌))).toFun φ

Tactic:
apply objEquiv.injective

Premises used: Equiv.injective, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
φ : (stdSimplex.obj Δ).left _⦋n⦌
h :
  Eq (α := Fin ((unop (op ⦋n⦌)).len + 1) →o Fin (Δ.len + 1))
    (SimplexCategory.Hom.toOrderHom
      (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
                (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
                  (shift
                    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                        (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                      f))) ≫
              (stdSimplex.obj Δ).left.δ 0))
          φ)))
    (SimplexCategory.Hom.toOrderHom
      (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((stdSimplex.obj Δ).left _⦋n⦌))).toFun φ)))
⊢ Eq (α := unop (op ⦋n⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
                (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
                  (shift
                    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                        (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                      f))) ≫
              (stdSimplex.obj Δ).left.δ 0))
          φ) :
      unop (op ⦋n⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((stdSimplex.obj Δ).left _⦋n⦌))).toFun φ) :
      unop (op ⦋n⦌) ⟶ Δ)

Tactic:
apply SimplexCategory.Hom.ext

Premises used: SimplexCategory.Hom.ext
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
φ : (stdSimplex.obj Δ).left _⦋n⦌
i : Fin ((unop (op ⦋n⦌)).len + 1)
⊢ Eq (α := Fin (Δ.len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
              (TypeCat.Fun.toFun
                (ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
                      (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
                        (shift
                          (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                              (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                            f))) ≫
                    (stdSimplex.obj Δ).left.δ 0))
                φ)) :
          (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (Δ.len + 1))
        i :
      Fin (Δ.len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((stdSimplex.obj Δ).left _⦋n⦌))).toFun φ)) :
          (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (Δ.len + 1))
        i :
      Fin (Δ.len + 1))

Tactic:
dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.stdSimplex,
      objEquiv, Equiv.ulift, uliftFunctor]

Premises used: SimplexCategory.δ, Equiv.ulift, SSet.stdSimplex, SSet.uliftFunctor, CategoryTheory.SimplicialObject.δ, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
h :
  ∀ (φ : (stdSimplex.obj Δ).left _⦋n + 1⦌),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (f : (stdSimplex.obj Δ).left _⦋n + 1⦌) ↦
              (Equiv.symm objEquiv : (a : unop (op ⦋n + 1 + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌)
                (shift
                  (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ Δ)) :
                      (a : SSet.stdSimplex.obj Δ _⦋n + 1⦌) → unop (op ⦋n + 1⦌) ⟶ Δ)
                    f))) ≫
            (stdSimplex.obj Δ).left.δ i.succ))
        φ =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((stdSimplex.obj Δ).left.δ i ≫
            ↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
              (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
                (shift
                  (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                      (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                    f))))
        φ
⊢ (↾fun (f : (stdSimplex.obj Δ).left _⦋n + 1⦌) ↦
        (Equiv.symm objEquiv : (a : unop (op ⦋n + 1 + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌)
          (shift
            (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ Δ)) :
                (a : SSet.stdSimplex.obj Δ _⦋n + 1⦌) → unop (op ⦋n + 1⦌) ⟶ Δ)
              f))) ≫
      (stdSimplex.obj Δ).left.δ i.succ =
    (stdSimplex.obj Δ).left.δ i ≫
      ↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
        (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
          (shift
            (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
              f))

Tactic:
ext φ
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
h :
  Eq (α := unop (op ⦋n + 1⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n + 1⦌) → unop (op ⦋n + 1⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (f : (stdSimplex.obj Δ).left _⦋n + 1⦌) ↦
                (Equiv.symm objEquiv : (a : unop (op ⦋n + 1 + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌)
                  (shift
                    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ Δ)) :
                        (a : SSet.stdSimplex.obj Δ _⦋n + 1⦌) → unop (op ⦋n + 1⦌) ⟶ Δ)
                      f))) ≫
              (stdSimplex.obj Δ).left.δ i.succ))
          φ) :
      unop (op ⦋n + 1⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n + 1⦌) → unop (op ⦋n + 1⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((stdSimplex.obj Δ).left.δ i ≫
              ↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
                (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
                  (shift
                    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                        (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                      f))))
          φ) :
      unop (op ⦋n + 1⦌) ⟶ Δ)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (f : (stdSimplex.obj Δ).left _⦋n + 1⦌) ↦
            (Equiv.symm objEquiv : (a : unop (op ⦋n + 1 + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌)
              (shift
                (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ Δ)) :
                    (a : SSet.stdSimplex.obj Δ _⦋n + 1⦌) → unop (op ⦋n + 1⦌) ⟶ Δ)
                  f))) ≫
          (stdSimplex.obj Δ).left.δ i.succ))
      φ =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((stdSimplex.obj Δ).left.δ i ≫
          ↾fun (f : (stdSimplex.obj Δ).left _⦋n⦌) ↦
            (Equiv.symm objEquiv : (a : unop (op ⦋n + 1⦌) ⟶ Δ) → SSet.stdSimplex.obj Δ _⦋n + 1⦌)
              (shift
                (((objEquiv : SSet.stdSimplex.obj Δ _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ Δ)) :
                    (a : SSet.stdSimplex.obj Δ _⦋n⦌) → unop (op ⦋n⦌) ⟶ Δ)
                  f))))
      φ

Tactic:
apply objEquiv.injective

Premises used: Equiv.injective, SSet.stdSimplex.objEquiv