[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 2)
hj₁ : j ≠ 0
hj₂ : n + 2 ≤ ↑j + q
⊢ φ ≫ δ X j = 0
[PROOFSTEP]
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero hj₁
[GOAL]
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : Fin.succ i ≠ 0
hj₂ : n + 2 ≤ ↑(Fin.succ i) + q
⊢ φ ≫ δ X (Fin.succ i) = 0
[PROOFSTEP]
apply v i
[GOAL]
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : Fin.succ i ≠ 0
hj₂ : n + 2 ≤ ↑(Fin.succ i) + q
⊢ n + 1 ≤ ↑i + q
[PROOFSTEP]
simp only [Fin.val_succ] at hj₂
[GOAL]
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : Fin.succ i ≠ 0
hj₂ : n + 2 ≤ ↑i + 1 + q
⊢ n + 1 ≤ ↑i + q
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish (q + 1) φ
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ n + 1 ≤ ↑j + (q + 1)
[PROOFSTEP]
simpa only [← add_assoc] using le_add_right hj
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y Z : C
q n : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ (f ≫ φ) ≫ δ X (Fin.succ j) = 0
[PROOFSTEP]
rw [assoc, v j hj, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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) }
[PROOFSTEP]
have hnaq_shift : ∀ d : ℕ, n + d = a + d + q := by
  intro d
  rw [add_assoc, add_comm d, ← add_assoc, hnaq]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
⊢ ∀ (d : ℕ), n + d = a + d + q
[PROOFSTEP]
intro d
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
d : ℕ
⊢ n + d = a + d + q
[PROOFSTEP]
rw [add_assoc, add_comm d, ← add_assoc, hnaq]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) =
    -φ ≫
        δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
[PROOFSTEP]
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)]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1]) = X.obj (Opposite.op [n + 1])) +
        (((-1) ^ (a + 1) • σ X { val := a + 1, isLt := (_ : a + 1 < Nat.succ (n + 1)) }) ≫
            eqToHom (_ : X.obj (Opposite.op [n + 1 + 1]) = X.obj (Opposite.op [n + 2]))) ≫
          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) }
[PROOFSTEP]
simp only [AlternatingFaceMapComplex.obj_d_eq, eqToHom_refl, comp_id, comp_sum, sum_comp, comp_add]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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) }
[PROOFSTEP]
simp only [comp_zsmul, zsmul_comp, ← assoc, ← mul_zsmul]
  -- cleaning up the first sum
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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) }
[PROOFSTEP]
rw [← Fin.sum_congr' _ (hnaq_shift 2).symm, Fin.sum_trunc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) i))) •
          (φ ≫ δ X (↑(Fin.castIso (_ : 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_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.natAdd (a + 2) j))) •
        (φ ≫ δ X (↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.natAdd (a + 2) j))) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) } =
      0
[PROOFSTEP]
swap
[GOAL]
case hf
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.natAdd (a + 2) j))) •
        (φ ≫ δ X (↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.natAdd (a + 2) j))) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) } =
      0
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case hf.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ((-1) ^ a * (-1) ^ ↑(↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.natAdd (a + 2) { val := k, isLt := hk }))) •
      (φ ≫ δ X (↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.natAdd (a + 2) { val := k, isLt := hk }))) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
[PROOFSTEP]
suffices φ ≫ X.δ (⟨a + 2 + k, by linarith⟩ : Fin (n + 2)) = 0 by
  simp only [this, Fin.natAdd_mk, Fin.castIso_mk, zero_comp, smul_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [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
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.natAdd (a + 2) { val := k, isLt := hk }))) •
      (φ ≫ δ X (↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.natAdd (a + 2) { val := k, isLt := hk }))) ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
