C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
have hnaq_shift : ∀ d : ℕ, n + d = a + d + q := by
  intro d
  rw [add_assoc, add_comm d, ← add_assoc, hnaq]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ φ ≫
      (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 1) n ≫
          ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫
            eqToHom (_ : X.obj [n + 1].op = X.obj [n + 1].op) +
        (((-1) ^ (a + 1) • σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
            eqToHom (_ : X.obj [n + 1 + 1].op = X.obj [n + 2].op)) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
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)]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun j =>
        φ ≫ ((-1) ^ ↑j • δ X j) ≫ ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) })) +
      Finset.sum Finset.univ fun j =>
        φ ≫ ((-1) ^ (a + 1) • σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫ ((-1) ^ ↑j • δ X j)) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ φ ≫
      (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 1) n ≫
          ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫
            eqToHom (_ : X.obj [n + 1].op = X.obj [n + 1].op) +
        (((-1) ^ (a + 1) • σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
            eqToHom (_ : X.obj [n + 1 + 1].op = X.obj [n + 2].op)) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
simp only [AlternatingFaceMapComplex.obj_d_eq, eqToHom_refl, comp_id, comp_sum, sum_comp,
  comp_add]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun x =>
        ((-1) ^ a * (-1) ^ ↑x) • (φ ≫ δ X x) ≫ σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun x =>
        ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫ δ X x) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun j =>
        φ ≫ ((-1) ^ ↑j • δ X j) ≫ ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) })) +
      Finset.sum Finset.univ fun j =>
        φ ≫ ((-1) ^ (a + 1) • σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫ ((-1) ^ ↑j • δ X j)) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
simp only [comp_zsmul, zsmul_comp, ← assoc, ← mul_zsmul]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) •
          (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun x =>
        ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫ δ X x) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }

case hf
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) j))) •
        (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) j))) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) } =
      0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun x =>
        ((-1) ^ a * (-1) ^ ↑x) • (φ ≫ δ X x) ≫ σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun x =>
        ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫ δ X x) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }
rw [← Fin.sum_congr' _ (hnaq_shift 2).symm, Fin.sum_trunc]
case hf
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) j))) •
        (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) j))) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) } =
      0

C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) •
          (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun x =>
        ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫ δ X x) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) •
          (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun x =>
        ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫ δ X x) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }

case hf
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) j))) •
        (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) j))) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) } =
      0
swap
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) •
          (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun i =>
        ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) i)) * (-1) ^ (a + 1)) •
          (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
            δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) i))) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }

case hf
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) j)) * (-1) ^ (a + 1)) •
        (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
          δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) j)) =
      0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) •
          (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun x =>
        ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫ δ X x) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }
rw [← Fin.sum_congr' _ (hnaq_shift 3).symm, @Fin.sum_trunc _ _ (a + 3)]
case hf
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) j)) * (-1) ^ (a + 1)) •
        (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
          δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) j)) =
      0

C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) •
          (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun i =>
        ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) i)) * (-1) ^ (a + 1)) •
          (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
            δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) i))) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) •
          (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun i =>
        ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) i)) * (-1) ^ (a + 1)) •
          (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
            δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) i))) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }

case hf
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) j)) * (-1) ^ (a + 1)) •
        (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
          δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) j)) =
      0
swap
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun x =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) x))) •
          φ ≫
            δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) x)) ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun x =>
        ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) x)) * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) x))) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) •
          (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) i))) ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun i =>
        ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) i)) * (-1) ^ (a + 1)) •
          (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
            δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) i))) =
    -(φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) }
simp only [assoc]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ (Finset.sum Finset.univ fun i =>
          ((-1) ^ a *
              (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) (↑Fin.castSucc i)))) •
            φ ≫
              δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) (↑Fin.castSucc i))) ≫
                σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
        ((-1) ^ a *
            (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) (Fin.last (a + 1))))) •
          φ ≫
            δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) (Fin.last (a + 1)))) ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) } +
      ((Finset.sum Finset.univ fun i =>
            ((-1) ^
                  ↑(↑(Fin.cast (_ : a + 3 + q = n + 3))
                      (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (↑Fin.castSucc (↑Fin.castSucc i)))) *
                (-1) ^ (a + 1)) •
              φ ≫
                σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                  δ X
                    (↑(Fin.cast (_ : a + 3 + q = n + 3))
                      (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (↑Fin.castSucc (↑Fin.castSucc i))))) +
          ((-1) ^
                ↑(↑(Fin.cast (_ : a + 3 + q = n + 3))
                    (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (↑Fin.castSucc (Fin.last (a + 1))))) *
              (-1) ^ (a + 1)) •
            φ ≫
              σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                δ X
                  (↑(Fin.cast (_ : a + 3 + q = n + 3))
                    (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (↑Fin.castSucc (Fin.last (a + 1))))) +
        ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (Fin.last (a + 2)))) *
            (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (Fin.last (a + 2))))) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ((Finset.sum Finset.univ fun x =>
        ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) x))) •
          φ ≫
            δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) x)) ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
      Finset.sum Finset.univ fun x =>
        ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) x)) * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) x))) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
