awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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, ⋯⟩
hf :
  ∀ (j : Fin q),
    (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.natAdd (a + 2) j)) : ℕ)) •
        (φ ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 2) j))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) =
      0
⊢ 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, ⋯⟩

Tactic:
rw [← Fin.sum_congr' _ (hnaq_shift 2).symm, Fin.sum_trunc]

Premises used: Fin.sum_trunc, Fin.sum_congr', OfNat.ofNat, Eq.symm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
⊢ a + 2 + k < n + 2

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
this : φ ≫ X.δ (⟨a + 2 + k, ⋯⟩ : Fin (n + 2)) = 0
⊢ (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

Tactic:
simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]

Premises used: smul_zero, Fin.cast_mk, CategoryTheory.Limits.zero_comp, Fin.natAdd_mk
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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 : φ ≫ X.δ (⟨a + 2 + k, ⋯⟩ : Fin (n + 2)) = 0
⊢ (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

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]
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
⊢ a + k + 1 < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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 + 1 ≤ a + k + 1 + q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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 : a + 2 + k = (↑(⟨a + k + 1, ⋯⟩ : Fin (n + 1)).succ : ℕ)
⊢ φ ≫ X.δ (⟨a + 2 + k, ⋯⟩ : Fin (n + 2)) = 0

Tactic:
convert! v ⟨a + k + 1, by lia⟩ (by rw [Fin.val_mk]; lia)

Premises used: Fin.mk, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
⊢ a + 2 + k = a + k + 1 + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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, ⋯⟩
hf :
  ∀ (j : Fin q),
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.natAdd (a + 3) j) : Fin (n + 3)) : ℕ) *
          HPow.hPow (α := ℤ) (-1) (a + 1)) •
        (φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 3) j)) =
      0
⊢ 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, ⋯⟩

Tactic:
rw [← Fin.sum_congr' _ (hnaq_shift 3).symm, @Fin.sum_trunc _ _ (a + 3)]

Premises used: Fin.sum_trunc, Fin.sum_congr', OfNat.ofNat, Eq.symm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
hf₂ : LT.lt (α := Fin (n + 2 + 1)) (Fin.succ ⟨a + 1, ⋯⟩) (Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩))
⊢ (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

Tactic:
rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]

Premises used: CategoryTheory.Category.assoc, zsmul_zero, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt', CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
⊢ a + 3 + k = 1

Tactic:
simp [Fin.ext_iff] at h

Premises used: Fin.ext_iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
⊢ a + 3 + k = 1

Tactic:
replace h : a + 3 + k = 1 := by simp [Fin.ext_iff] at h
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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 : a + 3 + k = 1
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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 : n + 2 ≤ a + 3 + k - 1 + q
⊢ n + 2 ≤ (↑(Fin.pred (Fin.cast ⋯ (Fin.natAdd (a + 3) (⟨k, hk⟩ : Fin q))) ⋯) : ℕ) + q

Tactic:
dsimp [Fin.cast, Fin.pred]

Premises used: Fin.pred, Fin.cast
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
⊢ LE.le (α := ℕ) 1 3

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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 : n + 2 ≤ a + k + HSub.hSub (α := ℕ) 3 1 + q
⊢ n + 2 ≤ a + 3 + k - 1 + q

Tactic:
rw [Nat.add_right_comm, Nat.add_sub_assoc (by simp : 1 ≤ 3)]

Premises used: Nat.add_sub_assoc, Nat.add_right_comm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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 + k + HSub.hSub (α := ℕ) 3 1 + q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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 : a + 1 + 1 < a + 3 + k
⊢ (↑(Fin.succ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1))) : ℕ) < (↑(Fin.cast ⋯ (Fin.natAdd (a + 3) ⟨k, hk⟩) : Fin (n + 3)) : ℕ)

Tactic:
dsimp [Fin.natAdd, Fin.cast]

Premises used: Fin.natAdd, Fin.cast
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
⊢ a + 1 + 1 < a + 3 + k

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
simp :
  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))) =
    -φ ≫ 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)))
      (∑ 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, ⋯⟩

Tactic:
simp only [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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))
a₂ :
  ∑ 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))
| 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)))

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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₁ :
  ∑ i : Fin (a + 1),
      (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc)) : ℕ)) •
        φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) +
    (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1)))) : ℕ)) •
      φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1)))) ≫ X.σ (⟨a, ⋯⟩ : Fin (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))

Tactic:
rw [Fin.sum_univ_castSucc]

Premises used: Fin.sum_univ_castSucc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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))

Tactic:
· rw [Fin.sum_univ_castSucc]

Premises used: Fin.sum_univ_castSucc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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₁ :
  ∑ i : Fin (a + 1),
        (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) : ℕ) *
            HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) +
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1)))) : Fin (n + 3)) : ℕ) *
          HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1))))) +
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2)))) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2))))
| ∑ 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))

Tactic:
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]

Premises used: Fin.sum_univ_castSucc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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₁ :
  ∑ i : Fin (a + 2),
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc)) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc)) +
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2)))) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2))))
a₂ :
  ∑ i : Fin (a + 1),
        (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) : ℕ) *
            HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) +
      (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1)))) : Fin (n + 3)) : ℕ) *
          HPow.hPow (α := ℤ) (-1) (a + 1)) •
        φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1))))) +
    (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2)))) : ℕ) * HPow.hPow (α := ℤ) (-1) (a + 1)) •
      φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2))))
| ∑ 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))

Tactic:
· rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]

Premises used: Fin.sum_univ_castSucc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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))
a₂ a₃ :
  ∑ 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))
| 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)))

Tactic:
congr
    · rw [Fin.sum_univ_castSucc]
    · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]

Premises used: Fin.sum_univ_castSucc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
conv_lhs :
  ∑ i : Fin (a + 1),
          (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc)) : ℕ)) •
            φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc)) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) +
        (HPow.hPow (α := ℤ) (-1) a * HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1)))) : ℕ)) •
          φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1)))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) +
      (∑ i : Fin (a + 1),
            (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) : ℕ) *
                HPow.hPow (α := ℤ) (-1) (a + 1)) •
              φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) +
          (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1)))) : Fin (n + 3)) : ℕ) *
              HPow.hPow (α := ℤ) (-1) (a + 1)) •
            φ ≫
              X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.castSucc (Fin.last (a + 1))))) +
        (HPow.hPow (α := ℤ) (-1) (↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2)))) : ℕ) *
            HPow.hPow (α := ℤ) (-1) (a + 1)) •
          φ ≫ X.σ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2))))) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩
⊢ 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))) =
    -φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2)) ≫ X.σ ⟨a, ⋯⟩

Tactic:
conv_lhs =>
    congr
    · rw [Fin.sum_univ_castSucc]
    · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]

Premises used: Fin.sum_univ_castSucc