[PROOFSTEP]
simp only [this, Fin.natAdd_mk, Fin.castIso_mk, zero_comp, smul_zero]
[GOAL]
case hf.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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
[PROOFSTEP]
convert v ⟨a + k + 1, by linarith⟩ (by rw [Fin.val_mk]; linarith)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [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
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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
[PROOFSTEP]
rw [Fin.val_mk]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [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
[PROOFSTEP]
linarith
[GOAL]
case h.e'_2.h.e'_7.h.e'_5.h.e'_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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) })
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_2.h.e'_7.h.e'_5.h.e'_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [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
[PROOFSTEP]
linarith
  -- cleaning up the second sum
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) i))) •
          (φ ≫ δ X (↑(Fin.castIso (_ : 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) }
[PROOFSTEP]
rw [← Fin.sum_congr' _ (hnaq_shift 3).symm, @Fin.sum_trunc _ _ (a + 3)]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) i))) •
          (φ ≫ δ X (↑(Fin.castIso (_ : 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.castIso (_ : 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.castIso (_ : 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_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ ↑(↑(Fin.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) j)) =
      0
[PROOFSTEP]
swap
[GOAL]
case hf
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ ↑(↑(Fin.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) j)) =
      0
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case hf.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ ((-1) ^ ↑(↑(Fin.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk })) =
    0
[PROOFSTEP]
rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
[GOAL]
case hf.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk })
[PROOFSTEP]
simp only [Fin.lt_iff_val_lt_val]
[GOAL]
case hf.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk }))
[PROOFSTEP]
dsimp [Fin.natAdd, Fin.castIso]
[GOAL]
case hf.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [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
[PROOFSTEP]
linarith
[GOAL]
case hf.mk.hj₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ Fin.pred (↑(Fin.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk }))
      (_ : ↑(Fin.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk }) = 0 → False) ≠
    0
[PROOFSTEP]
intro h
[GOAL]
case hf.mk.hj₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [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.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk }))
      (_ : ↑(Fin.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk }) = 0 → False) =
    0
⊢ False
[PROOFSTEP]
rw [Fin.pred_eq_iff_eq_succ, Fin.ext_iff] at h
[GOAL]
case hf.mk.hj₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
h : ↑(↑(Fin.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk })) = ↑(Fin.succ 0)
⊢ False
[PROOFSTEP]
dsimp [Fin.castIso] at h
[GOAL]
case hf.mk.hj₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [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
[PROOFSTEP]
linarith
[GOAL]
case hf.mk.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 2 ≤
    ↑(Fin.pred (↑(Fin.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk }))
          (_ : ↑(Fin.castIso (_ : a + 3 + q = n + 3)) (Fin.natAdd (a + 3) { val := k, isLt := hk }) = 0 → False)) +
      q
[PROOFSTEP]
dsimp [Fin.castIso, Fin.pred]
[GOAL]
case hf.mk.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ n + 2 ≤ a + 3 + k - 1 + q
[PROOFSTEP]
rw [Nat.add_right_comm, Nat.add_sub_assoc (by norm_num : 1 ≤ 3)]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
k : ℕ
hk : k < q
⊢ 1 ≤ 3
[PROOFSTEP]
norm_num
[GOAL]
case hf.mk.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [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 + (3 - 1) + q
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) i))) •
          (φ ≫ δ X (↑(Fin.castIso (_ : 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.castIso (_ : 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.castIso (_ : 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) }
[PROOFSTEP]
simp only [assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x))) •
          φ ≫
            δ X (↑(Fin.castIso (_ : 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.castIso (_ : 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.castIso (_ : 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) }
[PROOFSTEP]
conv_lhs =>
  congr
  ·rw [Fin.sum_univ_castSucc]
  ·rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x))) •
        φ ≫
          δ X (↑(Fin.castIso (_ : 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.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.castLE (_ : a + 3 ≤ a + 3 + q) x))
[PROOFSTEP]
  congr
  ·rw [Fin.sum_univ_castSucc]
  ·rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x))) •
        φ ≫
          δ X (↑(Fin.castIso (_ : 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.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.castLE (_ : a + 3 ≤ a + 3 + q) x))
[PROOFSTEP]
  congr
  ·rw [Fin.sum_univ_castSucc]
  ·rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x))) •
        φ ≫
          δ X (↑(Fin.castIso (_ : 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.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.castLE (_ : a + 3 ≤ a + 3 + q) x))
[PROOFSTEP]
congr
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x))) •
      φ ≫
        δ X (↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x)) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| Finset.sum Finset.univ fun x =>
    ((-1) ^ ↑(↑(Fin.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.castLE (_ : a + 3 ≤ a + 3 + q) x))
[PROOFSTEP]
·rw [Fin.sum_univ_castSucc]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x))) •
      φ ≫
        δ X (↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x)) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
