[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
⊢ objD X (n + 1) ≫ objD X n = 0
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
⊢ (∑ i : Fin (n + 1 + 2), (-1) ^ ↑i • SimplicialObject.δ X i) ≫ ∑ i : Fin (n + 2), (-1) ^ ↑i • SimplicialObject.δ X i =
    0
[PROOFSTEP]
simp only [comp_sum, sum_comp, ← Finset.sum_product']
  -- then, we decompose the index set P into a subset S and its complement Sᶜ
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
⊢ ∑ x in Finset.univ ×ˢ Finset.univ,
      ((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst) =
    0
[PROOFSTEP]
let P := Fin (n + 2) × Fin (n + 3)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
⊢ ∑ x in Finset.univ ×ˢ Finset.univ,
      ((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst) =
    0
[PROOFSTEP]
let S := Finset.univ.filter fun ij : P => (ij.2 : ℕ) ≤ (ij.1 : ℕ)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
⊢ ∑ x in Finset.univ ×ˢ Finset.univ,
      ((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst) =
    0
[PROOFSTEP]
erw [← Finset.sum_add_sum_compl S, ← eq_neg_iff_add_eq_zero, ← Finset.sum_neg_distrib]
  /- we are reduced to showing that two sums are equal, and this is obtained
      by constructing a bijection φ : S -> Sᶜ, which maps (i,j) to (j,i+1),
      and by comparing the terms -/
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
⊢ ∑ i in S, ((-1) ^ ↑i.snd • SimplicialObject.δ X i.snd) ≫ ((-1) ^ ↑i.fst • SimplicialObject.δ X i.fst) =
    ∑ x in Sᶜ, -((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst)
[PROOFSTEP]
let φ : ∀ ij : P, ij ∈ S → P := fun ij hij =>
  (Fin.castLT ij.2 (lt_of_le_of_lt (Finset.mem_filter.mp hij).right (Fin.is_lt ij.1)), ij.1.succ)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∑ i in S, ((-1) ^ ↑i.snd • SimplicialObject.δ X i.snd) ≫ ((-1) ^ ↑i.fst • SimplicialObject.δ X i.fst) =
    ∑ x in Sᶜ, -((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst)
[PROOFSTEP]
apply Finset.sum_bij φ
[GOAL]
case hi
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ
[PROOFSTEP]
intro ij hij
[GOAL]
case hi
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
ij : P
hij : ij ∈ S
⊢ φ ij hij ∈ Sᶜ
[PROOFSTEP]
simp only [Finset.mem_univ, Finset.compl_filter, Finset.mem_filter, true_and_iff, Fin.val_succ, Fin.coe_castLT] at hij ⊢
[GOAL]
case hi
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
ij : P
hij : ↑ij.snd ≤ ↑ij.fst
⊢ ¬↑ij.fst + 1 ≤ ↑ij.snd
[PROOFSTEP]
linarith
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (a : P) (ha : a ∈ S),
    ((-1) ^ ↑a.snd • SimplicialObject.δ X a.snd) ≫ ((-1) ^ ↑a.fst • SimplicialObject.δ X a.fst) =
      -((-1) ^ ↑(φ a ha).snd • SimplicialObject.δ X (φ a ha).snd) ≫
          ((-1) ^ ↑(φ a ha).fst • SimplicialObject.δ X (φ a ha).fst)
[PROOFSTEP]
rintro ⟨i, j⟩ hij
[GOAL]
case h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑(i, j).snd • SimplicialObject.δ X (i, j).snd) ≫ ((-1) ^ ↑(i, j).fst • SimplicialObject.δ X (i, j).fst) =
    -((-1) ^ ↑(φ (i, j) hij).snd • SimplicialObject.δ X (φ (i, j) hij).snd) ≫
        ((-1) ^ ↑(φ (i, j) hij).fst • SimplicialObject.δ X (φ (i, j) hij).fst)
[PROOFSTEP]
dsimp
[GOAL]
case h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑j • SimplicialObject.δ X j) ≫ ((-1) ^ ↑i • SimplicialObject.δ X i) =
    -((-1) ^ ↑(Fin.succ i) • SimplicialObject.δ X (Fin.succ i)) ≫
        ((-1) ^ ↑j • SimplicialObject.δ X (Fin.castLT j (_ : ↑j < n + 2)))
[PROOFSTEP]
simp only [zsmul_comp, comp_zsmul, smul_smul, ← neg_smul]
[GOAL]
case h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑i * (-1) ^ ↑j) • SimplicialObject.δ X j ≫ SimplicialObject.δ X i =
    -((-1) ^ ↑j * (-1) ^ ↑(Fin.succ i)) •
      SimplicialObject.δ X (Fin.succ i) ≫ SimplicialObject.δ X (Fin.castLT j (_ : ↑j < n + 2))
[PROOFSTEP]
congr 1
[GOAL]
case h.mk.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = -((-1) ^ ↑j * (-1) ^ ↑(Fin.succ i))
[PROOFSTEP]
simp only [Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
[GOAL]
case h.mk.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = (-1) ^ ↑j * (-1) ^ ↑i
[PROOFSTEP]
apply mul_comm
[GOAL]
case h.mk.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ SimplicialObject.δ X j ≫ SimplicialObject.δ X i =
    SimplicialObject.δ X (Fin.succ i) ≫ SimplicialObject.δ X (Fin.castLT j (_ : ↑j < n + 2))
[PROOFSTEP]
rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
[GOAL]
case h.mk.e_a.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ j ≤ Fin.castSucc i
[PROOFSTEP]
simpa using hij
[GOAL]
case i_inj
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (a₁ a₂ : P) (ha₁ : a₁ ∈ S) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂
[PROOFSTEP]
rintro ⟨i, j⟩ ⟨i', j'⟩ hij hij' h
[GOAL]
case i_inj.mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ (i, j) = (i', j')
[PROOFSTEP]
rw [Prod.mk.inj_iff]
[GOAL]
case i_inj.mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i' ∧ j = j'
[PROOFSTEP]
exact
  ⟨by simpa using congr_arg Prod.snd h, by
    simpa [Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i'
[PROOFSTEP]
simpa using congr_arg Prod.snd h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ j = j'
[PROOFSTEP]
simpa [Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)
[GOAL]
case i_surj
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (b : P), b ∈ Sᶜ → ∃ a ha, b = φ a ha
[PROOFSTEP]
rintro ⟨i', j'⟩ hij'
[GOAL]
case i_surj.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ Sᶜ
⊢ ∃ a ha, (i', j') = φ a ha
[PROOFSTEP]
simp only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.compl_filter, not_le, Finset.mem_filter,
  true_and] at hij' 
[GOAL]
case i_surj.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ ∃ a ha, (i', j') = φ a ha
[PROOFSTEP]
refine' ⟨(j'.pred <| _, Fin.castSucc i'), _, _⟩
[GOAL]
case i_surj.mk.refine'_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ j' ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case i_surj.mk.refine'_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
hij' : ↑i' < ↑0
⊢ False
[PROOFSTEP]
simp only [Fin.val_zero, not_lt_zero'] at hij' 
[GOAL]
case i_surj.mk.refine'_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (Fin.pred j' (_ : j' = 0 → False), Fin.castSucc i') ∈ S
[PROOFSTEP]
simpa only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.mem_filter, Fin.coe_castSucc,
  Fin.coe_pred, true_and] using Nat.le_pred_of_lt hij'
[GOAL]
case i_surj.mk.refine'_3
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (i', j') =
    φ (Fin.pred j' (_ : j' = 0 → False), Fin.castSucc i') (_ : (Fin.pred j' (_ : j' = 0 → False), Fin.castSucc i') ∈ S)
[PROOFSTEP]
simp only [Fin.castLT_castSucc, Fin.succ_pred]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ Y X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.d (obj X) (n + 1) n = ∑ i : Fin (n + 2), (-1) ^ ↑i • SimplicialObject.δ X i
[PROOFSTEP]
apply ChainComplex.of_d
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.114443, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ (fun n => NatTrans.app f (op [n])) (n + 1) ≫ objD Y n = objD X n ≫ (fun n => NatTrans.app f (op [n])) n
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.114443, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ NatTrans.app f (op [n + 1]) ≫ ∑ i : Fin (n + 2), (-1) ^ ↑i • SimplicialObject.δ Y i =
    (∑ i : Fin (n + 2), (-1) ^ ↑i • SimplicialObject.δ X i) ≫ NatTrans.app f (op [n])
[PROOFSTEP]
rw [comp_sum, sum_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.114443, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ ∑ j : Fin (n + 2), NatTrans.app f (op [n + 1]) ≫ ((-1) ^ ↑j • SimplicialObject.δ Y j) =
    ∑ j : Fin (n + 2), ((-1) ^ ↑j • SimplicialObject.δ X j) ≫ NatTrans.app f (op [n])
[PROOFSTEP]
refine' Finset.sum_congr rfl fun _ _ => _
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.114443, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ NatTrans.app f (op [n + 1]) ≫ ((-1) ^ ↑x✝¹ • SimplicialObject.δ Y x✝¹) =
    ((-1) ^ ↑x✝¹ • SimplicialObject.δ X x✝¹) ≫ NatTrans.app f (op [n])
[PROOFSTEP]
rw [comp_zsmul, zsmul_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.114443, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ (-1) ^ ↑x✝¹ • NatTrans.app f (op [n + 1]) ≫ SimplicialObject.δ Y x✝¹ =
    (-1) ^ ↑x✝¹ • SimplicialObject.δ X x✝¹ ≫ NatTrans.app f (op [n])
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u_1
inst✝¹ : Category.{?u.114443, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ NatTrans.app f (op [n + 1]) ≫ SimplicialObject.δ Y x✝¹ = SimplicialObject.δ X x✝¹ ≫ NatTrans.app f (op [n])
[PROOFSTEP]
symm
[GOAL]
case e_a
C : Type u_1
inst✝¹ : Category.{?u.114443, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ SimplicialObject.δ X x✝¹ ≫ NatTrans.app f (op [n]) = NatTrans.app f (op [n + 1]) ≫ SimplicialObject.δ Y x✝¹
[PROOFSTEP]
apply f.naturality
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.d ((alternatingFaceMapComplex C).obj X) (n + 1) n = AlternatingFaceMapComplex.objD X n
[PROOFSTEP]
dsimp only [alternatingFaceMapComplex, AlternatingFaceMapComplex.obj]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.d
      (ChainComplex.of (fun n => X.obj (op [n])) (AlternatingFaceMapComplex.objD X)
        (_ : ∀ (n : ℕ), AlternatingFaceMapComplex.objD X (n + 1) ≫ AlternatingFaceMapComplex.objD X n = 0))
      (n + 1) n =
    AlternatingFaceMapComplex.objD X n
[PROOFSTEP]
apply ChainComplex.of_d
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
⊢ alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ) =
    (SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D
[PROOFSTEP]
apply CategoryTheory.Functor.ext
[GOAL]
case h_map
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
⊢ autoParam
    (∀ (X Y : SimplicialObject C) (f : X ⟶ Y),
      (alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫
            eqToHom
              (_ :
                ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj Y =
                  (alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case h_map
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
X Y : SimplicialObject C
f : X ⟶ Y
⊢ (alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫
        eqToHom
          (_ :
            ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj Y =
              (alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj Y)
[PROOFSTEP]
ext n
[GOAL]
case h_map.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ HomologicalComplex.Hom.f ((alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map f)
      n =
    HomologicalComplex.Hom.f
      (eqToHom (_ : ?F.obj X = ?G.obj X) ≫
        ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫
          eqToHom
            (_ :
              ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj Y =
                (alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj Y))
      n
[PROOFSTEP]
simp only [Functor.comp_map, HomologicalComplex.comp_f, alternatingFaceMapComplex_map_f,
  Functor.mapHomologicalComplex_map_f, HomologicalComplex.eqToHom_f, eqToHom_refl, comp_id, id_comp,
  SimplicialObject.whiskering_obj_map_app]
[GOAL]
case h_obj
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
⊢ ∀ (X : SimplicialObject C),
    (alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X =
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
X : SimplicialObject C
⊢ (alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X =
    ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X
[PROOFSTEP]
apply HomologicalComplex.ext
[GOAL]
case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
X : SimplicialObject C
⊢ ∀ (i j : ℕ),
    ComplexShape.Rel (ComplexShape.down ℕ) i j →
      HomologicalComplex.d ((alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
            i j ≫
          eqToHom
            (_ :
              HomologicalComplex.X
                  ((alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) j =
                HomologicalComplex.X (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X)
                  j) =
        eqToHom
            (_ :
              HomologicalComplex.X
                  ((alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) i =
                HomologicalComplex.X (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X)
                  i) ≫
          HomologicalComplex.d (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X) i j
[PROOFSTEP]
rintro i j (rfl : j + 1 = i)
[GOAL]
case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
X : SimplicialObject C
j : ℕ
⊢ HomologicalComplex.d ((alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
        (j + 1) j ≫
      eqToHom
        (_ :
          HomologicalComplex.X
              ((alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) j =
            HomologicalComplex.X (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X) j) =
    eqToHom
        (_ :
          HomologicalComplex.X
              ((alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) (j + 1) =
            HomologicalComplex.X (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X)
              (j + 1)) ≫
      HomologicalComplex.d (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X) (j + 1) j
[PROOFSTEP]
dsimp only [Functor.comp_obj]
[GOAL]
case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
X : SimplicialObject C
j : ℕ
⊢ HomologicalComplex.d
        ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj ((alternatingFaceMapComplex C).obj X)) (j + 1) j ≫
      eqToHom
        (_ :
          HomologicalComplex.X
              ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj ((alternatingFaceMapComplex C).obj X)) j =
            HomologicalComplex.X ((alternatingFaceMapComplex D).obj (((SimplicialObject.whiskering C D).obj F).obj X))
              j) =
    eqToHom
        (_ :
          HomologicalComplex.X
              ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj ((alternatingFaceMapComplex C).obj X))
              (j + 1) =
            HomologicalComplex.X ((alternatingFaceMapComplex D).obj (((SimplicialObject.whiskering C D).obj F).obj X))
              (j + 1)) ≫
      HomologicalComplex.d ((alternatingFaceMapComplex D).obj (((SimplicialObject.whiskering C D).obj F).obj X)) (j + 1)
        j
[PROOFSTEP]
simp only [Functor.mapHomologicalComplex_obj_d, alternatingFaceMapComplex_obj_d, eqToHom_refl, id_comp, comp_id,
  AlternatingFaceMapComplex.objD, Functor.map_sum, Functor.map_zsmul]
[GOAL]
case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
X : SimplicialObject C
j : ℕ
⊢ ∑ x : Fin (j + 2), (-1) ^ ↑x • F.map (SimplicialObject.δ X x) =
    ∑ i : Fin (j + 2), (-1) ^ ↑i • SimplicialObject.δ (((SimplicialObject.whiskering C D).obj F).obj X) i
[PROOFSTEP]
rfl
[GOAL]
case h_obj.h_X
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
X : SimplicialObject C
⊢ ((alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X).X =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X
[PROOFSTEP]
ext n
[GOAL]
case h_obj.h_X.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : Functor.Additive F
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.X ((alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) n =
    HomologicalComplex.X (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X) n
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n).f =
    NatTrans.app P.p (op [n + 1]) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n).f =
    NatTrans.app P.p (op [n + 1]) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n
[PROOFSTEP]
simp only [AlternatingFaceMapComplex.obj_d_eq, Karoubi.sum_hom, Preadditive.comp_sum, Karoubi.zsmul_hom,
  Preadditive.comp_zsmul]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ∑ x : Fin (n + 2), (-1) ^ ↑x • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • NatTrans.app P.p (op [n + 1]) ≫ SimplicialObject.δ P.X x
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{?u.208144, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X ⟶
    (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C).obj X
[PROOFSTEP]
refine' (ChainComplex.toSingle₀Equiv _ _).symm _
[GOAL]
C : Type u_1
inst✝² : Category.{?u.208144, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ { f // HomologicalComplex.d ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X) 1 0 ≫ f = 0 }
[PROOFSTEP]
refine' ⟨X.hom.app (op [0]), _⟩
[GOAL]
C : Type u_1
inst✝² : Category.{?u.208144, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ HomologicalComplex.d ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X) 1 0 ≫
      NatTrans.app X.hom (op [0]) =
    0
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.208144, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ HomologicalComplex.d ((alternatingFaceMapComplex C).obj X.left) 1 0 ≫ NatTrans.app X.hom (op [0]) = 0
[PROOFSTEP]
rw [alternatingFaceMapComplex_obj_d, objD, Fin.sum_univ_two, Fin.val_zero, pow_zero, one_smul, Fin.val_one, pow_one,
  neg_smul, one_smul, add_comp, neg_comp, SimplicialObject.δ_naturality, SimplicialObject.δ_naturality]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.208144, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ NatTrans.app X.hom (op [0 + 1]) ≫ SimplicialObject.δ ((SimplicialObject.const C).obj X.right) 0 +
      -NatTrans.app X.hom (op [0 + 1]) ≫ SimplicialObject.δ ((SimplicialObject.const C).obj X.right) 1 =
    0
[PROOFSTEP]
apply add_right_neg
[GOAL]
C : Type u_1
inst✝² : Category.{?u.208144, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
x✝¹ x✝ : SimplicialObject.Augmented C
f : x✝¹ ⟶ x✝
⊢ HomologicalComplex.Hom.f
      ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).map f ≫
        (fun X =>
            ↑(ChainComplex.toSingle₀Equiv ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X)
                    (SimplicialObject.Augmented.point.obj X)).symm
              { val := NatTrans.app X.hom (op [0]),
                property :=
                  (_ :
                    HomologicalComplex.d ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X) 1 0 ≫
                        NatTrans.app X.hom (op [0]) =
                      0) })
          x✝)
      0 =
    HomologicalComplex.Hom.f
      ((fun X =>
            ↑(ChainComplex.toSingle₀Equiv ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X)
                    (SimplicialObject.Augmented.point.obj X)).symm
              { val := NatTrans.app X.hom (op [0]),
                property :=
                  (_ :
                    HomologicalComplex.d ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X) 1 0 ≫
                        NatTrans.app X.hom (op [0]) =
                      0) })
          x✝¹ ≫
        (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C).map f)
      0
[PROOFSTEP]
exact congr_app f.w _
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (normalizedMooreComplex A).obj X ⟶ (alternatingFaceMapComplex A).obj X
[PROOFSTEP]
dsimp only [normalizedMooreComplex, NormalizedMooreComplex.obj, alternatingFaceMapComplex,
  AlternatingFaceMapComplex.obj]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ ChainComplex.of (fun n => underlying.obj (NormalizedMooreComplex.objX X n)) (NormalizedMooreComplex.objD X)
      (_ : ∀ (n : ℕ), NormalizedMooreComplex.objD X (n + 1) ≫ NormalizedMooreComplex.objD X n = 0) ⟶
    ChainComplex.of (fun n => X.obj (op [n])) (AlternatingFaceMapComplex.objD X)
      (_ : ∀ (n : ℕ), AlternatingFaceMapComplex.objD X (n + 1) ≫ AlternatingFaceMapComplex.objD X n = 0)
[PROOFSTEP]
apply
  ChainComplex.ofHom _ _ _ _ _ _
    (fun n => (NormalizedMooreComplex.objX X n).arrow)
      /- we have to show the compatibility of the differentials on the alternating
                 face map complex with those defined on the normalized Moore complex:
                 we first get rid of the terms of the alternating sum that are obviously
                 zero on the normalized_Moore_complex -/
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ ∀ (i : ℕ),
    arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ AlternatingFaceMapComplex.objD X i =
      NormalizedMooreComplex.objD X i ≫ arrow (NormalizedMooreComplex.objX X i)
[PROOFSTEP]
intro i
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ AlternatingFaceMapComplex.objD X i =
    NormalizedMooreComplex.objD X i ≫ arrow (NormalizedMooreComplex.objX X i)
[PROOFSTEP]
simp only [AlternatingFaceMapComplex.objD, comp_sum]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ ∑ j : Fin (i + 2), arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ ((-1) ^ ↑j • SimplicialObject.δ X j) =
    NormalizedMooreComplex.objD X i ≫ arrow (NormalizedMooreComplex.objX X i)
[PROOFSTEP]
rw [Fin.sum_univ_succ, Fintype.sum_eq_zero]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) + 0 =
    NormalizedMooreComplex.objD X i ≫ arrow (NormalizedMooreComplex.objX X i)
case h
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ ∀ (a : Fin (i + 1)),
    arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ ((-1) ^ ↑(Fin.succ a) • SimplicialObject.δ X (Fin.succ a)) = 0
[PROOFSTEP]
swap
[GOAL]
case h
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ ∀ (a : Fin (i + 1)),
    arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ ((-1) ^ ↑(Fin.succ a) • SimplicialObject.δ X (Fin.succ a)) = 0
[PROOFSTEP]
intro j
[GOAL]
case h
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
j : Fin (i + 1)
⊢ arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ ((-1) ^ ↑(Fin.succ j) • SimplicialObject.δ X (Fin.succ j)) = 0
[PROOFSTEP]
rw [NormalizedMooreComplex.objX, comp_zsmul, ←
  factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ _ (Finset.mem_univ j)), Category.assoc,
  kernelSubobject_arrow_comp, comp_zero, smul_zero]
  -- finally, we study the remaining term which is induced by X.δ 0
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) + 0 =
    NormalizedMooreComplex.objD X i ≫ arrow (NormalizedMooreComplex.objX X i)
[PROOFSTEP]
rw [add_zero, Fin.val_zero, pow_zero, one_zsmul]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ SimplicialObject.δ X 0 =
    NormalizedMooreComplex.objD X i ≫ arrow (NormalizedMooreComplex.objX X i)
[PROOFSTEP]
dsimp [NormalizedMooreComplex.objD, NormalizedMooreComplex.objX]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫ SimplicialObject.δ X 0 =
    (match i with
      | 0 =>
        arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          SimplicialObject.δ X 0 ≫ inv (arrow ⊤)
      | Nat.succ n =>
        factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
          (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
            SimplicialObject.δ X 0)
          (_ :
            Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
              (arrow (NormalizedMooreComplex.objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0))) ≫
      arrow
        (match i with
        | 0 => ⊤
        | Nat.succ n => Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
[PROOFSTEP]
cases i
[GOAL]
case zero
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫ SimplicialObject.δ X 0 =
    (match Nat.zero with
      | 0 =>
        arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          SimplicialObject.δ X 0 ≫ inv (arrow ⊤)
      | Nat.succ n =>
        factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
          (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
            SimplicialObject.δ X 0)
          (_ :
            Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
              (arrow (NormalizedMooreComplex.objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0))) ≫
      arrow
        (match Nat.zero with
        | 0 => ⊤
        | Nat.succ n => Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
[PROOFSTEP]
simp
[GOAL]
case succ
C : Type u_1
inst✝³ : Category.{?u.231611, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.231633, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n✝ : ℕ
⊢ arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫ SimplicialObject.δ X 0 =
    (match Nat.succ n✝ with
      | 0 =>
        arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          SimplicialObject.δ X 0 ≫ inv (arrow ⊤)
      | Nat.succ n =>
        factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
          (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
            SimplicialObject.δ X 0)
          (_ :
            Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
              (arrow (NormalizedMooreComplex.objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0))) ≫
      arrow
        (match Nat.succ n✝ with
        | 0 => ⊤
        | Nat.succ n => Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.253905, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{u_3, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) n = arrow (NormalizedMooreComplex.objX X n)
[PROOFSTEP]
dsimp only [inclusionOfMooreComplexMap]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.253905, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{u_3, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f
      (id
        (ChainComplex.ofHom (fun n => underlying.obj (NormalizedMooreComplex.objX X n)) (NormalizedMooreComplex.objD X)
          (_ : ∀ (n : ℕ), NormalizedMooreComplex.objD X (n + 1) ≫ NormalizedMooreComplex.objD X n = 0)
          (fun n => X.obj (op [n])) (AlternatingFaceMapComplex.objD X)
          (_ : ∀ (n : ℕ), AlternatingFaceMapComplex.objD X (n + 1) ≫ AlternatingFaceMapComplex.objD X n = 0)
          (fun n => arrow (NormalizedMooreComplex.objX X n))
          (_ :
            ∀ (i : ℕ),
              arrow (NormalizedMooreComplex.objX X (i + 1)) ≫ AlternatingFaceMapComplex.objD X i =
                NormalizedMooreComplex.objD X i ≫ arrow (NormalizedMooreComplex.objX X i))))
      n =
    arrow (NormalizedMooreComplex.objX X n)
[PROOFSTEP]
exact ChainComplex.ofHom_f _ _ _ _ _ _ _ _ n
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.290163, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
n : ℕ
⊢ objD X n = (AlternatingFaceMapComplex.objD ((cosimplicialSimplicialEquiv C).functor.obj (op X)) n).unop
[PROOFSTEP]
simp only [objD, AlternatingFaceMapComplex.objD, unop_sum, unop_zsmul]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.290163, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
n : ℕ
⊢ ∑ i : Fin (n + 2), (-1) ^ ↑i • CosimplicialObject.δ X i =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • (SimplicialObject.δ ((cosimplicialSimplicialEquiv C).functor.obj (op X)) x).unop
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.291615, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
n : ℕ
⊢ objD X n ≫ objD X (n + 1) = 0
[PROOFSTEP]
simp only [d_eq_unop_d, ← unop_comp, AlternatingFaceMapComplex.d_squared, unop_zero]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.308930, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.308952, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ (fun n => NatTrans.app f [n]) n ≫ objD Y n = objD X n ≫ (fun n => NatTrans.app f [n]) (n + 1)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.308930, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.308952, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ NatTrans.app f [n] ≫ ∑ i : Fin (n + 2), (-1) ^ ↑i • CosimplicialObject.δ Y i =
    (∑ i : Fin (n + 2), (-1) ^ ↑i • CosimplicialObject.δ X i) ≫ NatTrans.app f [n + 1]
[PROOFSTEP]
rw [comp_sum, sum_comp]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.308930, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.308952, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ ∑ j : Fin (n + 2), NatTrans.app f [n] ≫ ((-1) ^ ↑j • CosimplicialObject.δ Y j) =
    ∑ j : Fin (n + 2), ((-1) ^ ↑j • CosimplicialObject.δ X j) ≫ NatTrans.app f [n + 1]
[PROOFSTEP]
refine' Finset.sum_congr rfl fun x _ => _
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.308930, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.308952, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
x✝ : x ∈ Finset.univ
⊢ NatTrans.app f [n] ≫ ((-1) ^ ↑x • CosimplicialObject.δ Y x) =
    ((-1) ^ ↑x • CosimplicialObject.δ X x) ≫ NatTrans.app f [n + 1]
[PROOFSTEP]
rw [comp_zsmul, zsmul_comp]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.308930, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.308952, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
x✝ : x ∈ Finset.univ
⊢ (-1) ^ ↑x • NatTrans.app f [n] ≫ CosimplicialObject.δ Y x =
    (-1) ^ ↑x • CosimplicialObject.δ X x ≫ NatTrans.app f [n + 1]
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u_1
inst✝³ : Category.{?u.308930, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.308952, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
x✝ : x ∈ Finset.univ
⊢ NatTrans.app f [n] ≫ CosimplicialObject.δ Y x = CosimplicialObject.δ X x ≫ NatTrans.app f [n + 1]
[PROOFSTEP]
symm
[GOAL]
case e_a
C : Type u_1
inst✝³ : Category.{?u.308930, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{?u.308952, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
x✝ : x ∈ Finset.univ
⊢ CosimplicialObject.δ X x ≫ NatTrans.app f [n + 1] = NatTrans.app f [n] ≫ CosimplicialObject.δ Y x
[PROOFSTEP]
apply f.naturality
