awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ 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))
have 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
Tactic: rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ 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))
have 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
Tactic: rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ 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))
have 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
Tactic: rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ 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))
have pos₄ : Eq.{v_1 + 1} (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) 0 0
Tactic: rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (hypothesis)
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
⊢ 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))
have hi₁ : n = (↑i : ℕ) + q
Tactic: replace hi : n = i + q := by lia
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ 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))
have 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))
Tactic: rcases n with _ | n
Cleared hypotheses: n, hq, i, h, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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))
⊢ 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))
have 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))
Tactic: rcases n with _ | n
Cleared hypotheses: n, hq, i, h, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ 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))
have neg : ∀ (h : ¬HAdd.hAdd (α := ℕ) 0 1 ≤ (↑((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋0⦌.len + 1))) : ℕ) + q)
  (hi : 0 = (↑((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋0⦌.len + 1))) : ℕ) + q),
  Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
    (X.σ ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : 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: fin_cases i
Cleared hypotheses: i, h, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ 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))
have neg : Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
  (X.σ ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : 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: rw [show q = 0 by lia]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ 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))
have neg : Eq (α := X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 1) (X.σ 0 ≫ HomologicalComplex.Hom.f (P 1) 1) 0
Tactic: change X.σ 0 ≫ (P 1).f 1 = 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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
⊢ Eq (α := X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 1) (X.σ 0 ≫ HomologicalComplex.Hom.f (P 1) 1)
    0
have 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 sorry)
      (X.σ 0 ≫
        HomologicalComplex.Hom.f (P 0) 1 ≫ hσ' 0 1 2 sorry ≫ ∑ i : Fin (1 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
  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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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 ≫ 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
have 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, sorry⟩ : 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, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ≫
            ∑ 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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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 ≫ 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
have 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
Tactic: dsimp [P_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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 ≫ 𝟙 (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
have 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
Tactic: rw [comp_id, Fin.sum_univ_two,
          Fin.sum_univ_succ, Fin.sum_univ_two]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (goal)
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 +
      (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
have 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
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]