[PROOFSTEP]
rw [Fin.sum_univ_castSucc]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x))) •
      φ ≫
        δ X (↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x)) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
[PROOFSTEP]
rw [Fin.sum_univ_castSucc]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x))) •
      φ ≫
        δ X (↑(Fin.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) x)) ≫
          σ X { val := a, isLt := (_ : a < Nat.succ n) }
[PROOFSTEP]
rw [Fin.sum_univ_castSucc]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| Finset.sum Finset.univ fun x =>
    ((-1) ^ ↑(↑(Fin.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.castLE (_ : a + 3 ≤ a + 3 + q) x))
[PROOFSTEP]
·rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| Finset.sum Finset.univ fun x =>
    ((-1) ^ ↑(↑(Fin.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.castLE (_ : a + 3 ≤ a + 3 + q) x))
[PROOFSTEP]
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| Finset.sum Finset.univ fun x =>
    ((-1) ^ ↑(↑(Fin.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.castLE (_ : a + 3 ≤ a + 3 + q) x))
[PROOFSTEP]
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
| Finset.sum Finset.univ fun x =>
    ((-1) ^ ↑(↑(Fin.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3)) (Fin.castLE (_ : a + 3 ≤ a + 3 + q) x))
[PROOFSTEP]
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) (Fin.castSucc i)))) •
            φ ≫
              δ X (↑(Fin.castIso (_ : 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.castIso (_ : a + 2 + q = n + 2)) (Fin.castLE (_ : a + 2 ≤ a + 2 + q) (Fin.last (a + 1))))) •
          φ ≫
            δ X (↑(Fin.castIso (_ : 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.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3))
                      (Fin.castLE (_ : a + 3 ≤ a + 3 + q) (Fin.castSucc (Fin.castSucc i))))) +
          ((-1) ^
                ↑(↑(Fin.castIso (_ : 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.castIso (_ : a + 3 + q = n + 3))
                    (Fin.castLE (_ : a + 3 ≤ a + 3 + q) (Fin.castSucc (Fin.last (a + 1))))) +
        ((-1) ^ ↑(↑(Fin.castIso (_ : 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.castIso (_ : 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) }
[PROOFSTEP]
dsimp [Fin.castIso, Fin.castLE, Fin.castLT]
  /- the purpose of the following `simplif` is to create three subgoals in order
        to finish the proof -/
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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) }
[PROOFSTEP]
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]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (a b c d e f : Y ⟶ X.obj (Opposite.op [n + 1])), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
[PROOFSTEP]
intro a b c d e f h1 h2 h3
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e f : Y ⟶ X.obj (Opposite.op [n + 1])
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
⊢ a + b + (c + d + e) = f
[PROOFSTEP]
rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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) }
[PROOFSTEP]
apply simplif
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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) }
[PROOFSTEP]
rw [← pow_add, Odd.neg_one_pow, neg_smul, one_zsmul]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ Odd (a + (a + 1))
[PROOFSTEP]
exact ⟨a, by linarith⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ a + (a + 1) = 2 * a + 1
[PROOFSTEP]
linarith
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
rw [X.δ_comp_σ_self' (Fin.castSucc_mk _ _ _).symm, X.δ_comp_σ_succ' (Fin.succ_mk _ _ _).symm]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ 𝟙 (X.obj (Opposite.op [n + 1])) +
      ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ 𝟙 (X.obj (Opposite.op [n + 1])) =
    0
[PROOFSTEP]
simp only [comp_id, pow_add _ (a + 1) 1, pow_one, mul_neg, mul_one, neg_mul, neg_smul, add_right_neg]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
rw [← Finset.sum_add_distrib]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
apply Finset.sum_eq_zero
[GOAL]
case a.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
rintro ⟨i, hi⟩ _
[GOAL]
case a.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
simp only
[GOAL]
case a.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
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
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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) }
[PROOFSTEP]
rw [Fin.le_iff_val_le_val]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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) })
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
linarith
[GOAL]
case a.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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
[PROOFSTEP]
erw [δ_comp_σ_of_le X hia, add_eq_zero_iff_eq_neg, ← neg_zsmul]
[GOAL]
case a.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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) }
[PROOFSTEP]
congr 2
[GOAL]
case a.h.mk.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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 (Opposite.op [n + 1])), 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)
[PROOFSTEP]
ring
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
[PROOFSTEP]
simp only [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl)]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫
      (HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 1) n ≫
          hσ' q n (n + 1) (_ : ComplexShape.Rel c (n + 1) n) +
        hσ' q (n + 1) (n + 2) (_ : ComplexShape.Rel c (n + 2) (n + 1)) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1)) =
    0
