awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ (↑i.succ : ℕ) + q
⊢ φ ≫ X.δ i.succ = 0
have apply : n + 1 ≤ (↑i : ℕ) + q
Tactic: apply v i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y Z : C
q n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ (↑j : ℕ) + q
⊢ (f ≫ φ) ≫ X.δ j.succ = 0
have rw : f ≫ φ ≫ X.δ j.succ = 0
Tactic: rw [assoc, v j hj, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y Z : C
q n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ (↑j : ℕ) + q
rw : f ≫ φ ≫ X.δ j.succ = 0
⊢ (f ≫ φ) ≫ X.δ j.succ = 0
have rw₁ : Eq (α := Z ⟶ X _⦋n⦌) (f ≫ 0) 0
Tactic: rw [assoc, v j hj, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y Z : C
q n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ (↑j : ℕ) + q
rw : f ≫ φ ≫ X.δ j.succ = 0
rw₁ : Eq (α := Z ⟶ X _⦋n⦌) (f ≫ 0) 0
⊢ (f ≫ φ) ≫ X.δ j.succ = 0
have rw₂ : Eq.{v_1 + 1} (α := Z ⟶ X _⦋n⦌) 0 0
Tactic: rw [assoc, v j hj, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))
have hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
Tactic: have hnaq_shift (d : ℕ) : n + d = a + d + q := by lia
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))
have rw : φ ≫
    HAdd.hAdd (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (β :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 1) n ≫
        (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, sorry⟩ : Fin (n + 1))) ≫ eqToHom sorry)
      ((HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (HPow.hPow (α := ℤ) (-1) (a + 1))
            (X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1))) ≫
          eqToHom sorry) ≫
        HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
  -φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2)) ≫ X.σ ⟨a, sorry⟩
Tactic: rw [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl),
    hσ'_eq hnaq (c_mk (n + 1) n rfl), hσ'_eq (hnaq_shift 1) (c_mk (n + 2) (n + 1) rfl)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ φ ≫
      HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (β :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 1) n ≫
          (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯)
        ((HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (HPow.hPow (α := ℤ) (-1) (a + 1))
              (X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫
            eqToHom ⋯) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩
have simp : HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ j : Fin (n + 2),
      φ ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, sorry⟩ : Fin (n + 1))))
    (∑ j : Fin (n + 1 + 2),
      φ ≫
        HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (HPow.hPow (α := ℤ) (-1) (a + 1))
            (X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1))) ≫
          (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j)) =
  -φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2)) ≫ X.σ ⟨a, sorry⟩
Tactic: simp only [AlternatingFaceMapComplex.obj_d_eq, eqToHom_refl, comp_id, comp_sum, sum_comp,
    comp_add]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ j : Fin (n + 2),
        φ ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ (HPow.hPow (α := ℤ) (-1) a • X.σ (⟨a, ⋯⟩ : Fin (n + 1))))
      (∑ j : Fin (n + 1 + 2),
        φ ≫
          HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (HPow.hPow (α := ℤ) (-1) (a + 1))
              (X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫
            (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j)) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩
have simp : HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ x : Fin (n + 2),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑x : ℕ)) • (φ ≫ X.δ x) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)))
    (∑ x : Fin (n + 1 + 2),
      (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        (φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1))) ≫ X.δ x) =
  -(φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2))) ≫ X.σ ⟨a, sorry⟩
Tactic: simp only [comp_zsmul, zsmul_comp, ← assoc, ← mul_zsmul]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ x : Fin (n + 2),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑x : ℕ)) • (φ ≫ X.δ x) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
      (∑ x : Fin (n + 1 + 2),
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ x) =
    -(φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ ⟨a, ⋯⟩
have rw : HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ i : Fin (a + 2),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q i)) : ℕ)) •
        (φ ≫ X.δ (Fin.cast sorry (Fin.castAdd q i))) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)))
    (∑ x : Fin (n + 1 + 2),
      (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        (φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1))) ≫ X.δ x) =
  -(φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2))) ≫ X.σ ⟨a, sorry⟩
Tactic: rw [← Fin.sum_congr' _ (hnaq_shift 2).symm, Fin.sum_trunc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
rw :
  HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ i : Fin (a + 2),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i)) : ℕ)) •
          (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
      (∑ x : Fin (n + 1 + 2),
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ x) =
    -(φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ ⟨a, ⋯⟩
⊢ HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ x : Fin (n + 2),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑x : ℕ)) • (φ ≫ X.δ x) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
      (∑ x : Fin (n + 1 + 2),
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ x) =
    -(φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ ⟨a, ⋯⟩
have hf : ∀ (j : Fin q),
  (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.natAdd (a + 2) j)) : ℕ)) •
      (φ ≫ X.δ (Fin.cast sorry (Fin.natAdd (a + 2) j))) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) =
    0
Tactic: rw [← Fin.sum_congr' _ (hnaq_shift 2).symm, Fin.sum_trunc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.natAdd (a + 2) (⟨k, hk⟩ : Fin q))) : ℕ)) •
      (φ ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 2) (⟨k, hk⟩ : Fin q)))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
    0
have hf : φ ≫ X.δ (⟨a + 2 + k, sorry⟩ : Fin (n + 2)) = 0
Tactic: suffices φ ≫ X.δ (⟨a + 2 + k, by lia⟩ : Fin (n + 2)) = 0 by
      simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ φ ≫ X.δ (⟨a + 2 + k, ⋯⟩ : Fin (n + 2)) = 0