conv_lhs =>
  congr
  . rw [Fin.sum_univ_castSucc]
  . rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ (Finset.sum Finset.univ fun i =>
          ((-1) ^ a * (-1) ^ ↑i) •
            φ ≫
              δ X { val := ↑i, isLt := (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc i) < a + 2 + q) } < n + 2) } ≫
                σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
        ((-1) ^ a * (-1) ^ (a + 1)) •
          φ ≫
            δ X
                { val := a + 1,
                  isLt := (_ : ↑{ val := a + 1, isLt := (_ : ↑(Fin.last (a + 1)) < a + 2 + q) } < n + 2) } ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) } +
      ((Finset.sum Finset.univ fun i =>
            ((-1) ^ ↑i * (-1) ^ (a + 1)) •
              φ ≫
                σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                  δ X
                    { val := ↑i,
                      isLt :=
                        (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc i)) < a + 3 + q) } < n + 3) }) +
          ((-1) ^ (a + 1) * (-1) ^ (a + 1)) •
            φ ≫
              σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                δ X
                  { val := a + 1,
                    isLt :=
                      (_ : ↑{ val := a + 1, isLt := (_ : ↑(↑Fin.castSucc (Fin.last (a + 1))) < a + 3 + q) } < n + 3) } +
        ((-1) ^ (a + 2) * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X
                { val := a + 2,
                  isLt := (_ : ↑{ val := a + 2, isLt := (_ : ↑(Fin.last (a + 2)) < a + 3 + q) } < n + 3) }) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ (Finset.sum Finset.univ fun i =>
          ((-1) ^ a *
              (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) (↑Fin.castSucc i)))) •
            φ ≫
              δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) (↑Fin.castSucc i))) ≫
                σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
        ((-1) ^ a *
            (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) (Fin.last (a + 1))))) •
          φ ≫
            δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.castLE (_ : a + 2 ≤ a + 2 + q)) (Fin.last (a + 1)))) ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) } +
      ((Finset.sum Finset.univ fun i =>
            ((-1) ^
                  ↑(↑(Fin.cast (_ : a + 3 + q = n + 3))
                      (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (↑Fin.castSucc (↑Fin.castSucc i)))) *
                (-1) ^ (a + 1)) •
              φ ≫
                σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                  δ X
                    (↑(Fin.cast (_ : a + 3 + q = n + 3))
                      (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (↑Fin.castSucc (↑Fin.castSucc i))))) +
          ((-1) ^
                ↑(↑(Fin.cast (_ : a + 3 + q = n + 3))
                    (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (↑Fin.castSucc (Fin.last (a + 1))))) *
              (-1) ^ (a + 1)) •
            φ ≫
              σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                δ X
                  (↑(Fin.cast (_ : a + 3 + q = n + 3))
                    (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (↑Fin.castSucc (Fin.last (a + 1))))) +
        ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (Fin.last (a + 2)))) *
            (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.castLE (_ : a + 3 ≤ a + 3 + q)) (Fin.last (a + 2))))) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
