awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ 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₂)
have pos : ∀ (h₁ : i₁ = 0),
  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: by_cases h₁ : i₁ = 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
pos :
  ∀ (h₁ : i₁ = 0),
    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₂)
have neg : ∀ (h₁ : ¬i₁ = 0),
  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: by_cases h₁ : i₁ = 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : i₁ = 0
⊢ 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₂)
have pos : ∀ (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: subst h₁
Cleared hypotheses: i₁, hi, h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (hypothesis)
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
⊢ 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₂)
have h₂ : i₂ ≠ 0
Tactic: have h₂ : i₂ ≠ 0 := by
            rintro rfl
            exact h₁ (le_antisymm hi (Fin.zero_le _))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ ≠ 0
⊢ 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₂)
have 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₂)
Tactic: obtain ⟨j₁, hj₁⟩ := Fin.eq_succ_of_ne_zero h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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
⊢ 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₂)
have 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₂)
Tactic: obtain ⟨j₂, hj₂⟩ := Fin.eq_succ_of_ne_zero h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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
⊢ 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₂)
have 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)
Tactic: substs hj₁ hj₂
Cleared hypotheses: i₁, i₂, hi, h₁, h₂, hj₁, hj₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
⊢ 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)))
have 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' := sorry : 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: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
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)
have 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' := sorry : 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⦌) ⟶ Δ)
Tactic: apply objEquiv.injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
⊢ (↾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⦌)
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.δ 0))
      φ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((stdSimplex.obj Δ).left _⦋n⦌))).toFun φ
Tactic: ext φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
φ : (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 φ
have 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⦌) ⟶ Δ)
Tactic: apply objEquiv.injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ 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⦌) ⟶ Δ)
have 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 φ)))
Tactic: apply SimplexCategory.Hom.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
⊢ (↾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))
have 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))))
      φ
Tactic: ext φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (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))))
      φ
have 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⦌) ⟶ Δ)
Tactic: apply objEquiv.injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
⊢ 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⦌) ⟶ Δ)
have 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))))
        φ)))
Tactic: apply SimplexCategory.Hom.ext