awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
h :
  Eq (α := Fin ((unop (op ⦋n + 1⦌)).len + 1) →o Fin (Δ.len + 1))
    (SimplexCategory.Hom.toOrderHom
      (((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))
          φ)))
    (SimplexCategory.Hom.toOrderHom
      (((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))))
          φ)))
⊢ 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⦌) ⟶ Δ)

Tactic:
apply SimplexCategory.Hom.ext

Premises used: SimplexCategory.Hom.ext
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
j : Fin ((unop (op ⦋n + 1⦌)).len + 1)
h :
  Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1)) (i.succ.succAbove j))
    (shiftFun
      (Function.comp (β := Fin (n + 1 + 1))
        (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1))
        (⇑i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)))
      j)
⊢ Eq (α := Fin (Δ.len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (((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))
                φ)) :
          (a : Fin ((unop (op ⦋n + 1⦌)).len + 1)) → Fin (Δ.len + 1))
        j :
      Fin (Δ.len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (((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))))
                φ)) :
          (a : Fin ((unop (op ⦋n + 1⦌)).len + 1)) → Fin (Δ.len + 1))
        j :
      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)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
j : Fin ((unop (op ⦋n + 1⦌)).len + 1)
h :
  Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1)) (i.succ.succAbove 0))
    (shiftFun (n := n + 1)
      (Function.comp (β := Fin (n + 1 + 1))
        (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1))
        (⇑i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)))
      0)
h₁ :
  ∀ (i_1 : Fin (unop (op ⦋n + 1⦌)).len),
    Eq (α := Fin (Δ.len + 1))
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1))
        (i.succ.succAbove i_1.succ))
      (shiftFun
        (Function.comp (β := Fin (n + 1 + 1))
          (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1))
          (⇑i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)))
        i_1.succ)
⊢ Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1)) (i.succ.succAbove j))
    (shiftFun
      (Function.comp (β := Fin (n + 1 + 1))
        (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1))
        (⇑i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)))
      j)

Tactic:
cases j using Fin.cases
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
⊢ Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1)) (i.succ.succAbove 0))
    (shiftFun (n := n + 1)
      (Function.comp (β := Fin (n + 1 + 1))
        (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1))
        (⇑i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)))
      0)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
i_1 : Fin (unop (op ⦋n + 1⦌)).len
⊢ Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1))
      (i.succ.succAbove i_1.succ))
    (shiftFun
      (Function.comp (β := Fin (n + 1 + 1))
        (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1 + 1)) → Fin (Δ.len + 1))
        (⇑i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)))
      i_1.succ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
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.σ i.succ))
        φ =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((stdSimplex.obj Δ).left.σ i ≫
            ↾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))))
        φ
⊢ (↾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.σ i.succ =
    (stdSimplex.obj Δ).left.σ i ≫
      ↾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))

Tactic:
ext φ
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
h :
  Eq (α := unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌ ≃ (unop (op ⦋n + 1 + 1⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌) → unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
        (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.σ i.succ))
          φ) :
      unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
    (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌ ≃ (unop (op ⦋n + 1 + 1⦌) ⟶ Δ)) :
          (a : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌) → unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((stdSimplex.obj Δ).left.σ i ≫
              ↾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))))
          φ) :
      unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
⊢ 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.σ i.succ))
      φ =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((stdSimplex.obj Δ).left.σ i ≫
          ↾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))))
      φ

Tactic:
apply objEquiv.injective

Premises used: Equiv.injective, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
j : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)
h :
  Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.succ.predAbove j))
    (shiftFun
      (fun (x : Fin (n + 1 + 1)) ↦
        (SimplexCategory.Hom.toOrderHom φ.down : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.predAbove x))
      j)
⊢ Eq (α := Fin (Δ.len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌ ≃ (unop (op ⦋n + 1 + 1⦌) ⟶ Δ)) :
                (a : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌) → unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
              (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.σ i.succ))
                φ)) :
          (a : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)) → Fin (Δ.len + 1))
        j :
      Fin (Δ.len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (((objEquiv : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌ ≃ (unop (op ⦋n + 1 + 1⦌) ⟶ Δ)) :
                (a : SSet.stdSimplex.obj Δ _⦋n + 1 + 1⦌) → unop (op ⦋n + 1 + 1⦌) ⟶ Δ)
              (TypeCat.Fun.toFun
                (ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((stdSimplex.obj Δ).left.σ i ≫
                    ↾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))))
                φ)) :
          (a : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)) → Fin (Δ.len + 1))
        j :
      Fin (Δ.len + 1))

Tactic:
dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.stdSimplex, objEquiv, Equiv.ulift,
      uliftFunctor, Function.comp_def]

Premises used: Equiv.ulift, SimplexCategory.σ, SSet.stdSimplex, SSet.uliftFunctor, Function.comp_def, SSet.stdSimplex.objEquiv, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
j : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)
h :
  Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.succ.predAbove 0))
    (shiftFun (n := n + 1 + 1)
      (fun (x : Fin (n + 1 + 1)) ↦
        (SimplexCategory.Hom.toOrderHom φ.down : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.predAbove x))
      0)
h₁ :
  ∀ (i_1 : Fin (unop (op ⦋n + 1 + 1⦌)).len),
    Eq (α := Fin (Δ.len + 1))
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1)) → Fin (Δ.len + 1))
        (i.succ.predAbove i_1.succ))
      (shiftFun
        (fun (x : Fin (n + 1 + 1)) ↦
          (SimplexCategory.Hom.toOrderHom φ.down : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.predAbove x))
        i_1.succ)
⊢ Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.succ.predAbove j))
    (shiftFun
      (fun (x : Fin (n + 1 + 1)) ↦
        (SimplexCategory.Hom.toOrderHom φ.down : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.predAbove x))
      j)

