[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


[GOAL]
⊢ LargeCategory SSet
[PROOFSTEP]
dsimp only [SSet]
[GOAL]
⊢ LargeCategory (SimplicialObject (Type ?u.23))
[PROOFSTEP]
infer_instance
[GOAL]
⊢ HasLimits SSet
[PROOFSTEP]
dsimp only [SSet]
[GOAL]
⊢ HasLimits (SimplicialObject (Type ?u.489))
[PROOFSTEP]
infer_instance
[GOAL]
⊢ HasColimits SSet
[PROOFSTEP]
dsimp only [SSet]
[GOAL]
⊢ HasColimits (SimplicialObject (Type ?u.577))
[PROOFSTEP]
infer_instance
  -- Porting note: added an `ext` lemma.
  -- See https://github.com/leanprover-community/mathlib4/issues/5229
[GOAL]
n : ℕ
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // ¬Function.Surjective ↑(asOrderHom α) }) m₁
⊢ ¬Function.Surjective ↑(asOrderHom (f.unop ≫ ↑α))
[PROOFSTEP]
intro h
[GOAL]
n : ℕ
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // ¬Function.Surjective ↑(asOrderHom α) }) m₁
h : Function.Surjective ↑(asOrderHom (f.unop ≫ ↑α))
⊢ False
[PROOFSTEP]
apply α.property
[GOAL]
n : ℕ
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // ¬Function.Surjective ↑(asOrderHom α) }) m₁
h : Function.Surjective ↑(asOrderHom (f.unop ≫ ↑α))
⊢ Function.Surjective ↑(asOrderHom ↑α)
[PROOFSTEP]
exact Function.Surjective.of_comp h
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
⊢ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i} ≠ Set.univ
[PROOFSTEP]
intro h
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i} = Set.univ
⊢ False
[PROOFSTEP]
apply α.property
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i} = Set.univ
⊢ Set.range ↑(asOrderHom ↑α) ∪ {i} = Set.univ
[PROOFSTEP]
rw [Set.eq_univ_iff_forall] at h ⊢
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i}
⊢ ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom ↑α) ∪ {i}
[PROOFSTEP]
intro j
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i}
j : Fin (n + 1)
⊢ j ∈ Set.range ↑(asOrderHom ↑α) ∪ {i}
[PROOFSTEP]
apply Or.imp _ id (h j)
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i}
j : Fin (n + 1)
⊢ j ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) → j ∈ Set.range ↑(asOrderHom ↑α)
[PROOFSTEP]
intro hj
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i}
j : Fin (n + 1)
hj : j ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α))
⊢ j ∈ Set.range ↑(asOrderHom ↑α)
[PROOFSTEP]
exact Set.range_comp_subset_range _ _ hj
[GOAL]
n : ℕ
⊢ LargeCategory (Truncated n)
[PROOFSTEP]
dsimp only [Truncated]
[GOAL]
n : ℕ
⊢ LargeCategory (SimplicialObject.Truncated (Type ?u.74955) n)
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ HasLimits (Truncated n)
[PROOFSTEP]
dsimp only [Truncated]
[GOAL]
n : ℕ
⊢ HasLimits (SimplicialObject.Truncated (Type ?u.75436) n)
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ HasColimits (Truncated n)
[PROOFSTEP]
dsimp only [Truncated]
[GOAL]
n : ℕ
⊢ HasColimits (SimplicialObject.Truncated (Type ?u.75544) n)
[PROOFSTEP]
infer_instance
  -- Porting note: added an `ext` lemma.
  -- See https://github.com/leanprover-community/mathlib4/issues/5229


[GOAL]
X✝ : Type u
Y : Type v
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X✝
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Group (FundamentalGroup X x)
[PROOFSTEP]
dsimp only [FundamentalGroup]
[GOAL]
X✝ : Type u
Y : Type v
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X✝
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Group (Aut x)
[PROOFSTEP]
infer_instance
[GOAL]
X✝ : Type u
Y : Type v
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X✝
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Inhabited (FundamentalGroup X x)
[PROOFSTEP]
dsimp only [FundamentalGroup]
[GOAL]
X✝ : Type u
Y : Type v
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X✝
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Inhabited (Aut x)
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ underlying.obj (objX X (n + 1 + 1)) ⟶ underlying.obj (objX X (n + 1))
[PROOFSTEP]
refine'
  factorThru _ (arrow _ ≫ X.δ (0 : Fin (n + 3)))
    _
      -- We now need to show that it factors!
          -- A morphism factors through an intersection of subobjects if it factors through each.
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ Factors (objX X (n + 1)) (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)
[PROOFSTEP]
refine'
  (finset_inf_factors _).mpr fun i _ =>
    _
      -- A morphism `f` factors through the kernel of `g` exactly if `f ≫ g = 0`.
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i))) (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)
[PROOFSTEP]
apply kernelSubobject_factors
[GOAL]
case w
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0) ≫ SimplicialObject.δ X (Fin.succ i) = 0
[PROOFSTEP]
dsimp [objX]
  -- Use a simplicial identity