[PROOFSTEP]
rw [hσ'_eq_zero hqn (c_mk (n + 1) n rfl), comp_zero, zero_add]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫
      hσ' q (n + 1) (n + 2) (_ : ComplexShape.Rel c (n + 2) (n + 1)) ≫
        HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1) =
    0
[PROOFSTEP]
by_cases hqn' : n + 1 < q
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : n + 1 < q
⊢ φ ≫
      hσ' q (n + 1) (n + 2) (_ : ComplexShape.Rel c (n + 2) (n + 1)) ≫
        HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1) =
    0
[PROOFSTEP]
rw [hσ'_eq_zero hqn' (c_mk (n + 2) (n + 1) rfl), zero_comp, comp_zero]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫
      hσ' q (n + 1) (n + 2) (_ : ComplexShape.Rel c (n + 2) (n + 1)) ≫
        HomologicalComplex.d (AlternatingFaceMapComplex.obj X) (n + 2) (n + 1) =
    0
[PROOFSTEP]
simp only [hσ'_eq (show n + 1 = 0 + q by linarith) (c_mk (n + 2) (n + 1) rfl), pow_zero, Fin.mk_zero, one_zsmul,
  eqToHom_refl, comp_id, comp_sum, AlternatingFaceMapComplex.obj_d_eq]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ n + 1 = 0 + q