have h : a + 2 + k = (↑(⟨a + k + 1, sorry⟩ : Fin (n + 1)).succ : ℕ)
Tactic: convert! v ⟨a + k + 1, by lia⟩ (by rw [Fin.val_mk]; lia)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ i : Fin (a + 2),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i)) : ℕ)) •
          (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
      (∑ x : Fin (n + 1 + 2),
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ x) =
    -(φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ ⟨a, ⋯⟩
have rw : HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ i : Fin (a + 2),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q i)) : ℕ)) •
        (φ ≫ X.δ (Fin.cast sorry (Fin.castAdd q i))) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)))
    (∑ i : Fin (a + 3),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q i)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        (φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1))) ≫ X.δ (Fin.cast sorry (Fin.castAdd q i))) =
  -(φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2))) ≫ X.σ ⟨a, sorry⟩
Tactic: rw [← Fin.sum_congr' _ (hnaq_shift 3).symm, @Fin.sum_trunc _ _ (a + 3)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
rw :
  HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ i : Fin (a + 2),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i)) : ℕ)) •
          (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
      (∑ i : Fin (a + 3),
        (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) =
    -(φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ ⟨a, ⋯⟩
⊢ HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ i : Fin (a + 2),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i)) : ℕ)) •
          (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
      (∑ x : Fin (n + 1 + 2),
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ x) =
    -(φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ ⟨a, ⋯⟩
have hf : ∀ (j : Fin q),
  (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.natAdd (a + 3) j) : Fin (n + 3)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      (φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1))) ≫ X.δ (Fin.cast sorry (Fin.natAdd (a + 3) j)) =
    0
Tactic: rw [← Fin.sum_congr' _ (hnaq_shift 3).symm, @Fin.sum_trunc _ _ (a + 3)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q)) : Fin (n + 3)) : ℕ) *
        HPow.hPow (α := ℤ) (-1) (a + 1)) •
      (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) =
    0
have hf : Fin.pred (Fin.cast sorry (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) sorry ≠ 0
Tactic: rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
hf : Fin.pred (Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) ⋯ ≠ 0
⊢ (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q)) : Fin (n + 3)) : ℕ) *
        HPow.hPow (α := ℤ) (-1) (a + 1)) •
      (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) =
    0
have hf₁ : n + 2 ≤ (↑(Fin.pred (Fin.cast sorry (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) sorry) : ℕ) + q
Tactic: rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
hf : Fin.pred (Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) ⋯ ≠ 0
hf₁ : n + 2 ≤ (↑(Fin.pred (Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) ⋯) : ℕ) + q
⊢ (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q)) : Fin (n + 3)) : ℕ) *
        HPow.hPow (α := ℤ) (-1) (a + 1)) •
      (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) =
    0
have hf₂ : LT.lt (α := Fin (n + 2 + 1)) (Fin.succ ⟨a + 1, sorry⟩) (Fin.cast sorry (Fin.natAdd (a + 3) ⟨k, hk⟩))
Tactic: rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
h : Fin.pred (Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) ⋯ = 0
⊢ False
have h₁ : a + 3 + k = 1
Tactic: replace h : a + 3 + k = 1 := by simp [Fin.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 2 ≤ (↑(Fin.pred (Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) ⋯) : ℕ) + q
have hf : n + 2 ≤ a + 3 + k - 1 + q
Tactic: dsimp [Fin.cast, Fin.pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 2 ≤ a + 3 + k - 1 + q
have hf : n + 2 ≤ a + k + HSub.hSub (α := ℕ) 3 1 + q
Tactic: rw [Nat.add_right_comm, Nat.add_sub_assoc (by simp : 1 ≤ 3)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ (↑(Fin.succ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) : ℕ) < (↑(Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩) : Fin (n + 3)) : ℕ)
have hf : a + 1 + 1 < a + 3 + k
Tactic: dsimp [Fin.natAdd, Fin.cast]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (∑ i : Fin (a + 2),
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i)) : ℕ)) •
          (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
      (∑ i : Fin (a + 3),
        (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
          (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) =
    -(φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ ⟨a, ⋯⟩
have simp : HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ x : Fin (a + 2),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q x)) : ℕ)) •
        φ ≫ X.δ (Fin.cast sorry (Fin.castAdd q x)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)))
    (∑ x : Fin (a + 3),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q x))) =
  -φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2)) ≫ X.σ ⟨a, sorry⟩
Tactic: simp only [assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ x : Fin (a + 2),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ)) •
        φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
    (∑ x : Fin (a + 3),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)))
have a₁ : ∑ x : Fin (a + 2),
  (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q x)) : ℕ)) •
    φ ≫ X.δ (Fin.cast sorry (Fin.castAdd q x)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1))
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
a₁ :
  ∑ x : Fin (a + 2),
    (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ)) •
      φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))
| HAdd.hAdd (α := Y ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
    (∑ x : Fin (a + 2),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ)) •
        φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)))
    (∑ x : Fin (a + 3),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)))
have a₂ : ∑ x : Fin (a + 3),
  (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q x)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
    φ ≫ X.σ (⟨a + 1, sorry⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast sorry (Fin.castAdd q x))
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| ∑ x : Fin (a + 2),
    (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q x)) : ℕ)) •
      φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1))
have a₁ : ∑ i : Fin (a + 1),
    (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q i.castSucc)) : ℕ)) •
      φ ≫ X.δ (Fin.cast sorry (Fin.castAdd q i.castSucc)) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) +
  (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast sorry (Fin.castAdd q (Fin.last (a + 1)))) : ℕ)) •
    φ ≫ X.δ (Fin.cast sorry (Fin.castAdd q (Fin.last (a + 1)))) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1))
Tactic: rw [Fin.sum_univ_castSucc]