[GOAL]
case w
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        SimplicialObject.δ X 0) ≫
      SimplicialObject.δ X (Fin.succ i) =
    0
[PROOFSTEP]
erw [Category.assoc, ← X.δ_comp_δ (Fin.zero_le i.succ)]
  -- We can rewrite the arrow out of the intersection of all the kernels as a composition
      -- of a morphism we don't care about with the arrow out of the kernel of `X.δ i.succ.succ`.
[GOAL]
case w
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
      SimplicialObject.δ X (Fin.succ (Fin.succ i)) ≫ SimplicialObject.δ X 0 =
    0
[PROOFSTEP]
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)), Category.assoc,
  kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ Fin.succ i ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (n + 1) ≫ objD X n = 0
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ objD X (Nat.zero + 1) ≫ objD X Nat.zero = 0
[PROOFSTEP]
dsimp [objD]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (Nat.succ n + 1) ≫ objD X (Nat.succ n) = 0
[PROOFSTEP]
dsimp [objD]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ 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 (objX X (0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        SimplicialObject.δ X 0 ≫ inv (arrow ⊤) =
    0
[PROOFSTEP]
erw [Subobject.factorThru_arrow_assoc, Category.assoc, ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)), ←
  factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)), Category.assoc,
  kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ 0 ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
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 (objX X (n + 1 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      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 (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)) =
    0
[PROOFSTEP]
erw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc, ←
  X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))), ←
  factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)), Category.assoc,
  kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ 0 ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n : ℕ
⊢ Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ Factors (objX Y Nat.zero) (arrow (objX X Nat.zero) ≫ NatTrans.app f (op (SimplexCategory.mk Nat.zero)))
[PROOFSTEP]
dsimp
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ Factors (objX Y (Nat.succ n✝)) (arrow (objX X (Nat.succ n✝)) ≫ NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))
[PROOFSTEP]
dsimp
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ Factors ⊤ (arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0)))
[PROOFSTEP]
apply top_factors
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
    (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
      NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))
[PROOFSTEP]
refine' (finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ _
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝)))) ≫
      SimplicialObject.δ Y (Fin.succ i) =
    0
[PROOFSTEP]
erw [Category.assoc, ← f.naturality, ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)),
  Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ i ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n : ℕ
⊢ (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        (n + 1) ≫
      objD Y n =
    objD X n ≫
      (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        n
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        (Nat.zero + 1) ≫
      objD Y Nat.zero =
    objD X Nat.zero ≫
      (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        Nat.zero
[PROOFSTEP]
dsimp [objD, objX]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        (Nat.succ n✝ + 1) ≫
      objD Y (Nat.succ n✝) =
    objD X (Nat.succ n✝) ≫
      (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        (Nat.succ n✝)
[PROOFSTEP]
dsimp [objD, objX]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          NatTrans.app f (op (SimplexCategory.mk (0 + 1))))
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
            (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
              NatTrans.app f (op (SimplexCategory.mk (Nat.succ 0))))) ≫
      arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k))) ≫
        SimplicialObject.δ Y 0 ≫ inv (arrow ⊤) =
    (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        SimplicialObject.δ X 0 ≫ inv (arrow ⊤)) ≫
      factorThru ⊤ (arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0)))
        (_ : Factors ⊤ (arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0))))
[PROOFSTEP]
aesop_cat
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝ + 1))))
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
            (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
              NatTrans.app f (op (SimplexCategory.mk (Nat.succ (Nat.succ n✝)))))) ≫
      factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k))) ≫
          SimplicialObject.δ Y 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
            (arrow (objX Y (n✝ + 1 + 1)) ≫ SimplicialObject.δ Y 0)) =
    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 (objX X (n✝ + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
            (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
              NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝)))))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ { obj := obj, map := fun {X Y} f => map f }.map (𝟙 X) = 𝟙 ({ obj := obj, map := fun {X Y} f => map f }.obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (𝟙 X)) Nat.zero =
    HomologicalComplex.Hom.f (𝟙 ({ obj := obj, map := fun {X Y} f => map f }.obj X)) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n✝ : ℕ
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (𝟙 X)) (Nat.succ n✝) =
    HomologicalComplex.Hom.f (𝟙 ({ obj := obj, map := fun {X Y} f => map f }.obj X)) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ Subobject.factorThru ⊤ (Subobject.arrow ⊤ ≫ 𝟙 (X.obj (op (SimplexCategory.mk 0))))
      (_ : Subobject.Factors (objX X 0) (Subobject.arrow (objX X 0) ≫ NatTrans.app (𝟙 X) (op (SimplexCategory.mk 0)))) =
    𝟙 (Subobject.underlying.obj ⊤)