[PROOFSTEP]
linarith
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ (Finset.sum Finset.univ fun j => φ ≫ σ X 0 ≫ ((-1) ^ ↑j • δ X j)) = 0
[PROOFSTEP]
rw [← Fin.sum_congr' _ (show 2 + (n + 1) = n + 1 + 2 by linarith), Fin.sum_trunc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ 2 + (n + 1) = n + 1 + 2
[PROOFSTEP]
linarith
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ (Finset.sum Finset.univ fun i =>
      φ ≫
        σ X 0 ≫
          ((-1) ^ ↑(↑(Fin.castIso (_ : 2 + (n + 1) = n + 1 + 2)) (Fin.castLE (_ : 2 ≤ 2 + (n + 1)) i)) •
            δ X (↑(Fin.castIso (_ : 2 + (n + 1) = n + 1 + 2)) (Fin.castLE (_ : 2 ≤ 2 + (n + 1)) i)))) =
    0
[PROOFSTEP]
simp only [Fin.sum_univ_castSucc, Fin.sum_univ_zero, zero_add, Fin.last, Fin.castLE_mk, Fin.castIso_mk, Fin.castSucc_mk]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫ σ X 0 ≫ ((-1) ^ 0 • δ X { val := 0, isLt := (_ : 0 < n + 1 + 2) }) +
      φ ≫ σ X 0 ≫ ((-1) ^ 1 • δ X { val := 1, isLt := (_ : 1 < n + 1 + 2) }) =
    0
[PROOFSTEP]
simp only [Fin.mk_zero, Fin.val_zero, pow_zero, one_zsmul, Fin.mk_one, Fin.val_one, pow_one, neg_smul, comp_neg]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫ σ X 0 ≫ δ X 0 + -φ ≫ σ X 0 ≫ δ X 1 = 0
[PROOFSTEP]
erw [δ_comp_σ_self, δ_comp_σ_succ, add_right_neg]
[GOAL]
case neg.hf
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ ∀ (j : Fin (n + 1)),
    φ ≫
        σ X 0 ≫
          ((-1) ^ ↑(↑(Fin.castIso (_ : 2 + (n + 1) = n + 1 + 2)) (Fin.natAdd 2 j)) •
            δ X (↑(Fin.castIso (_ : 2 + (n + 1) = n + 1 + 2)) (Fin.natAdd 2 j))) =
      0
[PROOFSTEP]
intro j
[GOAL]
case neg.hf
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ φ ≫
      σ X 0 ≫
        ((-1) ^ ↑(↑(Fin.castIso (_ : 2 + (n + 1) = n + 1 + 2)) (Fin.natAdd 2 j)) •
          δ X (↑(Fin.castIso (_ : 2 + (n + 1) = n + 1 + 2)) (Fin.natAdd 2 j))) =
    0
[PROOFSTEP]
dsimp [Fin.castIso, Fin.castLE, Fin.castLT]
[GOAL]
case neg.hf
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ φ ≫ σ X 0 ≫ ((-1) ^ (2 + ↑j) • δ X { val := 2 + ↑j, isLt := (_ : ↑(Fin.natAdd 2 j) < n + 1 + 2) }) = 0
[PROOFSTEP]
rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
[GOAL]
case neg.hf.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ Fin.succ 0 < { val := 2 + ↑j, isLt := (_ : ↑(Fin.natAdd 2 j) < n + 1 + 2) }
[PROOFSTEP]
simp only [Fin.lt_iff_val_lt_val]
[GOAL]
case neg.hf.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ ↑(Fin.succ 0) < 2 + ↑j
[PROOFSTEP]
dsimp [Fin.succ]
[GOAL]
case neg.hf.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ 0 + 1 < 2 + ↑j
[PROOFSTEP]
linarith
[GOAL]
case neg.hf.hj₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ Fin.pred { val := 2 + ↑j, isLt := (_ : ↑(Fin.natAdd 2 j) < n + 1 + 2) }
      (_ : { val := 2 + ↑j, isLt := (_ : ↑(Fin.natAdd 2 j) < n + 1 + 2) } = 0 → False) ≠
    0
[PROOFSTEP]
intro h
[GOAL]
case neg.hf.hj₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
h :
  Fin.pred { val := 2 + ↑j, isLt := (_ : ↑(Fin.natAdd 2 j) < n + 1 + 2) }
      (_ : { val := 2 + ↑j, isLt := (_ : ↑(Fin.natAdd 2 j) < n + 1 + 2) } = 0 → False) =
    0
⊢ False
[PROOFSTEP]
simp only [Fin.pred, Fin.subNat, Fin.ext_iff, Nat.succ_add_sub_one, Fin.val_zero, add_eq_zero, false_and] at h
[GOAL]
case neg.hf.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤
    ↑(Fin.pred { val := 2 + ↑j, isLt := (_ : ↑(Fin.natAdd 2 j) < n + 1 + 2) }
          (_ : { val := 2 + ↑j, isLt := (_ : ↑(Fin.natAdd 2 j) < n + 1 + 2) } = 0 → False)) +
      q
[PROOFSTEP]
simp only [Fin.pred, Fin.subNat, Nat.pred_eq_sub_one, Nat.succ_add_sub_one]
[GOAL]
case neg.hf.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤ 1 + ↑j + q
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
⊢ HigherFacesVanish (q + 1) (φ ≫ HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q) (n + 1))
[PROOFSTEP]
intro j hj₁
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ (φ ≫ HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ (φ ≫ (𝟙 (X.obj (Opposite.op [n + 1])) + HomologicalComplex.Hom.f (Hσ q) (n + 1))) ≫ δ X (Fin.succ j) = 0
[PROOFSTEP]
simp only [comp_add, add_comp, comp_id]
  -- when n < q, the result follows immediately from the assumption
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
[PROOFSTEP]
by_cases hqn : n < q
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : n < q
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
[PROOFSTEP]
rw [v.comp_Hσ_eq_zero hqn, zero_comp, add_zero, v j (by linarith)]
  -- we now assume that n≥q, and write n=a+q
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : n < q
⊢ n + 1 ≤ ↑j + q
[PROOFSTEP]
linarith
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
[PROOFSTEP]
cases' Nat.le.dest (not_lt.mp hqn) with a ha
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
[PROOFSTEP]
rw [v.comp_Hσ_eq (show n = a + q by linarith), neg_comp, add_neg_eq_zero, assoc, assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ n = a + q
[PROOFSTEP]
linarith
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) } ≫ δ X (Fin.succ j)
[PROOFSTEP]
cases' n with m hm
[GOAL]
case neg.intro.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.zero + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.zero + 1)
hj₁ : Nat.zero + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.zero < q
ha : q + a = Nat.zero
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.zero + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ Nat.zero) } ≫ δ X (Fin.succ j)
[PROOFSTEP]
simp only [Nat.eq_zero_of_add_eq_zero_left ha, Fin.eq_zero j, Fin.mk_zero, Fin.mk_one, δ_comp_σ_succ, comp_id]
[GOAL]
case neg.intro.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.zero + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.zero + 1)
hj₁ : Nat.zero + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.zero < q
ha : q + a = Nat.zero
⊢ φ ≫ δ X (Fin.succ 0) = φ ≫ δ X { val := 0 + 1, isLt := (_ : 0 + 1 < Nat.zero + 2) }
[PROOFSTEP]
rfl
  -- in the other case, we need to write n as m+1
    -- then, we first consider the particular case j = a