dsimp [Fin.cast, Fin.castLE, Fin.castLT]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ (Finset.sum Finset.univ fun i =>
          ((-1) ^ a * (-1) ^ ↑i) •
            φ ≫
              δ X { val := ↑i, isLt := (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc i) < a + 2 + q) } < n + 2) } ≫
                σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
        ((-1) ^ a * (-1) ^ (a + 1)) •
          φ ≫
            δ X
                { val := a + 1,
                  isLt := (_ : ↑{ val := a + 1, isLt := (_ : ↑(Fin.last (a + 1)) < a + 2 + q) } < n + 2) } ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) } +
      ((Finset.sum Finset.univ fun i =>
            ((-1) ^ ↑i * (-1) ^ (a + 1)) •
              φ ≫
                σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                  δ X
                    { val := ↑i,
                      isLt :=
                        (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc i)) < a + 3 + q) } < n + 3) }) +
          ((-1) ^ (a + 1) * (-1) ^ (a + 1)) •
            φ ≫
              σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                δ X
                  { val := a + 1,
                    isLt :=
                      (_ : ↑{ val := a + 1, isLt := (_ : ↑(↑Fin.castSucc (Fin.last (a + 1))) < a + 3 + q) } < n + 3) } +
        ((-1) ^ (a + 2) * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X
                { val := a + 2,
                  isLt := (_ : ↑{ val := a + 2, isLt := (_ : ↑(Fin.last (a + 2)) < a + 3 + q) } < n + 3) }) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ (Finset.sum Finset.univ fun i =>
          ((-1) ^ a * (-1) ^ ↑i) •
            φ ≫
              δ X { val := ↑i, isLt := (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc i) < a + 2 + q) } < n + 2) } ≫
                σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
        ((-1) ^ a * (-1) ^ (a + 1)) •
          φ ≫
            δ X
                { val := a + 1,
                  isLt := (_ : ↑{ val := a + 1, isLt := (_ : ↑(Fin.last (a + 1)) < a + 2 + q) } < n + 2) } ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) } +
      ((Finset.sum Finset.univ fun i =>
            ((-1) ^ ↑i * (-1) ^ (a + 1)) •
              φ ≫
                σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                  δ X
                    { val := ↑i,
                      isLt :=
                        (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc i)) < a + 3 + q) } < n + 3) }) +
          ((-1) ^ (a + 1) * (-1) ^ (a + 1)) •
            φ ≫
              σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                δ X
                  { val := a + 1,
                    isLt :=
                      (_ : ↑{ val := a + 1, isLt := (_ : ↑(↑Fin.castSucc (Fin.last (a + 1))) < a + 3 + q) } < n + 3) } +
        ((-1) ^ (a + 2) * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X
                { val := a + 2,
                  isLt := (_ : ↑{ val := a + 2, isLt := (_ : ↑(Fin.last (a + 2)) < a + 3 + q) } < n + 3) }) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
have simplif :
  ∀ a b c d e f : Y ⟶ X _[n + 1], b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f := by
  intro a b c d e f h1 h2 h3
  rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ a * (-1) ^ (a + 1)) •
      φ ≫
        δ X { val := a + 1, isLt := (_ : ↑{ val := a + 1, isLt := (_ : ↑(Fin.last (a + 1)) < a + 2 + q) } < n + 2) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }

case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ (a + 1) * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := a + 1,
                isLt :=
                  (_ : ↑{ val := a + 1, isLt := (_ : ↑(↑Fin.castSucc (Fin.last (a + 1))) < a + 3 + q) } < n + 3) } +
      ((-1) ^ (a + 2) * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := a + 2, isLt := (_ : ↑{ val := a + 2, isLt := (_ : ↑(Fin.last (a + 2)) < a + 3 + q) } < n + 3) } =
    0

case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ ↑i * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X
                { val := ↑i,
                  isLt :=
                    (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc i)) < a + 3 + q) } < n + 3) }) +
      Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑i) •
          φ ≫
            δ X { val := ↑i, isLt := (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc i) < a + 2 + q) } < n + 2) } ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) }) =
    0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ (Finset.sum Finset.univ fun i =>
          ((-1) ^ a * (-1) ^ ↑i) •
            φ ≫
              δ X { val := ↑i, isLt := (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc i) < a + 2 + q) } < n + 2) } ≫
                σ X { val := a, isLt := (_ : a < Nat.succ n) }) +
        ((-1) ^ a * (-1) ^ (a + 1)) •
          φ ≫
            δ X
                { val := a + 1,
                  isLt := (_ : ↑{ val := a + 1, isLt := (_ : ↑(Fin.last (a + 1)) < a + 2 + q) } < n + 2) } ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) } +
      ((Finset.sum Finset.univ fun i =>
            ((-1) ^ ↑i * (-1) ^ (a + 1)) •
              φ ≫
                σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                  δ X
                    { val := ↑i,
                      isLt :=
                        (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc i)) < a + 3 + q) } < n + 3) }) +
          ((-1) ^ (a + 1) * (-1) ^ (a + 1)) •
            φ ≫
              σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                δ X
                  { val := a + 1,
                    isLt :=
                      (_ : ↑{ val := a + 1, isLt := (_ : ↑(↑Fin.castSucc (Fin.last (a + 1))) < a + 3 + q) } < n + 3) } +
        ((-1) ^ (a + 2) * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X
                { val := a + 2,
                  isLt := (_ : ↑{ val := a + 2, isLt := (_ : ↑(Fin.last (a + 2)) < a + 3 + q) } < n + 3) }) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