Tactic:
cases j using Fin.cases
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.succ.predAbove 0))
    (shiftFun (n := n + 1 + 1)
      (fun (x : Fin (n + 1 + 1)) ↦
        (SimplexCategory.Hom.toOrderHom φ.down : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.predAbove x))
      0)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
i_1 : Fin (unop (op ⦋n + 1 + 1⦌)).len
⊢ Eq (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) : (a : Fin (n + 1)) → Fin (Δ.len + 1))
      (i.succ.predAbove i_1.succ))
    (shiftFun
      (fun (x : Fin (n + 1 + 1)) ↦
        (SimplexCategory.Hom.toOrderHom φ.down : (a : Fin (n + 1)) → Fin (Δ.len + 1)) (i.predAbove x))
      i_1.succ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
Δ : SimplexCategory
⊢ Nonempty.{u_1 + 1} (ExtraDegeneracy (stdSimplex.obj Δ))

Tactic:
⟨StandardSimplex.extraDegeneracy Δ⟩

Premises used: Nonempty.intro, SSet.Augmented.StandardSimplex.extraDegeneracy
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f : Arrow.{v_1, u_1} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin ((unop (op ⦋n + 1⦌)).len + 1)
zero :
  Eq (α := f.cechNerve _⦋n⦌ ⟶ f.right)
    ((fun (i : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦
          (Fin.cases.{v_1 + 1} (motive := fun (x : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦ f.cechNerve _⦋n⦌ ⟶ f.left)
              ((WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ≫ S.section_ :
                f.cechNerve _⦋n⦌ ⟶ f.left)
              (WidePullback.π fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom :
                (j : Fin (unop (op ⦋n + 1⦌)).len) →
                  (widePullback.{0, v_1, u_1} f.right (fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.left)
                      fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ⟶
                    f.left)
              i :
            f.cechNerve _⦋n⦌ ⟶ f.left))
        0 ≫
      f.hom)
    (WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom)
succ :
  ∀ (i : Fin (unop (op ⦋n + 1⦌)).len),
    Eq (α := f.cechNerve _⦋n⦌ ⟶ f.right)
      ((fun (i : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦
            (Fin.cases.{v_1 + 1} (motive := fun (x : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦ f.cechNerve _⦋n⦌ ⟶ f.left)
                ((WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ≫ S.section_ :
                  f.cechNerve _⦋n⦌ ⟶ f.left)
                (WidePullback.π fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom :
                  (j : Fin (unop (op ⦋n + 1⦌)).len) →
                    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.left)
                        fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ⟶
                      f.left)
                i :
              f.cechNerve _⦋n⦌ ⟶ f.left))
          i.succ ≫
        f.hom)
      (WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom)
⊢ Eq (α := f.cechNerve _⦋n⦌ ⟶ f.right)
    ((fun (i : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦
          (Fin.cases.{v_1 + 1} (motive := fun (x : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦ f.cechNerve _⦋n⦌ ⟶ f.left)
              ((WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ≫ S.section_ :
                f.cechNerve _⦋n⦌ ⟶ f.left)
              (WidePullback.π fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom :
                (j : Fin (unop (op ⦋n + 1⦌)).len) →
                  (widePullback.{0, v_1, u_1} f.right (fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.left)
                      fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ⟶
                    f.left)
              i :
            f.cechNerve _⦋n⦌ ⟶ f.left))
        i ≫
      f.hom)
    (WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom)

Tactic:
cases i using Fin.cases
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f : Arrow.{v_1, u_1} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
S : SplitEpi f.hom
n : ℕ
⊢ Eq (α := f.cechNerve _⦋n⦌ ⟶ f.right)
    ((fun (i : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦
          (Fin.cases.{v_1 + 1} (motive := fun (x : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦ f.cechNerve _⦋n⦌ ⟶ f.left)
              ((WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ≫ S.section_ :
                f.cechNerve _⦋n⦌ ⟶ f.left)
              (WidePullback.π fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom :
                (j : Fin (unop (op ⦋n + 1⦌)).len) →
                  (widePullback.{0, v_1, u_1} f.right (fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.left)
                      fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ⟶
                    f.left)
              i :
            f.cechNerve _⦋n⦌ ⟶ f.left))
        0 ≫
      f.hom)
    (WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f : Arrow.{v_1, u_1} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (unop (op ⦋n + 1⦌)).len
⊢ Eq (α := f.cechNerve _⦋n⦌ ⟶ f.right)
    ((fun (i : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦
          (Fin.cases.{v_1 + 1} (motive := fun (x : Fin ((unop (op ⦋n + 1⦌)).len + 1)) ↦ f.cechNerve _⦋n⦌ ⟶ f.left)
              ((WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ≫ S.section_ :
                f.cechNerve _⦋n⦌ ⟶ f.left)
              (WidePullback.π fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom :
                (j : Fin (unop (op ⦋n + 1⦌)).len) →
                  (widePullback.{0, v_1, u_1} f.right (fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.left)
                      fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom) ⟶
                    f.left)
              i :
            f.cechNerve _⦋n⦌ ⟶ f.left))
        i.succ ≫
      f.hom)
    (WidePullback.base fun (x : Fin ((unop (op ⦋n⦌)).len + 1)) ↦ f.hom)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f : Arrow.{v_1, u_1} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
S : SplitEpi f.hom
n : ℕ
⊢ Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
        (s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) (WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) 0) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.left)
    ((WidePullback.base fun (x : Fin (n + 1)) ↦ f.hom) ≫ S.section_ :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.left)

Tactic:
simp [ExtraDegeneracy.s]

Premises used: CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s