[GOAL]
case neg.intro.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
[PROOFSTEP]
by_cases hj₂ : a = (j : ℕ)
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : a = ↑j
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
[PROOFSTEP]
simp only [hj₂, Fin.eta, δ_comp_σ_succ, comp_id]
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : a = ↑j
⊢ φ ≫ δ X (Fin.succ j) = φ ≫ δ X { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ m + 2) }
[PROOFSTEP]
rfl
  -- now, we assume j ≠ a (i.e. a < j)
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
[PROOFSTEP]
have haj : a < j := (Ne.le_iff_lt hj₂).mp (by linarith)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
⊢ a ≤ ↑j
[PROOFSTEP]
linarith
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
[PROOFSTEP]
have hj₃ := j.is_lt
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
[PROOFSTEP]
have ham : a ≤ m := by
  by_contra h
  rw [not_le, ← Nat.succ_le_iff] at h
  linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
⊢ a ≤ m
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
h : ¬a ≤ m
⊢ False
[PROOFSTEP]
rw [not_le, ← Nat.succ_le_iff] at h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
h : Nat.succ m ≤ a
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
[PROOFSTEP]
rw [X.δ_comp_σ_of_gt', j.pred_succ]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j
[PROOFSTEP]
swap
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j
[PROOFSTEP]
rw [Fin.lt_iff_val_lt_val]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ ↑(Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }) < ↑(Fin.succ j)
[PROOFSTEP]
simpa only [Fin.val_mk, Fin.val_succ, add_lt_add_iff_right] using haj
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
[PROOFSTEP]
obtain _ | ham'' := ham.lt_or_eq
[GOAL]
case neg.inl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
[PROOFSTEP]
rw [← X.δ_comp_δ''_assoc]
[GOAL]
case neg.inl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X
            (Fin.castLT { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) }
              (_ : ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } < m + 2)) ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
case neg.inl.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≤ Fin.castSucc j
[PROOFSTEP]
swap
[GOAL]
case neg.inl.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≤ Fin.castSucc j
[PROOFSTEP]
rw [Fin.le_iff_val_le_val]
[GOAL]
case neg.inl.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≤ ↑(Fin.castSucc j)
[PROOFSTEP]
dsimp
[GOAL]
case neg.inl.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ a + 1 ≤ ↑j
[PROOFSTEP]
linarith
[GOAL]
case neg.inl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X
            (Fin.castLT { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) }
              (_ : ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } < m + 2)) ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
[PROOFSTEP]
simp only [← assoc, v j (by linarith), zero_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ Nat.succ m + 1 ≤ ↑j + q
[PROOFSTEP]
linarith
[GOAL]
case neg.inr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
[PROOFSTEP]
rw [X.δ_comp_δ_self'_assoc]
[GOAL]
case neg.inr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
case neg.inr.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } = Fin.castSucc j
[PROOFSTEP]
swap
[GOAL]
case neg.inr.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } = Fin.castSucc j
[PROOFSTEP]
ext
[GOAL]
case neg.inr.H.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } = ↑(Fin.castSucc j)
[PROOFSTEP]
dsimp
[GOAL]
case neg.inr.H.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ a + 1 = ↑j
[PROOFSTEP]
linarith
[GOAL]
case neg.inr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
[PROOFSTEP]
simp only [← assoc, v j (by linarith), zero_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj (Opposite.op [Nat.succ m + 1])
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ Nat.succ m + 1 ≤ ↑j + q
[PROOFSTEP]
linarith