apply simplif
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
d : ℕ
⊢ n + d = a + d + q
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
⊢ ∀ (d : ℕ), n + d = a + d + q
intro d
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
d : ℕ
⊢ n + d = a + d + q
rw [add_assoc, add_comm d, ← add_assoc, hnaq]
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) { val := k, isLt := hk }))) •
      (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) { val := k, isLt := hk }))) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
case hf
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) j))) •
        (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) j))) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) } =
      0
rintro ⟨k, hk⟩
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ φ ≫ δ X { val := a + 2 + k, isLt := (_ : a + 2 + k < n + 2) } = 0
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) { val := k, isLt := hk }))) •
      (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) { val := k, isLt := hk }))) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
suffices φ ≫ X.δ (⟨a + 2 + k, by linarith⟩ : Fin (n + 2)) = 0 by
  simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]
case h.e'_2.h.e'_7.h.e'_5.h.e'_2
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ a + 2 + k = ↑(Fin.succ { val := a + k + 1, isLt := (_ : a + k + 1 < n + 1) })
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ φ ≫ δ X { val := a + 2 + k, isLt := (_ : a + 2 + k < n + 2) } = 0
convert v ⟨a + k + 1, by linarith⟩ (by rw [Fin.val_mk] ; linarith)
case h.e'_2.h.e'_7.h.e'_5.h.e'_2
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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
case h.e'_2.h.e'_7.h.e'_5.h.e'_2
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ a + 2 + k = ↑(Fin.succ { val := a + k + 1, isLt := (_ : a + k + 1 < n + 1) })
dsimp
no goals
case h.e'_2.h.e'_7.h.e'_5.h.e'_2
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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
linarith
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ a + 2 + k < n + 2
linarith
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
this : φ ≫ δ X { val := a + 2 + k, isLt := (_ : a + 2 + k < n + 2) } = 0
⊢ ((-1) ^ a * (-1) ^ ↑(↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) { val := k, isLt := hk }))) •
      (φ ≫ δ X (↑(Fin.cast (_ : a + 2 + q = n + 2)) (↑(Fin.natAdd (a + 2)) { val := k, isLt := hk }))) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ a + k + 1 < n + 1
linarith
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 1 ≤ ↑{ val := a + k + 1, isLt := (_ : a + k + 1 < n + 1) } + q
rw [Fin.val_mk]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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
linarith
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })) * (-1) ^ (a + 1)) •
      (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
        δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })) =
    0
case hf
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) j)) * (-1) ^ (a + 1)) •
        (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
          δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) j)) =
      0
rintro ⟨k, hk⟩
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.succ { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } <
    ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })

case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.pred (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
      (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False) ≠
    0

case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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 (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
          (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False)) +
      q

case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.succ { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } <
    ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })

case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.succ { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } <
    ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ((-1) ^ ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })) * (-1) ^ (a + 1)) •
      (φ ≫ σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
        δ X (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })) =
    0
rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.pred (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
      (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False) ≠
    0

case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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 (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
          (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False)) +
      q
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.succ { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } <
    ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })

case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.pred (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
      (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False) ≠
    0

case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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 (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
          (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False)) +
      q

case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.succ { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } <
    ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })

case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.succ { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } <
    ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })
. simp only [Fin.lt_iff_val_lt_val]
  dsimp [Fin.natAdd, Fin.cast]
  linarith
case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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 (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
          (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False)) +
      q
case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.pred (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
      (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False) ≠
    0

case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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 (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
          (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False)) +
      q
. intro h
  rw [Fin.pred_eq_iff_eq_succ, Fin.ext_iff] at h
  dsimp [Fin.cast] at h
  linarith
no goals
case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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 (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
          (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False)) +
      q
. dsimp [Fin.cast, Fin.pred]
  rw [Nat.pred_eq_sub_one, Nat.succ_add_sub_one]
  linarith
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ↑(Fin.succ { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) <
    ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.succ { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } <
    ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })
