awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
j : Fin ((unop (op ⦋n + 1⦌)).len + 1)
⊢ 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))
have 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)
Tactic: dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.stdSimplex,
      objEquiv, Equiv.ulift, uliftFunctor]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
j : Fin ((unop (op ⦋n + 1⦌)).len + 1)
⊢ 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)
have 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)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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)
⊢ 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)
have 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)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
⊢ (↾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))
have 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))))
      φ
Tactic: ext φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (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))))
      φ
have 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⦌) ⟶ Δ)
Tactic: apply objEquiv.injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ 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⦌) ⟶ Δ)
have h : Eq (α := Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1) →o 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))
        φ)))
  (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))))
        φ)))
Tactic: apply SimplexCategory.Hom.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
j : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)
⊢ 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))
have 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)
Tactic: dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.stdSimplex, objEquiv, Equiv.ulift,
      uliftFunctor, Function.comp_def]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
j : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)
⊢ 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)
have 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)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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)
⊢ 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)
have 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)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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)
⊢ 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)
have 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)
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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)
⊢ 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)
have 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)
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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
⊢ Eq (α := f.augmentedCechNerve.left _⦋0⦌ ⟶ f.augmentedCechNerve.left _⦋0⦌)
    (CategoryStruct.comp (Y := f.augmentedCechNerve.left _⦋1⦌)
        (ExtraDegeneracy.s f S 0 : f.cechNerve _⦋0⦌ ⟶ f.cechNerve _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
        (f.augmentedCechNerve.left.δ 1) :
      f.augmentedCechNerve.left _⦋0⦌ ⟶ f.augmentedCechNerve.left _⦋0⦌)
    (f.augmentedCechNerve.hom.app (op ⦋0⦌) ≫
        S.section_ ≫ WidePullback.lift f.hom (fun (x : Fin ((unop (op ⦋0⦌)).len + 1)) ↦ 𝟙 f.left) ⋯ :
      f.augmentedCechNerve.left _⦋0⦌ ⟶ f.augmentedCechNerve.left _⦋0⦌)
have dsimp : Eq (α :=
  (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶
    widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
  (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 2) ↦ f.left) fun (x : Fin 2) ↦ f.hom)
      (ExtraDegeneracy.s f S 0 : f.cechNerve _⦋0⦌ ⟶ f.cechNerve _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (WidePullback.lift (WidePullback.base fun (x : Fin 2) ↦ f.hom)
        (fun (i : Fin 1) ↦ WidePullback.π (fun (x : Fin 2) ↦ f.hom) (Fin.succAbove 1 i)) sorry) :
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
  ((WidePullback.base fun (x : Fin 1) ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun (x : Fin 1) ↦ 𝟙 f.left) sorry :
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
Tactic: dsimp [SimplicialObject.δ, SimplexCategory.δ]