awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (n + 1)
⊢ 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) i.succ) :
      (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.π (fun (x : Fin (n + 1)) ↦ f.hom) i :
      (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
-- 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.right)
    (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.base fun (x : Fin (n + 1 + 1)) ↦ f.hom) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.right)
    (WidePullback.base fun (x : Fin (n + 1)) ↦ f.hom :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.right)

Tactic:
WidePullback.lift_base ..

Premises used: CategoryTheory.Limits.WidePullback.lift_base, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s, CategoryTheory.Limits.limit
-- 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
⊢ ∀ (j : Fin ((unop (op ⦋0⦌)).len + 1)),
    (fun (x : Fin ((unop (op ⦋0⦌)).len + 1)) ↦ (𝟙 f.left : f.left ⟶ f.left)) j ≫ f.hom = 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
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)) ⋯) :
      (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) ⋯ :
      (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)
⊢ 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⦌)

Tactic:
dsimp [SimplicialObject.δ, SimplexCategory.δ]

Premises used: SimplexCategory.δ, CategoryTheory.SimplicialObject.δ
-- 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
j : Fin 1
a :
  Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := 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)) ⋯))
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := 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) ⋯)
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
⊢ Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := 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)) ⋯))
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) j) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := 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) ⋯)
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) j) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)

Tactic:
fin_cases j
-- 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
⊢ Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := 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)) ⋯))
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := 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) ⋯)
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)

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
⊢ Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.right)
    (CategoryStruct.comp (Y := 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)) ⋯))
        (WidePullback.base 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) ⟶ f.right)
    (CategoryStruct.comp (Y := 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) ⋯)
        (WidePullback.base 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) ⟶ f.right)

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 : ℕ
dsimp :
  Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
    (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)
        (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌)
        (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
          (fun (i : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) i.succ) ⋯) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
    (𝟙 (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
⊢ Eq (α := f.augmentedCechNerve.left _⦋n⦌ ⟶ f.augmentedCechNerve.left _⦋n⦌)
    (CategoryStruct.comp (Y := f.augmentedCechNerve.left _⦋n + 1⦌)
        (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) (f.augmentedCechNerve.left.δ 0) :
      f.augmentedCechNerve.left _⦋n⦌ ⟶ f.augmentedCechNerve.left _⦋n⦌)
    (𝟙 (f.augmentedCechNerve.left _⦋n⦌) : f.augmentedCechNerve.left _⦋n⦌ ⟶ f.augmentedCechNerve.left _⦋n⦌)

Tactic:
dsimp [SimplicialObject.δ, SimplexCategory.δ]

Premises used: SimplexCategory.δ, CategoryTheory.SimplicialObject.δ
-- 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 (n + 2)
dsimp :
  Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
        (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌)
        (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom)
          (fun (i_1 : Fin (n + 1 + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) (i.succ.succAbove i_1))
          ⋯) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
        (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
            (fun (i_1 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succAbove i_1)) ⋯ :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
        (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
⊢ Eq (α := f.augmentedCechNerve.left _⦋n + 1⦌ ⟶ f.augmentedCechNerve.left _⦋n + 1⦌)
    (ExtraDegeneracy.s f S (n + 1) ≫ f.augmentedCechNerve.left.δ i.succ :
      f.augmentedCechNerve.left _⦋n + 1⦌ ⟶ f.augmentedCechNerve.left _⦋n + 1⦌)
    (f.augmentedCechNerve.left.δ i ≫ ExtraDegeneracy.s f S n :
      f.augmentedCechNerve.left _⦋n + 1⦌ ⟶ f.augmentedCechNerve.left _⦋n + 1⦌)

Tactic:
dsimp [SimplicialObject.δ, SimplexCategory.δ]

Premises used: SimplexCategory.δ, CategoryTheory.SimplicialObject.δ
-- 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 (n + 2)
⊢ Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 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)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
            f.hom)
          (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌)
          (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom)
            (fun (i_1 : Fin (n + 1 + 1)) ↦
              WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) (i.succ.succAbove i_1))
            ⋯))
        (WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) 0) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 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)
        (CategoryStruct.comp (Y :=
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
            (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
                (fun (i_1 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succAbove i_1)) ⋯ :
              (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                  f.hom) ⟶
                widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
            (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
        (WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) 0 :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
            f.left) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
        f.left)

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 (n + 2)
i_1 : Fin (n + 1)
⊢ Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 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)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
            f.hom)
          (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌)
          (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom)
            (fun (i_2 : Fin (n + 1 + 1)) ↦
              WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) (i.succ.succAbove i_2))
            ⋯))
        (WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) i_1.succ) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 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)
        (CategoryStruct.comp (Y :=
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
            (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
                (fun (i_2 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succAbove i_2)) ⋯ :
              (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                  f.hom) ⟶
                widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
            (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
        (WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) i_1.succ :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
            f.left) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
        f.left)

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 (n + 2)
⊢ Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
      f.right)
    (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)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
            f.hom)
          (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌)
          (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom)
            (fun (i_1 : Fin (n + 1 + 1)) ↦
              WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) (i.succ.succAbove i_1))
            ⋯))
        (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
        f.right)
    (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)
        (CategoryStruct.comp (Y :=
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
            (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
                (fun (i_1 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succAbove i_1)) ⋯ :
              (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                  f.hom) ⟶
                widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
            (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
        (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
            f.right) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
        f.right)

Tactic:
simp