simp only [Fin.lt_iff_val_lt_val]
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ↑(Fin.succ { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) <
    ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
dsimp [Fin.natAdd, Fin.cast]
no goals
case hf.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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
linarith
case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
h :
  Fin.pred (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
      (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False) =
    0
⊢ False
case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.pred (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
      (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False) ≠
    0
intro h
case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
h : ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })) = ↑(Fin.succ 0)
⊢ False
case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
h :
  Fin.pred (↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
      (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False) =
    0
⊢ False
rw [Fin.pred_eq_iff_eq_succ, Fin.ext_iff] at h
case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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
case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
h : ↑(↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk })) = ↑(Fin.succ 0)
⊢ False
dsimp [Fin.cast] at h
no goals
case hf.mk.hj₁
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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
linarith
case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 2 ≤ Nat.pred (a + 3 + k) + q
case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
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 (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }))
          (_ : ↑(Fin.cast (_ : a + 3 + q = n + 3)) (↑(Fin.natAdd (a + 3)) { val := k, isLt := hk }) = 0 → False)) +
      q
dsimp [Fin.cast, Fin.pred]
case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 2 ≤ a + 2 + k + q
case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 2 ≤ Nat.pred (a + 3 + k) + q
rw [Nat.pred_eq_sub_one, Nat.succ_add_sub_one]
no goals
case hf.mk.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 2 ≤ a + 2 + k + q
linarith
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e f : Y ⟶ X.obj [n + 1].op
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
⊢ a + b + (c + d + e) = f
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
intro a b c d e f h1 h2 h3
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e f : Y ⟶ X.obj [n + 1].op
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
⊢ a + b + (c + d + e) = f
rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ Odd (a + (a + 1))
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ a * (-1) ^ (a + 1)) •
      φ ≫
        δ X { val := a + 1, isLt := (_ : ↑{ val := a + 1, isLt := (_ : ↑(Fin.last (a + 1)) < a + 2 + q) } < n + 2) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
rw [← pow_add, Odd.neg_one_pow, neg_smul, one_zsmul]
no goals
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ Odd (a + (a + 1))
exact ⟨a, by linarith⟩
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ a + (a + 1) = 2 * a + 1
linarith
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ 𝟙 (X.obj [n + 1].op) +
      ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ 𝟙 (X.obj [n + 1].op) =
    0
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ (a + 1) * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := a + 1,
                isLt :=
                  (_ : ↑{ val := a + 1, isLt := (_ : ↑(↑Fin.castSucc (Fin.last (a + 1))) < a + 3 + q) } < n + 3) } +
      ((-1) ^ (a + 2) * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := a + 2, isLt := (_ : ↑{ val := a + 2, isLt := (_ : ↑(Fin.last (a + 2)) < a + 3 + q) } < n + 3) } =
    0
rw [X.δ_comp_σ_self' (Fin.castSucc_mk _ _ _).symm,
  X.δ_comp_σ_succ' (Fin.succ_mk _ _ _).symm]
no goals
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ 𝟙 (X.obj [n + 1].op) +
      ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ 𝟙 (X.obj [n + 1].op) =
    0
simp only [comp_id, pow_add _ (a + 1) 1, pow_one, mul_neg, mul_one, neg_mul, neg_smul,
  add_right_neg]
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ (Finset.sum Finset.univ fun x =>
      ((-1) ^ ↑x * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X
                { val := ↑x,
                  isLt := (_ : ↑{ val := ↑x, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc x)) < a + 3 + q) } < n + 3) } +
        ((-1) ^ a * (-1) ^ ↑x) •
          φ ≫
            δ X { val := ↑x, isLt := (_ : ↑{ val := ↑x, isLt := (_ : ↑(↑Fin.castSucc x) < a + 2 + q) } < n + 2) } ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) }) =
    0
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((Finset.sum Finset.univ fun i =>
        ((-1) ^ ↑i * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X
                { val := ↑i,
                  isLt :=
                    (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc i)) < a + 3 + q) } < n + 3) }) +
      Finset.sum Finset.univ fun i =>
        ((-1) ^ a * (-1) ^ ↑i) •
          φ ≫
            δ X { val := ↑i, isLt := (_ : ↑{ val := ↑i, isLt := (_ : ↑(↑Fin.castSucc i) < a + 2 + q) } < n + 2) } ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) }) =
    0