[PROOFSTEP]
aesop_cat
[GOAL]
case h.succ
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n✝ : ℕ
⊢ Subobject.factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
      (Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        𝟙 (X.obj (op (SimplexCategory.mk (Nat.succ n✝)))))
      (_ :
        Subobject.Factors (objX X (Nat.succ n✝))
          (Subobject.arrow (objX X (Nat.succ n✝)) ≫ NatTrans.app (𝟙 X) (op (SimplexCategory.mk (Nat.succ n✝))))) =
    𝟙 (Subobject.underlying.obj (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := obj, map := fun {X Y} f => map f }.map (f ≫ g) =
    { obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (f ≫ g)) Nat.zero =
    HomologicalComplex.Hom.f
      ({ obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g) Nat.zero
[PROOFSTEP]
apply Subobject.eq_of_comp_arrow_eq
[GOAL]
case h.succ
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
n✝ : ℕ
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (f ≫ g)) (Nat.succ n✝) =
    HomologicalComplex.Hom.f
      ({ obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g)
      (Nat.succ n✝)
[PROOFSTEP]
apply Subobject.eq_of_comp_arrow_eq
[GOAL]
case h.zero.h
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (f ≫ g)) Nat.zero ≫
      Subobject.arrow (objX Z✝ Nat.zero) =
    HomologicalComplex.Hom.f
        ({ obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g)
        Nat.zero ≫
      Subobject.arrow (objX Z✝ Nat.zero)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ.h
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
n✝ : ℕ
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (f ≫ g)) (Nat.succ n✝) ≫
      Subobject.arrow (objX Z✝ (Nat.succ n✝)) =
    HomologicalComplex.Hom.f
        ({ obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g)
        (Nat.succ n✝) ≫
      Subobject.arrow (objX Z✝ (Nat.succ n✝))
[PROOFSTEP]
dsimp
[GOAL]
case h.zero.h
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Subobject.factorThru ⊤
        (Subobject.arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0)) ≫ NatTrans.app g (op (SimplexCategory.mk 0)))
        (_ :
          Subobject.Factors (objX Z✝ 0)
            (Subobject.arrow (objX X✝ 0) ≫ NatTrans.app (f ≫ g) (op (SimplexCategory.mk 0)))) ≫
      Subobject.arrow ⊤ =
    (Subobject.factorThru ⊤ (Subobject.arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0)))
          (_ :
            Subobject.Factors (objX Y✝ 0) (Subobject.arrow (objX X✝ 0) ≫ NatTrans.app f (op (SimplexCategory.mk 0)))) ≫
        Subobject.factorThru ⊤ (Subobject.arrow ⊤ ≫ NatTrans.app g (op (SimplexCategory.mk 0)))
          (_ :
            Subobject.Factors (objX Z✝ 0) (Subobject.arrow (objX Y✝ 0) ≫ NatTrans.app g (op (SimplexCategory.mk 0))))) ≫
      Subobject.arrow ⊤
[PROOFSTEP]
aesop_cat
[GOAL]
case h.succ.h
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
n✝ : ℕ
⊢ Subobject.factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Z✝ (Fin.succ k)))
        (Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X✝ (Fin.succ k))) ≫
          NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))) ≫
            NatTrans.app g (op (SimplexCategory.mk (Nat.succ n✝))))
        (_ :
          Subobject.Factors (objX Z✝ (Nat.succ n✝))
            (Subobject.arrow (objX X✝ (Nat.succ n✝)) ≫ NatTrans.app (f ≫ g) (op (SimplexCategory.mk (Nat.succ n✝))))) ≫
      Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Z✝ (Fin.succ k))) =
    (Subobject.factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y✝ (Fin.succ k)))
          (Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X✝ (Fin.succ k))) ≫
            NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))
          (_ :
            Subobject.Factors (objX Y✝ (Nat.succ n✝))
              (Subobject.arrow (objX X✝ (Nat.succ n✝)) ≫ NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))) ≫
        Subobject.factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Z✝ (Fin.succ k)))
          (Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y✝ (Fin.succ k))) ≫
            NatTrans.app g (op (SimplexCategory.mk (Nat.succ n✝))))
          (_ :
            Subobject.Factors (objX Z✝ (Nat.succ n✝))
              (Subobject.arrow (objX Y✝ (Nat.succ n✝)) ≫ NatTrans.app g (op (SimplexCategory.mk (Nat.succ n✝)))))) ≫
      Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Z✝ (Fin.succ k)))
[PROOFSTEP]
aesop_cat


[GOAL]
x y : Path PUnit.unit PUnit.unit
⊢ x = y
[PROOFSTEP]
ext
[GOAL]
x y : FundamentalGroupoid PUnit
⊢ Subsingleton (x ⟶ y)
[PROOFSTEP]
convert_to Subsingleton (Path.Homotopic.Quotient PUnit.unit PUnit.unit)
[GOAL]
x y : FundamentalGroupoid PUnit
⊢ Subsingleton (Path.Homotopic.Quotient PUnit.unit PUnit.unit)
[PROOFSTEP]
apply Quotient.instSubsingletonQuotient
[GOAL]
x✝ : FundamentalGroupoid PUnit
⊢ (𝟭 (FundamentalGroupoid PUnit)).obj x✝ =
    (Functor.star (FundamentalGroupoid PUnit) ⋙ (Functor.const (Discrete PUnit)).obj PUnit.unit).obj x✝
[PROOFSTEP]
simp