awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n q : ℕ
hq :
  ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
i : Fin (n + 1)
hi : n + 1 ≤ (↑i : ℕ) + (q + 1)
pos :
  ∀ (h : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
neg :
  ∀ (h : ¬n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))

Tactic:
by_cases h : n + 1 ≤ (i : ℕ) + q

Premises used: Fin.val
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n q : ℕ
hq :
  ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
i : Fin (n + 1)
hi : n + 1 ≤ (↑i : ℕ) + (q + 1)
h : n + 1 ≤ (↑i : ℕ) + q
pos :
  X.σ i ≫
      (P q ≫
            HAdd.hAdd (α :=
              Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
                (AlternatingFaceMapComplex.obj X))
              (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
        (n + 1) =
    0
pos₁ :
  X.σ i ≫
      HomologicalComplex.Hom.f (P q) (n + 1) ≫
        (HAdd.hAdd (α :=
              Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
                (AlternatingFaceMapComplex.obj X))
              (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
          (n + 1) =
    0
pos₂ :
  (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1)) ≫
      (HAdd.hAdd (α :=
            Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
              (AlternatingFaceMapComplex.obj X))
            (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
        (n + 1) =
    0
pos₃ :
  Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 ≫
      (HAdd.hAdd (α :=
            Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
              (AlternatingFaceMapComplex.obj X))
            (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
        (n + 1))
    0
pos₄ pos₅ : Eq.{v_1 + 1} (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) 0 0
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))

Tactic:
rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n q : ℕ
hq :
  ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
i : Fin (n + 1)
hi : n + 1 ≤ (↑i : ℕ) + (q + 1)
h : ¬n + 1 ≤ (↑i : ℕ) + q
⊢ n = (↑i : ℕ) + q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n q : ℕ
hq :
  ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
i : Fin (n + 1)
hi : n + 1 ≤ (↑i : ℕ) + (q + 1)
h : ¬n + 1 ≤ (↑i : ℕ) + q
⊢ n = (↑i : ℕ) + q

Tactic:
replace hi : n = i + q := by lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n q : ℕ
hq :
  ∀ (i : Fin (n + 1)) (hi : n + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
      (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
i : Fin (n + 1)
h : ¬n + 1 ≤ (↑i : ℕ) + q
hi : n = (↑i : ℕ) + q
neg :
  ∀
    (hq :
      ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
        Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
          (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
          (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1)))
    (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (h : ¬HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q) (hi : 0 = (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
neg₁ :
  ∀ (n : ℕ)
    (hq :
      ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
        Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
          (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
          (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1)))
    (i : Fin (n + 1 + 1)) (h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q) (hi : n + 1 = (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))

Tactic:
rcases n with _ | n
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
h : ¬HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q
hi : 0 = (↑i : ℕ) + q
neg :
  ∀ (h : ¬HAdd.hAdd (α := ℕ) 0 1 ≤ (↑((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1))) : ℕ) + q)
    (hi : 0 = (↑((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1))) : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1))) ≫
          HomologicalComplex.Hom.f (P (q + 1)) (HAdd.hAdd (α := ℕ) 0 1) :
        X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
⊢ Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
    (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
    (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ q = 0

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
neg :
  Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
    (X.σ ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1))) ≫
        HomologicalComplex.Hom.f (P (HAdd.hAdd (α := ℕ) 0 1)) (HAdd.hAdd (α := ℕ) 0 1) :
      X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
    (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
⊢ Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
    (X.σ ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1))) ≫
        HomologicalComplex.Hom.f (P (q + 1)) (HAdd.hAdd (α := ℕ) 0 1) :
      X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
    (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
rw [show q = 0 by lia]
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
neg :
  Eq (α := X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 1) (X.σ 0 ≫ HomologicalComplex.Hom.f (P 1) 1)
    0
⊢ Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
    (X.σ ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1))) ≫
        HomologicalComplex.Hom.f (P (HAdd.hAdd (α := ℕ) 0 1)) (HAdd.hAdd (α := ℕ) 0 1) :
      X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
    (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
change X.σ 0 ≫ (P 1).f 1 = 0

Premises used: HomologicalComplex.Hom.f, OfNat.ofNat, CategoryTheory.SimplicialObject.σ, AlgebraicTopology.DoldKan.P
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
neg :
  X.σ 0 ≫ HomologicalComplex.Hom.f (P 0) 1 +
      HAdd.hAdd (α := X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 1)
        (X.σ 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            (∑ i : Fin (0 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫ hσ' 0 0 1 ⋯)
        (X.σ 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            hσ' 0 1 2 ⋯ ≫ ∑ i : Fin (1 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
    0
⊢ Eq (α := X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 1) (X.σ 0 ≫ HomologicalComplex.Hom.f (P 1) 1)
    0

Tactic:
simp only [P_succ, HomologicalComplex.add_f_apply, comp_add,
          AlternatingFaceMapComplex.obj_d_eq, Hσ,
          HomologicalComplex.comp_f, Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl),
          comp_id]

Premises used: HomologicalComplex.add_f_apply, AlgebraicTopology.DoldKan.Hσ, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, AlgebraicTopology.DoldKan.c_mk, CategoryTheory.Preadditive.comp_add, Homotopy.nullHomotopicMap'_f, OfNat.ofNat, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
neg :
  X.σ 0 ≫ HomologicalComplex.Hom.f (P 0) 1 +
      (X.σ 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            (∑ i : Fin (0 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫
              HSMul.hSMul (β := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (HPow.hPow (α := ℤ) (β := ℕ) (-1) 0)
                (X.σ (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) +
        X.σ 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            HSMul.hSMul (β := X _⦋1⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 1 1⦌) (HPow.hPow (α := ℤ) (β := ℕ) (-1) 1)
                (X.σ (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ≫
              ∑ i : Fin (1 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
    0
⊢ X.σ 0 ≫ HomologicalComplex.Hom.f (P 0) 1 +
      HAdd.hAdd (α := X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 1)
        (X.σ 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            (∑ i : Fin (0 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫ hσ' 0 0 1 ⋯)
        (X.σ 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            hσ' 0 1 2 ⋯ ≫ ∑ i : Fin (1 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
    0

Tactic:
rw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm]

Premises used: zero_add, add_zero, OfNat.ofNat, Eq.symm, AlgebraicTopology.DoldKan.hσ'_eq'
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
neg :
  X.σ 0 ≫ 𝟙 (X _⦋1⦌) +
      (X.σ 0 ≫
          𝟙 (X _⦋1⦌) ≫
            (∑ i : Fin 2, HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫
              HSMul.hSMul (α := ℤ) (β := X _⦋0⦌ ⟶ X _⦋1⦌) 1 (X.σ 0) +
        X.σ 0 ≫
          𝟙 (X _⦋1⦌) ≫
            HSMul.hSMul (α := ℤ) (β := X _⦋1⦌ ⟶ X _⦋2⦌) (-1) (X.σ 1) ≫
              ∑ i : Fin 3, HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
    0
⊢ X.σ 0 ≫ HomologicalComplex.Hom.f (P 0) 1 +
      (X.σ 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            (∑ i : Fin (0 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫
              HSMul.hSMul (β := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (HPow.hPow (α := ℤ) (β := ℕ) (-1) 0)
                (X.σ (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) +
        X.σ 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            HSMul.hSMul (β := X _⦋1⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 1 1⦌) (HPow.hPow (α := ℤ) (β := ℕ) (-1) 1)
                (X.σ (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ≫
              ∑ i : Fin (1 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
    0

Tactic:
dsimp [P_zero]

Premises used: AlgebraicTopology.DoldKan.P_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
neg :
  X.σ 0 +
      (X.σ 0 ≫
          𝟙 (X _⦋1⦌) ≫
            (HSMul.hSMul (β := X _⦋1⦌ ⟶ X _⦋0⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) +
                HSMul.hSMul (β := X _⦋1⦌ ⟶ X _⦋0⦌) (HPow.hPow (α := ℤ) (-1) (↑1 : ℕ)) (X.δ 1)) ≫
              HSMul.hSMul (α := ℤ) (β := X _⦋0⦌ ⟶ X _⦋1⦌) 1 (X.σ 0) +
        X.σ 0 ≫
          𝟙 (X _⦋1⦌) ≫
            HSMul.hSMul (α := ℤ) (β := X _⦋1⦌ ⟶ X _⦋2⦌) (-1) (X.σ 1) ≫
              (HSMul.hSMul (β := X _⦋2⦌ ⟶ X _⦋1⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) +
                (HSMul.hSMul (β := X _⦋2⦌ ⟶ X _⦋1⦌) (HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 0) : ℕ)) (X.δ (Fin.succ 0)) +
                  HSMul.hSMul (β := X _⦋2⦌ ⟶ X _⦋1⦌) (HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 1) : ℕ))
                    (X.δ (Fin.succ 1))))) =
    0
⊢ X.σ 0 ≫ 𝟙 (X _⦋1⦌) +
      (X.σ 0 ≫
          𝟙 (X _⦋1⦌) ≫
            (∑ i : Fin 2, HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) ≫
              HSMul.hSMul (α := ℤ) (β := X _⦋0⦌ ⟶ X _⦋1⦌) 1 (X.σ 0) +
        X.σ 0 ≫
          𝟙 (X _⦋1⦌) ≫
            HSMul.hSMul (α := ℤ) (β := X _⦋1⦌ ⟶ X _⦋2⦌) (-1) (X.σ 1) ≫
              ∑ i : Fin 3, HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
    0

Tactic:
rw [comp_id, Fin.sum_univ_two,
          Fin.sum_univ_succ, Fin.sum_univ_two]

Premises used: CategoryTheory.Category.comp_id, Fin.sum_univ_two, Fin.sum_univ_succ
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
neg :
  X.σ 0 +
      (HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0 ≫ X.δ 0 ≫ X.σ 0) (-X.σ 0 ≫ X.δ 1 ≫ X.σ 0) +
        (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 +
          HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0 ≫ X.σ 1 ≫ X.δ 1) (-X.σ 0 ≫ X.σ 1 ≫ X.δ (Fin.succ 1)))) =
    0
⊢ X.σ 0 +
      (X.σ 0 ≫
          𝟙 (X _⦋1⦌) ≫
            (HSMul.hSMul (β := X _⦋1⦌ ⟶ X _⦋0⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) +
                HSMul.hSMul (β := X _⦋1⦌ ⟶ X _⦋0⦌) (HPow.hPow (α := ℤ) (-1) (↑1 : ℕ)) (X.δ 1)) ≫
              HSMul.hSMul (α := ℤ) (β := X _⦋0⦌ ⟶ X _⦋1⦌) 1 (X.σ 0) +
        X.σ 0 ≫
          𝟙 (X _⦋1⦌) ≫
            HSMul.hSMul (α := ℤ) (β := X _⦋1⦌ ⟶ X _⦋2⦌) (-1) (X.σ 1) ≫
              (HSMul.hSMul (β := X _⦋2⦌ ⟶ X _⦋1⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) +
                (HSMul.hSMul (β := X _⦋2⦌ ⟶ X _⦋1⦌) (HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 0) : ℕ)) (X.δ (Fin.succ 0)) +
                  HSMul.hSMul (β := X _⦋2⦌ ⟶ X _⦋1⦌) (HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 1) : ℕ))
                    (X.δ (Fin.succ 1))))) =
    0

Tactic:
simp only [Fin.val_zero, pow_zero, pow_one, pow_add, one_smul, neg_smul, Fin.val_succ,
          Fin.val_one, mul_neg, one_mul, neg_mul, neg_neg, id_comp, add_comp, comp_add, neg_comp,
          comp_neg, Fin.succ_zero_eq_one]

Premises used: neg_smul, CategoryTheory.Preadditive.comp_neg, pow_add, neg_neg, Fin.val_one, Fin.val_succ, Fin.succ_zero_eq_one, pow_zero, one_smul, CategoryTheory.Preadditive.add_comp, pow_one, CategoryTheory.Preadditive.comp_add, CategoryTheory.Preadditive.neg_comp, neg_mul, Fin.val_zero, one_mul, mul_neg, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
rw rw₁ : LE.le (α := Fin 2) 0 0
⊢ LE.le (α := Fin 2) 0 (Fin.castSucc 0)

Tactic:
rw [Fin.castSucc_zero]

Premises used: Fin.castSucc_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
neg :
  X.σ 0 +
      (HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0) (-X.σ 0) +
        (-X.σ 0 + HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0) (-X.σ 0))) =
    0
⊢ X.σ 0 +
      (HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0 ≫ X.δ 0 ≫ X.σ 0) (-X.σ 0 ≫ X.δ 1 ≫ X.σ 0) +
        (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 +
          HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0 ≫ X.σ 1 ≫ X.δ 1) (-X.σ 0 ≫ X.σ 1 ≫ X.δ (Fin.succ 1)))) =
    0

Tactic:
rw [← Fin.castSucc_one, SimplicialObject.δ_comp_σ_self, ← Fin.castSucc_zero (n := 1),
          SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ, comp_id, ← Fin.castSucc_zero (n := 2),
          ← Fin.succ_zero_eq_one,
          SimplicialObject.δ_comp_σ_of_le X
            (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
          ← Fin.castSucc_zero (n := 1), SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ_assoc]

Premises used: Fin.castSucc_one, CategoryTheory.Category.comp_id, Fin.succ_zero_eq_one, CategoryTheory.SimplicialObject.δ_comp_σ_of_le, CategoryTheory.SimplicialObject.δ_comp_σ_self, Fin.castSucc_zero, CategoryTheory.SimplicialObject.δ_comp_σ_succ, CategoryTheory.SimplicialObject.δ_comp_σ_self_assoc, CategoryTheory.SimplicialObject.δ_comp_σ_succ_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0) (-X.σ 0) +
        (-X.σ 0 + HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0) (-X.σ 0))) =
    0

Tactic:
simp only [add_neg_cancel, add_zero, zero_add]

Premises used: add_neg_cancel, zero_add, add_zero