rw [← Finset.sum_add_distrib]
case a.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ∀ (x : Fin (a + 1)),
    x ∈ Finset.univ →
      ((-1) ^ ↑x * (-1) ^ (a + 1)) •
            φ ≫
              σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                δ X
                  { val := ↑x,
                    isLt :=
                      (_ : ↑{ val := ↑x, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc x)) < a + 3 + q) } < n + 3) } +
          ((-1) ^ a * (-1) ^ ↑x) •
            φ ≫
              δ X { val := ↑x, isLt := (_ : ↑{ val := ↑x, isLt := (_ : ↑(↑Fin.castSucc x) < a + 2 + q) } < n + 2) } ≫
                σ X { val := a, isLt := (_ : a < Nat.succ n) } =
        0
case a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ (Finset.sum Finset.univ fun x =>
      ((-1) ^ ↑x * (-1) ^ (a + 1)) •
          φ ≫
            σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
              δ X
                { val := ↑x,
                  isLt := (_ : ↑{ val := ↑x, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc x)) < a + 3 + q) } < n + 3) } +
        ((-1) ^ a * (-1) ^ ↑x) •
          φ ≫
            δ X { val := ↑x, isLt := (_ : ↑{ val := ↑x, isLt := (_ : ↑(↑Fin.castSucc x) < a + 2 + q) } < n + 2) } ≫
              σ X { val := a, isLt := (_ : a < Nat.succ n) }) =
    0
apply Finset.sum_eq_zero
case a.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ ((-1) ^ ↑{ val := i, isLt := hi } * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := ↑{ val := i, isLt := hi },
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc { val := i, isLt := hi })) < a + 3 + q) } <
                      n + 3) } +
      ((-1) ^ a * (-1) ^ ↑{ val := i, isLt := hi }) •
        φ ≫
          δ X
              { val := ↑{ val := i, isLt := hi },
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc { val := i, isLt := hi }) < a + 2 + q) } <
                      n + 2) } ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
case a.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ∀ (x : Fin (a + 1)),
    x ∈ Finset.univ →
      ((-1) ^ ↑x * (-1) ^ (a + 1)) •
            φ ≫
              σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
                δ X
                  { val := ↑x,
                    isLt :=
                      (_ : ↑{ val := ↑x, isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc x)) < a + 3 + q) } < n + 3) } +
          ((-1) ^ a * (-1) ^ ↑x) •
            φ ≫
              δ X { val := ↑x, isLt := (_ : ↑{ val := ↑x, isLt := (_ : ↑(↑Fin.castSucc x) < a + 2 + q) } < n + 2) } ≫
                σ X { val := a, isLt := (_ : a < Nat.succ n) } =
        0
rintro ⟨i, hi⟩ _
case a.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ ((-1) ^ i * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := i,
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc { val := i, isLt := hi })) < a + 3 + q) } <
                      n + 3) } +
      ((-1) ^ a * (-1) ^ i) •
        φ ≫
          δ X
              { val := i,
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc { val := i, isLt := hi }) < a + 2 + q) } <
                      n + 2) } ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
case a.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ ((-1) ^ ↑{ val := i, isLt := hi } * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := ↑{ val := i, isLt := hi },
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc { val := i, isLt := hi })) < a + 3 + q) } <
                      n + 3) } +
      ((-1) ^ a * (-1) ^ ↑{ val := i, isLt := hi }) •
        φ ≫
          δ X
              { val := ↑{ val := i, isLt := hi },
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc { val := i, isLt := hi }) < a + 2 + q) } <
                      n + 2) } ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
simp only
case a.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
hia : { val := i, isLt := (_ : i < n + 2) } ≤ ↑Fin.castSucc { val := a, isLt := (_ : a < n + 1) }
⊢ ((-1) ^ i * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := i,
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc { val := i, isLt := hi })) < a + 3 + q) } <
                      n + 3) } +
      ((-1) ^ a * (-1) ^ i) •
        φ ≫
          δ X
              { val := i,
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc { val := i, isLt := hi }) < a + 2 + q) } <
                      n + 2) } ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
case a.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ ((-1) ^ i * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := i,
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc { val := i, isLt := hi })) < a + 3 + q) } <
                      n + 3) } +
      ((-1) ^ a * (-1) ^ i) •
        φ ≫
          δ X
              { val := i,
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc { val := i, isLt := hi }) < a + 2 + q) } <
                      n + 2) } ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
have hia : (⟨i, by linarith⟩ : Fin (n + 2)) ≤
    Fin.castSucc (⟨a, by linarith⟩ : Fin (n + 1)) := by
  rw [Fin.le_iff_val_le_val]
  dsimp
  linarith
case a.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
hia : { val := i, isLt := (_ : i < n + 2) } ≤ ↑Fin.castSucc { val := a, isLt := (_ : a < n + 1) }
⊢ ((-1) ^ i * (-1) ^ (a + 1)) •
      φ ≫ δ X { val := i, isLt := (_ : i < n + 2) } ≫ σ X { val := a, isLt := (_ : a < n + 1) } =
    -((-1) ^ a * (-1) ^ i) •
      φ ≫
        δ X
            { val := i,
              isLt :=
                (_ :
                  ↑{ val := ↑{ val := i, isLt := hi },
                        isLt := (_ : ↑(↑Fin.castSucc { val := i, isLt := hi }) < a + 2 + q) } <
                    n + 2) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
case a.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
hia : { val := i, isLt := (_ : i < n + 2) } ≤ ↑Fin.castSucc { val := a, isLt := (_ : a < n + 1) }
⊢ ((-1) ^ i * (-1) ^ (a + 1)) •
        φ ≫
          σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) } ≫
            δ X
              { val := i,
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc (↑Fin.castSucc { val := i, isLt := hi })) < a + 3 + q) } <
                      n + 3) } +
      ((-1) ^ a * (-1) ^ i) •
        φ ≫
          δ X
              { val := i,
                isLt :=
                  (_ :
                    ↑{ val := ↑{ val := i, isLt := hi },
                          isLt := (_ : ↑(↑Fin.castSucc { val := i, isLt := hi }) < a + 2 + q) } <
                      n + 2) } ≫
            σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
erw [δ_comp_σ_of_le X hia, add_eq_zero_iff_eq_neg, ← neg_zsmul]
case a.h.mk.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
hia : { val := i, isLt := (_ : i < n + 2) } ≤ ↑Fin.castSucc { val := a, isLt := (_ : a < n + 1) }
⊢ (-1) ^ i * (-1) ^ (a + 1) = -((-1) ^ a * (-1) ^ i)
case a.h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
hia : { val := i, isLt := (_ : i < n + 2) } ≤ ↑Fin.castSucc { val := a, isLt := (_ : a < n + 1) }
⊢ ((-1) ^ i * (-1) ^ (a + 1)) •
      φ ≫ δ X { val := i, isLt := (_ : i < n + 2) } ≫ σ X { val := a, isLt := (_ : a < n + 1) } =
    -((-1) ^ a * (-1) ^ i) •
      φ ≫
        δ X
            { val := i,
              isLt :=
                (_ :
                  ↑{ val := ↑{ val := i, isLt := hi },
                        isLt := (_ : ↑(↑Fin.castSucc { val := i, isLt := hi }) < a + 2 + q) } <
                    n + 2) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
congr 2
no goals
case a.h.mk.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
hia : { val := i, isLt := (_ : i < n + 2) } ≤ ↑Fin.castSucc { val := a, isLt := (_ : a < n + 1) }
⊢ (-1) ^ i * (-1) ^ (a + 1) = -((-1) ^ a * (-1) ^ i)
ring
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ i < n + 2
linarith
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ a < n + 1
linarith
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ ↑{ val := i, isLt := (_ : i < n + 2) } ≤ ↑(↑Fin.castSucc { val := a, isLt := (_ : a < n + 1) })
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ { val := i, isLt := (_ : i < n + 2) } ≤ ↑Fin.castSucc { val := a, isLt := (_ : a < n + 1) }
rw [Fin.le_iff_val_le_val]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ i ≤ a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ ↑{ val := i, isLt := (_ : i < n + 2) } ≤ ↑(↑Fin.castSucc { val := a, isLt := (_ : a < n + 1) })
dsimp
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
simplif : ∀ (a b c d e f : Y ⟶ X.obj [n + 1].op), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
i : ℕ
hi : i < a + 1
a✝ : { val := i, isLt := hi } ∈ Finset.univ
⊢ i ≤ a
linarith