[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i : Δ' ⟶ [n]
hi : Mono i
h₁ : len Δ' ≠ n
h₂ : ¬Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
[PROOFSTEP]
induction' Δ' using SimplexCategory.rec with m
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
[PROOFSTEP]
obtain ⟨k, hk⟩ :=
  Nat.exists_eq_add_of_lt
    (len_lt_of_mono i fun h => by
      rw [← h] at h₁
      exact h₁ rfl)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
h : [n] = [m]
⊢ False
[PROOFSTEP]
rw [← h] at h₁
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [n] ≠ n
h₂ : ¬Isδ₀ i
h : [n] = [m]
⊢ False
[PROOFSTEP]
exact h₁ rfl
[GOAL]
case h.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : len [n] = len [m] + k + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
[PROOFSTEP]
simp only [len_mk] at hk
[GOAL]
case h.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + k + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
[PROOFSTEP]
rcases k with _ | k
[GOAL]
case h.intro.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + Nat.zero + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
[PROOFSTEP]
change n = m + 1 at hk
[GOAL]
case h.intro.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
[PROOFSTEP]
subst hk
[GOAL]
case h.intro.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i✝ : Δ' ⟶ [m + 1]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i✝
i : [m] ⟶ [m + 1]
hi : Mono i
h₁ : len [m] ≠ m + 1
h₂ : ¬Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map i.op = 0
[PROOFSTEP]
obtain ⟨j, rfl⟩ := eq_δ_of_mono i
[GOAL]
case h.intro.zero.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬Isδ₀ (SimplexCategory.δ j)
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0
[PROOFSTEP]
rw [Isδ₀.iff] at h₂
[GOAL]
case h.intro.zero.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0
[PROOFSTEP]
have h₃ : 1 ≤ (j : ℕ) := by
  by_contra h
  exact h₂ (by simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ 1 ≤ ↑j
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h : ¬1 ≤ ↑j
⊢ False
[PROOFSTEP]
exact h₂ (by simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h : ¬1 ≤ ↑j
⊢ j = 0
[PROOFSTEP]
simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h
[GOAL]
case h.intro.zero.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ ↑j
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0
[PROOFSTEP]
exact (HigherFacesVanish.of_P (m + 1) m).comp_δ_eq_zero j h₂ (by linarith)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ ↑j
⊢ m + 2 ≤ ↑j + (m + 1)
[PROOFSTEP]
linarith
[GOAL]
case h.intro.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + Nat.succ k + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, ← add_assoc] at hk
[GOAL]
case h.intro.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + k + 1 + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
[PROOFSTEP]
clear h₂ hi
[GOAL]
case h.intro.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi : Mono i✝
h₁✝ : len Δ' ≠ n
h₂ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
h₁ : len [m] ≠ n
k : ℕ
hk : n = m + k + 1 + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
[PROOFSTEP]
subst hk
[GOAL]
case h.intro.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map i.op = 0
[PROOFSTEP]
obtain ⟨j₁ : Fin (_ + 1), i, rfl⟩ :=
  eq_comp_δ_of_not_surjective i fun h =>
    by
    have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)
    dsimp at h'
    linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
h : Function.Surjective ↑(Hom.toOrderHom i)
⊢ False
[PROOFSTEP]
have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : len [m + k + 1 + 1] ≤ len [m]
⊢ False
[PROOFSTEP]
dsimp at h'
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : m + k + 1 + 1 ≤ m
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case h.intro.succ.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ j₁).op = 0
[PROOFSTEP]
obtain ⟨j₂, i, rfl⟩ :=
  eq_comp_δ_of_not_surjective i fun h =>
    by
    have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)
    dsimp at h'
    linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
h : Function.Surjective ↑(Hom.toOrderHom i)
⊢ False
[PROOFSTEP]
have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : len [m + k + 1] ≤ len [m]
⊢ False
[PROOFSTEP]
dsimp at h'
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : m + k + 1 ≤ m
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case h.intro.succ.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
[PROOFSTEP]
by_cases hj₁ : j₁ = 0
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : j₁ = 0
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
[PROOFSTEP]
subst hj₁
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ 0).op = 0
[PROOFSTEP]
rw [assoc, ← SimplexCategory.δ_comp_δ'' (Fin.zero_le _)]
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫
      X.map (i ≫ SimplexCategory.δ (Fin.castLT 0 (_ : ↑0 < m + k + 2)) ≫ SimplexCategory.δ (Fin.succ j₂)).op =
    0
[PROOFSTEP]
simp only [op_comp, X.map_comp, assoc, PInfty_f]
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ (Fin.succ j₂)).op ≫
        X.map (SimplexCategory.δ (Fin.castLT 0 (_ : ↑0 < m + k + 2))).op ≫ X.map i.op =
    0
[PROOFSTEP]
erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ j₂.succ_ne_zero, zero_comp]
[GOAL]
case pos.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ m + k + 1 + 2 ≤ ↑(Fin.succ j₂) + (m + k + 1 + 1)
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, Nat.add, Fin.succ]
[GOAL]
case pos.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ m + k + 1 + 2 ≤ ↑j₂ + 1 + (m + k + 1 + 1)
[PROOFSTEP]
linarith
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
[PROOFSTEP]
simp only [op_comp, X.map_comp, assoc, PInfty_f]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₁).op ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op =
    0
[PROOFSTEP]
erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ hj₁, zero_comp]
[GOAL]
case neg.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
[PROOFSTEP]
by_contra
[GOAL]
case neg.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
x✝ : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ False
[PROOFSTEP]
exact hj₁ (by simp only [Fin.ext_iff, Fin.val_zero]; linarith)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
x✝ : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ j₁ = 0
[PROOFSTEP]
simp only [Fin.ext_iff, Fin.val_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
x✝ : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ ↑j₁ = 0
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty (len Δ) =
    HomologicalComplex.Hom.f PInfty (len Δ') ≫ X.map i.op
[PROOFSTEP]
induction' Δ using SimplexCategory.rec with n
[GOAL]
case h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝ : Δ ⟶ Δ'
inst✝¹ : Mono i✝
n : ℕ
i : [n] ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty (len [n]) =
    HomologicalComplex.Hom.f PInfty (len Δ') ≫ X.map i.op
[PROOFSTEP]
induction' Δ' using SimplexCategory.rec with n'
[GOAL]
case h.h
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty (len [n]) =
    HomologicalComplex.Hom.f PInfty (len [n']) ≫ X.map i.op
[PROOFSTEP]
dsimp
  -- We start with the case `i` is an identity
[GOAL]
case h.h
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
[PROOFSTEP]
by_cases n = n'
[GOAL]
case h.h
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
[PROOFSTEP]
by_cases n = n'
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n]
inst✝¹ : Mono i✝
i : [n] ⟶ [n]
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n ≫ X.map i.op
[PROOFSTEP]
simp only [SimplexCategory.eq_id_of_mono i, Γ₀.Obj.Termwise.mapMono_id, op_id, X.map_id]
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n]
inst✝¹ : Mono i✝
i : [n] ⟶ [n]
inst✝ : Mono i
⊢ 𝟙 (HomologicalComplex.X K[X] (len [n])) ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (X.obj (op [n]))
[PROOFSTEP]
dsimp
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n]
inst✝¹ : Mono i✝
i : [n] ⟶ [n]
inst✝ : Mono i
⊢ 𝟙 (X.obj (op [n])) ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (X.obj (op [n]))
[PROOFSTEP]
simp only [id_comp, comp_id]
[GOAL]
case neg
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
[PROOFSTEP]
by_cases hi : Isδ₀ i
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
[PROOFSTEP]
have h' : n' = n + 1 := hi.left
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : Isδ₀ i
h' : n' = n + 1
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
[PROOFSTEP]
subst h'
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
[PROOFSTEP]
simp only [Γ₀.Obj.Termwise.mapMono_δ₀' _ i hi]
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.d K[X] (len [n + 1]) (len [n]) ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
[PROOFSTEP]
dsimp
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.d K[X] (n + 1) n ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
[PROOFSTEP]
rw [← PInfty.comm _ n, AlternatingFaceMapComplex.obj_d_eq]
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ (HomologicalComplex.Hom.f PInfty (n + 1) ≫ Finset.sum Finset.univ fun i => (-1) ^ ↑i • SimplicialObject.δ X i) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
[PROOFSTEP]
simp only [eq_self_iff_true, id_comp, if_true, Preadditive.comp_sum]
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ (Finset.sum Finset.univ fun j => HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑j • SimplicialObject.δ X j)) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
[PROOFSTEP]
rw [Finset.sum_eq_single (0 : Fin (n + 2))]
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
case pos.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ (b : Fin (n + 2)),
    b ∈ Finset.univ → b ≠ 0 → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑b • SimplicialObject.δ X b) = 0
case pos.h₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ¬0 ∈ Finset.univ → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) = 0
[PROOFSTEP]
rotate_left
[GOAL]
case pos.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ (b : Fin (n + 2)),
    b ∈ Finset.univ → b ≠ 0 → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑b • SimplicialObject.δ X b) = 0
[PROOFSTEP]
intro b _ hb
[GOAL]
case pos.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑b • SimplicialObject.δ X b) = 0
[PROOFSTEP]
rw [Preadditive.comp_zsmul]
[GOAL]
case pos.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ (-1) ^ ↑b • HomologicalComplex.Hom.f PInfty (n + 1) ≫ SimplicialObject.δ X b = 0
[PROOFSTEP]
erw [PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
    (by
      rw [Isδ₀.iff]
      exact hb),
  zsmul_zero]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ b)
[PROOFSTEP]
rw [Isδ₀.iff]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬b = 0
[PROOFSTEP]
exact hb
[GOAL]
case pos.h₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ¬0 ∈ Finset.univ → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) = 0
[PROOFSTEP]
simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff]
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
[PROOFSTEP]
simp only [hi.eq_δ₀, Fin.val_zero, pow_zero, one_zsmul]
[GOAL]
case pos
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ SimplicialObject.δ X 0 =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map (SimplexCategory.δ 0).op
[PROOFSTEP]
rfl
  -- The case `i ≠ δ 0`
[GOAL]
case neg
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
[PROOFSTEP]
rw [Γ₀.Obj.Termwise.mapMono_eq_zero _ i _ hi, zero_comp]
[GOAL]
case neg
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ [n'] ≠ [n]
[PROOFSTEP]
swap
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ [n'] ≠ [n]
[PROOFSTEP]
by_contra h'
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : [n'] = [n]
⊢ False
[PROOFSTEP]
exact h (congr_arg SimplexCategory.len h'.symm)
[GOAL]
case neg
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
[PROOFSTEP]
rw [PInfty_comp_map_mono_eq_zero]
[GOAL]
case neg.h₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ len [n] ≠ n'
[PROOFSTEP]
exact h
[GOAL]
case neg.h₂
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ¬Isδ₀ i
[PROOFSTEP]
by_contra h'
[GOAL]
case neg.h₂
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : Isδ₀ i
⊢ False
[PROOFSTEP]
exact hi h'
[GOAL]
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
⊢ ((N₁ ⋙ Γ₂).obj X).X.map θ ≫
      (fun Δ =>
          Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
            HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
        Δ' =
    (fun Δ =>
          Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
            HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
        Δ ≫
      ((toKaroubi (SimplicialObject C)).obj X).X.map θ
[PROOFSTEP]
apply (Γ₀.splitting K[X]).hom_ext'
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
⊢ ∀ (A : Splitting.IndexSet Δ),
    Splitting.ιSummand (Γ₀.splitting K[X]) A ≫
        ((N₁ ⋙ Γ₂).obj X).X.map θ ≫
          (fun Δ =>
              Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
            Δ' =
      Splitting.ιSummand (Γ₀.splitting K[X]) A ≫
        (fun Δ =>
              Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
            Δ ≫
          ((toKaroubi (SimplicialObject C)).obj X).X.map θ
[PROOFSTEP]
intro A
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ Splitting.ιSummand (Γ₀.splitting K[X]) A ≫
      ((N₁ ⋙ Γ₂).obj X).X.map θ ≫
        (fun Δ =>
            Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
              HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
          Δ' =
    Splitting.ιSummand (Γ₀.splitting K[X]) A ≫
      (fun Δ =>
            Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
              HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
          Δ ≫
        ((toKaroubi (SimplicialObject C)).obj X).X.map θ
[PROOFSTEP]
change _ ≫ (Γ₀.obj K[X]).map θ ≫ _ = _
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ Splitting.ιSummand (Γ₀.splitting K[X]) A ≫
      (Γ₀.obj K[X]).map θ ≫
        (fun Δ =>
            Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
              HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
          Δ' =
    Splitting.ιSummand (Γ₀.splitting K[X]) A ≫
      (fun Δ =>
            Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
              HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
          Δ ≫
        ((toKaroubi (SimplicialObject C)).obj X).X.map θ
[PROOFSTEP]
simp only [Splitting.ι_desc_assoc, assoc, Γ₀.Obj.map_on_summand'_assoc, Splitting.ι_desc]
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ Γ₀.Obj.Termwise.mapMono K[X] (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      HomologicalComplex.Hom.f PInfty (len (Splitting.IndexSet.pull A θ).fst.unop) ≫
        X.map (Splitting.IndexSet.e (Splitting.IndexSet.pull A θ)).op =
    HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫
      X.map (Splitting.IndexSet.e A).op ≫ ((toKaroubi (SimplicialObject C)).obj X).X.map θ
[PROOFSTEP]
erw [Γ₀_obj_termwise_mapMono_comp_PInfty_assoc X (image.ι (θ.unop ≫ A.e))]
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫
      X.map (image.ι (θ.unop ≫ Splitting.IndexSet.e A)).op ≫
        X.map (Splitting.IndexSet.e (Splitting.IndexSet.pull A θ)).op =
    HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫
      X.map (Splitting.IndexSet.e A).op ≫ ((toKaroubi (SimplicialObject C)).obj X).X.map θ
[PROOFSTEP]
dsimp only [toKaroubi]
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫
      X.map (image.ι (θ.unop ≫ Splitting.IndexSet.e A)).op ≫
        X.map (Splitting.IndexSet.e (Splitting.IndexSet.pull A θ)).op =
    HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op ≫ X.map θ
[PROOFSTEP]
simp only [← X.map_comp]
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫
      X.map ((image.ι (θ.unop ≫ Splitting.IndexSet.e A)).op ≫ (Splitting.IndexSet.e (Splitting.IndexSet.pull A θ)).op) =
    HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map ((Splitting.IndexSet.e A).op ≫ θ)
[PROOFSTEP]
congr 2
[GOAL]
case h.e_a.e_a
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ (image.ι (θ.unop ≫ Splitting.IndexSet.e A)).op ≫ (Splitting.IndexSet.e (Splitting.IndexSet.pull A θ)).op =
    (Splitting.IndexSet.e A).op ≫ θ
[PROOFSTEP]
simp only [eqToHom_refl, id_comp, comp_id, ← op_comp]
[GOAL]
case h.e_a.e_a
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ (Splitting.IndexSet.e (Splitting.IndexSet.pull A θ) ≫ image.ι (θ.unop ≫ Splitting.IndexSet.e A)).op =
    (Splitting.IndexSet.e A).op ≫ θ
[PROOFSTEP]
exact Quiver.Hom.unop_inj (A.fac_pull θ)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ (NatTrans.mk fun Δ =>
      Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
        HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op) =
    ((N₁ ⋙ Γ₂).obj X).p ≫
      (NatTrans.mk fun Δ =>
          Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
            HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op) ≫
        ((toKaroubi (SimplicialObject C)).obj X).p
[PROOFSTEP]
apply (Γ₀.splitting K[X]).hom_ext
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ ∀ (n : ℕ),
    Splitting.φ (Γ₀.splitting K[X])
        (NatTrans.mk fun Δ =>
          Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
            HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
        n =
      Splitting.φ (Γ₀.splitting K[X])
        (((N₁ ⋙ Γ₂).obj X).p ≫
          (NatTrans.mk fun Δ =>
              Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op) ≫
            ((toKaroubi (SimplicialObject C)).obj X).p)
        n
[PROOFSTEP]
intro n
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
n : ℕ
⊢ Splitting.φ (Γ₀.splitting K[X])
      (NatTrans.mk fun Δ =>
        Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
          HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op)
      n =
    Splitting.φ (Γ₀.splitting K[X])
      (((N₁ ⋙ Γ₂).obj X).p ≫
        (NatTrans.mk fun Δ =>
            Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
              HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op) ≫
          ((toKaroubi (SimplicialObject C)).obj X).p)
      n
[PROOFSTEP]
dsimp [N₁]
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
n : ℕ
⊢ (Splitting.ι (Γ₀.splitting K[X]) n ≫
      Splitting.desc (Γ₀.splitting K[X]) (op [n]) fun A =>
        HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op) =
    Splitting.ι (Γ₀.splitting K[X]) n ≫
      (Splitting.desc (Γ₀.splitting K[X]) (op [n]) fun A =>
          HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ Splitting.ιSummand (Γ₀.splitting K[X]) A) ≫
        (Splitting.desc (Γ₀.splitting K[X]) (op [n]) fun A =>
            HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op) ≫
          𝟙 (X.obj (op [n]))
[PROOFSTEP]
simp only [← Splitting.ιSummand_id, Splitting.ι_desc, comp_id, Splitting.ι_desc_assoc, assoc, PInfty_f_idem_assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
f : X ⟶ Y
⊢ (N₁ ⋙ Γ₂).map f ≫
      (fun X =>
          Karoubi.Hom.mk
            (NatTrans.mk fun Δ =>
              Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op))
        Y =
    (fun X =>
          Karoubi.Hom.mk
            (NatTrans.mk fun Δ =>
              Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op))
        X ≫
      (toKaroubi (SimplicialObject C)).map f
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
f : X ⟶ Y
⊢ ((N₁ ⋙ Γ₂).map f ≫
        (fun X =>
            Karoubi.Hom.mk
              (NatTrans.mk fun Δ =>
                Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                  HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op))
          Y).f =
    ((fun X =>
            Karoubi.Hom.mk
              (NatTrans.mk fun Δ =>
                Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                  HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op))
          X ≫
        (toKaroubi (SimplicialObject C)).map f).f
[PROOFSTEP]
apply (Γ₀.splitting K[X]).hom_ext
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
f : X ⟶ Y
⊢ ∀ (n : ℕ),
    Splitting.φ (Γ₀.splitting K[X])
        ((N₁ ⋙ Γ₂).map f ≫
            (fun X =>
                Karoubi.Hom.mk
                  (NatTrans.mk fun Δ =>
                    Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                      HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op))
              Y).f
        n =
      Splitting.φ (Γ₀.splitting K[X])
        ((fun X =>
                Karoubi.Hom.mk
                  (NatTrans.mk fun Δ =>
                    Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                      HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op))
              X ≫
            (toKaroubi (SimplicialObject C)).map f).f
        n
[PROOFSTEP]
intro n
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ Splitting.φ (Γ₀.splitting K[X])
      ((N₁ ⋙ Γ₂).map f ≫
          (fun X =>
              Karoubi.Hom.mk
                (NatTrans.mk fun Δ =>
                  Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                    HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op))
            Y).f
      n =
    Splitting.φ (Γ₀.splitting K[X])
      ((fun X =>
              Karoubi.Hom.mk
                (NatTrans.mk fun Δ =>
                  Splitting.desc (Γ₀.splitting K[X]) Δ fun A =>
                    HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op))
            X ≫
          (toKaroubi (SimplicialObject C)).map f).f
      n
[PROOFSTEP]
dsimp [N₁, toKaroubi]
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{?u.47488, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ (Splitting.ι (Γ₀.splitting K[X]) n ≫
      (Splitting.desc (Γ₀.splitting K[X]) (op [n]) fun A =>
          (HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ NatTrans.app f A.fst) ≫
            Splitting.ιSummand (Γ₀.splitting K[Y]) A) ≫
        Splitting.desc (Γ₀.splitting K[Y]) (op [n]) fun A =>
          HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ Y.map (Splitting.IndexSet.e A).op) =
    Splitting.ι (Γ₀.splitting K[X]) n ≫
      (Splitting.desc (Γ₀.splitting K[X]) (op [n]) fun A =>
          HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ X.map (Splitting.IndexSet.e A).op) ≫
        NatTrans.app f (op [n])
[PROOFSTEP]
simp only [← Splitting.ιSummand_id, Splitting.ι_desc, Splitting.ι_desc_assoc, assoc, PInfty_f_idem_assoc,
  Karoubi.comp_f, NatTrans.comp_app, Γ₂_map_f_app, HomologicalComplex.comp_f, AlternatingFaceMapComplex.map_f,
  PInfty_f_naturality_assoc, NatTrans.naturality, Splitting.IndexSet.id_fst, unop_op, len_mk]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.59660, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ toKaroubi (SimplicialObject C) ⋙ N₂ ⋙ Γ₂ = N₁ ⋙ Γ₂
[PROOFSTEP]
rw [← Functor.assoc, compatibility_N₁_N₂]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.80371, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ (toKaroubi (SimplicialObject C) ⋙ N₂ ⋙ Γ₂).obj X = (N₁ ⋙ Γ₂).obj X
[PROOFSTEP]
rw [← Functor.assoc, compatibility_N₁_N₂]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.hom X =
    eqToHom (_ : (toKaroubi (SimplicialObject C) ⋙ N₂ ⋙ Γ₂).obj X = (N₁ ⋙ Γ₂).obj X)
[PROOFSTEP]
dsimp only [compatibility_Γ₂N₁_Γ₂N₂, CategoryTheory.eqToIso]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app (eqToHom (_ : toKaroubi (SimplicialObject C) ⋙ N₂ ⋙ Γ₂ = N₁ ⋙ Γ₂)) X =
    eqToHom (_ : (toKaroubi (SimplicialObject C) ⋙ N₂ ⋙ Γ₂).obj X = (N₁ ⋙ Γ₂).obj X)
[PROOFSTEP]
apply eqToHom_app
[GOAL]
C : Type u_1
inst✝² : Category.{?u.83718, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ (N₁ ⋙ Γ₂).obj X = (toKaroubi (SimplicialObject C) ⋙ N₂ ⋙ Γ₂).obj X
[PROOFSTEP]
rw [← Functor.assoc, compatibility_N₁_N₂]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X =
    eqToHom (_ : (N₁ ⋙ Γ₂).obj X = (toKaroubi (SimplicialObject C) ⋙ N₂ ⋙ Γ₂).obj X)
[PROOFSTEP]
rw [← cancel_mono (compatibility_Γ₂N₁_Γ₂N₂.hom.app X), Iso.inv_hom_id_app, compatibility_Γ₂N₁_Γ₂N₂_hom_app,
  eqToHom_trans, eqToHom_refl]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.89220, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ ((whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (SimplicialObject C))).obj
          (toKaroubi (SimplicialObject C))).obj
      (N₂ ⋙ Γ₂) ⟶
    ((whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (SimplicialObject C))).obj
          (toKaroubi (SimplicialObject C))).obj
      (𝟭 (Karoubi (SimplicialObject C)))
[PROOFSTEP]
exact compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans
[GOAL]
C : Type u_1
inst✝² : Category.{?u.94055, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (N₂ ⋙ Γ₂).obj P ⟶ (𝟭 (Karoubi (SimplicialObject C))).obj P
[PROOFSTEP]
exact (N₂ ⋙ Γ₂).map P.decompId_i ≫ (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ NatTrans.app natTrans P =
    (N₂ ⋙ Γ₂).map (Karoubi.decompId_i P) ≫
      NatTrans.app (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans) P.X ≫ Karoubi.decompId_p P
[PROOFSTEP]
dsimp only [natTrans]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ NatTrans.app
      (((whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (SimplicialObject C))).obj
            (toKaroubi (SimplicialObject C))).preimage
        (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans))
      P =
    (N₂ ⋙ Γ₂).map (Karoubi.decompId_i P) ≫
      NatTrans.app (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans) P.X ≫ Karoubi.decompId_p P
[PROOFSTEP]
rw [whiskeringLeft_obj_preimage_app (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans : _ ⟶ toKaroubi _ ⋙ 𝟭 _) P,
  Functor.id_map]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app Γ₂N₁.natTrans X =
    (compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫ NatTrans.app Γ₂N₂.natTrans ((toKaroubi (SimplicialObject C)).obj X)
[PROOFSTEP]
rw [Γ₂N₂.natTrans_app_f_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app Γ₂N₁.natTrans X =
    (compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫
      (N₂ ⋙ Γ₂).map (Karoubi.decompId_i ((toKaroubi (SimplicialObject C)).obj X)) ≫
        NatTrans.app (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans) ((toKaroubi (SimplicialObject C)).obj X).X ≫
          Karoubi.decompId_p ((toKaroubi (SimplicialObject C)).obj X)
[PROOFSTEP]
dsimp only [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi, Functor.comp_map, NatTrans.comp_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app Γ₂N₁.natTrans X =
    (compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫
      Γ₂.map (N₂.map (𝟙 ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.hom ((toKaroubi (SimplicialObject C)).obj X).X ≫
            NatTrans.app Γ₂N₁.natTrans ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙 (Karoubi.mk ((toKaroubi (SimplicialObject C)).obj X).X (𝟙 ((toKaroubi (SimplicialObject C)).obj X).X))
[PROOFSTEP]
rw [N₂.map_id, Γ₂.map_id, Iso.app_inv]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app Γ₂N₁.natTrans X =
    NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X ≫
      𝟙 (Γ₂.obj (N₂.obj ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.hom ((toKaroubi (SimplicialObject C)).obj X).X ≫
            NatTrans.app Γ₂N₁.natTrans ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙 (Karoubi.mk ((toKaroubi (SimplicialObject C)).obj X).X (𝟙 ((toKaroubi (SimplicialObject C)).obj X).X))
[PROOFSTEP]
dsimp only [toKaroubi]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app Γ₂N₁.natTrans X =
    NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X ≫
      𝟙 (Γ₂.obj (N₂.obj (Karoubi.mk X (𝟙 X)))) ≫
        (NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.hom X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫ 𝟙 (Karoubi.mk X (𝟙 X))
[PROOFSTEP]
erw [id_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app Γ₂N₁.natTrans X =
    NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X ≫
      (NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.hom X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫ 𝟙 (Karoubi.mk X (𝟙 X))
[PROOFSTEP]
rw [comp_id, Iso.inv_hom_id_app_assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ NatTrans.app N₂Γ₂.inv (N₂.obj P) ≫ N₂.map (NatTrans.app Γ₂N₂.natTrans P) = 𝟙 (N₂.obj P)
[PROOFSTEP]
ext n
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P) ≫ N₂.map (NatTrans.app Γ₂N₂.natTrans P)).f n =
    HomologicalComplex.Hom.f (𝟙 (N₂.obj P)).f n
[PROOFSTEP]
have eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op [n]) ≫ (Γ₀.splitting (N₂.obj P).X).ιSummand (Splitting.IndexSet.id (op [n])) :=
  by simp only [N₂Γ₂_inv_app_f_f, N₂_obj_p_f, assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P)).f n =
    HomologicalComplex.Hom.f PInfty n ≫
      NatTrans.app P.p (op [n]) ≫ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
simp only [N₂Γ₂_inv_app_f_f, N₂_obj_p_f, assoc]
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P)).f n =
    HomologicalComplex.Hom.f PInfty n ≫
      NatTrans.app P.p (op [n]) ≫ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n]))
⊢ HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P) ≫ N₂.map (NatTrans.app Γ₂N₂.natTrans P)).f n =
    HomologicalComplex.Hom.f (𝟙 (N₂.obj P)).f n
[PROOFSTEP]
have eq₂ :
  (Γ₀.splitting (N₂.obj P).X).ιSummand (Splitting.IndexSet.id (op [n])) ≫ (N₂.map (Γ₂N₂.natTrans.app P)).f.f n =
    PInfty.f n ≫ P.p.app (op [n]) :=
  by
  dsimp
  simp only [assoc, Γ₂N₂.natTrans_app_f_app, Functor.comp_map, NatTrans.comp_app, Karoubi.comp_f,
    compatibility_Γ₂N₁_Γ₂N₂_hom_app, eqToHom_refl, Karoubi.eqToHom_f, PInfty_on_Γ₀_splitting_summand_eq_self_assoc,
    Functor.comp_obj]
  dsimp [N₂]
  simp only [Splitting.ι_desc_assoc, assoc, id_comp, unop_op, Splitting.IndexSet.id_fst, len_mk, Splitting.IndexSet.e,
    Splitting.IndexSet.id_snd_coe, op_id, P.X.map_id, id_comp, PInfty_f_naturality_assoc, PInfty_f_idem_assoc, app_idem]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P)).f n =
    HomologicalComplex.Hom.f PInfty n ≫
      NatTrans.app P.p (op [n]) ≫ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n]))
⊢ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n])) ≫
      HomologicalComplex.Hom.f (N₂.map (NatTrans.app Γ₂N₂.natTrans P)).f n =
    HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app P.p (op [n])
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P)).f n =
    HomologicalComplex.Hom.f PInfty n ≫
      NatTrans.app P.p (op [n]) ≫ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n]))
⊢ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n])) ≫
      HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app (NatTrans.app Γ₂N₂.natTrans P).f (op [n]) =
    HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app P.p (op [n])
[PROOFSTEP]
simp only [assoc, Γ₂N₂.natTrans_app_f_app, Functor.comp_map, NatTrans.comp_app, Karoubi.comp_f,
  compatibility_Γ₂N₁_Γ₂N₂_hom_app, eqToHom_refl, Karoubi.eqToHom_f, PInfty_on_Γ₀_splitting_summand_eq_self_assoc,
  Functor.comp_obj]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P)).f n =
    HomologicalComplex.Hom.f PInfty n ≫
      NatTrans.app P.p (op [n]) ≫ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n]))
⊢ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n])) ≫
      NatTrans.app
        ((Γ₂.map (N₂.map (Karoubi.decompId_i P))).f ≫
          (Γ₂.obj (N₂.obj (Karoubi.mk P.X (𝟙 P.X)))).p ≫
            𝟙 (Γ₂.obj (N₂.obj (Karoubi.mk P.X (𝟙 P.X)))).X ≫
              (NatTrans.app Γ₂N₁.natTrans P.X).f ≫ (Karoubi.decompId_p P).f)
        (op [n]) =
    HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app P.p (op [n])
[PROOFSTEP]
dsimp [N₂]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P)).f n =
    HomologicalComplex.Hom.f PInfty n ≫
      NatTrans.app P.p (op [n]) ≫ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n]))
⊢ Splitting.ιSummand (Γ₀.splitting K[P.X]) (Splitting.IndexSet.id (op [n])) ≫
      (Splitting.desc (Γ₀.splitting K[P.X]) (op [n]) fun A =>
          (HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ NatTrans.app P.p A.fst) ≫
            Splitting.ιSummand (Γ₀.splitting K[P.X]) A) ≫
        (Splitting.desc (Γ₀.splitting K[P.X]) (op [n]) fun A =>
            (HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ 𝟙 (P.X.obj A.fst)) ≫
              Splitting.ιSummand (Γ₀.splitting K[P.X]) A) ≫
          𝟙 (Γ₀.Obj.obj₂ K[P.X] (op [n])) ≫
            (Splitting.desc (Γ₀.splitting K[P.X]) (op [n]) fun A =>
                HomologicalComplex.Hom.f PInfty (len A.fst.unop) ≫ P.X.map (Splitting.IndexSet.e A).op) ≫
              NatTrans.app P.p (op [n]) =
    HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app P.p (op [n])
[PROOFSTEP]
simp only [Splitting.ι_desc_assoc, assoc, id_comp, unop_op, Splitting.IndexSet.id_fst, len_mk, Splitting.IndexSet.e,
  Splitting.IndexSet.id_snd_coe, op_id, P.X.map_id, id_comp, PInfty_f_naturality_assoc, PInfty_f_idem_assoc, app_idem]
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P)).f n =
    HomologicalComplex.Hom.f PInfty n ≫
      NatTrans.app P.p (op [n]) ≫ Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n]))
eq₂ :
  Splitting.ιSummand (Γ₀.splitting (N₂.obj P).X) (Splitting.IndexSet.id (op [n])) ≫
      HomologicalComplex.Hom.f (N₂.map (NatTrans.app Γ₂N₂.natTrans P)).f n =
    HomologicalComplex.Hom.f PInfty n ≫ NatTrans.app P.p (op [n])
⊢ HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv (N₂.obj P) ≫ N₂.map (NatTrans.app Γ₂N₂.natTrans P)).f n =
    HomologicalComplex.Hom.f (𝟙 (N₂.obj P)).f n
[PROOFSTEP]
simp only [Karoubi.comp_f, HomologicalComplex.comp_f, Karoubi.id_eq, N₂_obj_p_f, assoc, eq₁, eq₂,
  PInfty_f_naturality_assoc, app_idem, PInfty_f_idem_assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ (𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (Functor.associator N₂ Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂ = 𝟙 N₂
[PROOFSTEP]
ext P : 2
[GOAL]
case w.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ NatTrans.app ((𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (Functor.associator N₂ Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂) P = NatTrans.app (𝟙 N₂) P
[PROOFSTEP]
dsimp only [NatTrans.comp_app, NatTrans.hcomp_app, Functor.comp_map, Functor.associator, NatTrans.id_app,
  Functor.comp_obj]
[GOAL]
case w.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (NatTrans.app N₂Γ₂.inv (N₂.obj P) ≫ N₂.map (Γ₂.map (𝟙 (N₂.obj P)))) ≫
      𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (NatTrans.app Γ₂N₂.natTrans P) =
    𝟙 (N₂.obj P)
[PROOFSTEP]
rw [Γ₂.map_id, N₂.map_id, comp_id, id_comp, id_comp, identity_N₂_objectwise P]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.207135, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ IsIso Γ₂N₂.natTrans
[PROOFSTEP]
have : ∀ P : Karoubi (SimplicialObject C), IsIso (Γ₂N₂.natTrans.app P) :=
  by
  intro P
  have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) :=
    by
    have h := identity_N₂_objectwise P
    erw [hom_comp_eq_id] at h
    rw [h]
    infer_instance
  exact isIso_of_reflects_iso _ N₂
[GOAL]
C : Type u_1
inst✝² : Category.{?u.207135, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ ∀ (P : Karoubi (SimplicialObject C)), IsIso (NatTrans.app Γ₂N₂.natTrans P)
[PROOFSTEP]
intro P
[GOAL]
C : Type u_1
inst✝² : Category.{?u.207135, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ IsIso (NatTrans.app Γ₂N₂.natTrans P)
[PROOFSTEP]
have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) :=
  by
  have h := identity_N₂_objectwise P
  erw [hom_comp_eq_id] at h
  rw [h]
  infer_instance
[GOAL]
C : Type u_1
inst✝² : Category.{?u.207135, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ IsIso (N₂.map (NatTrans.app Γ₂N₂.natTrans P))
[PROOFSTEP]
have h := identity_N₂_objectwise P
[GOAL]
C : Type u_1
inst✝² : Category.{?u.207135, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
h : NatTrans.app N₂Γ₂.inv (N₂.obj P) ≫ N₂.map (NatTrans.app Γ₂N₂.natTrans P) = 𝟙 (N₂.obj P)
⊢ IsIso (N₂.map (NatTrans.app Γ₂N₂.natTrans P))
[PROOFSTEP]
erw [hom_comp_eq_id] at h
[GOAL]
C : Type u_1
inst✝² : Category.{?u.207135, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
h : N₂.map (NatTrans.app Γ₂N₂.natTrans P) = inv (NatTrans.app N₂Γ₂.inv (N₂.obj P))
⊢ IsIso (N₂.map (NatTrans.app Γ₂N₂.natTrans P))
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.207135, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
h : N₂.map (NatTrans.app Γ₂N₂.natTrans P) = inv (NatTrans.app N₂Γ₂.inv (N₂.obj P))
⊢ IsIso (inv (NatTrans.app N₂Γ₂.inv (N₂.obj P)))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝² : Category.{?u.207135, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
this : IsIso (N₂.map (NatTrans.app Γ₂N₂.natTrans P))
⊢ IsIso (NatTrans.app Γ₂N₂.natTrans P)
[PROOFSTEP]
exact isIso_of_reflects_iso _ N₂
[GOAL]
C : Type u_1
inst✝² : Category.{?u.207135, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
this : ∀ (P : Karoubi (SimplicialObject C)), IsIso (NatTrans.app Γ₂N₂.natTrans P)
⊢ IsIso Γ₂N₂.natTrans
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
C : Type u_1
inst✝² : Category.{?u.212338, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ IsIso Γ₂N₁.natTrans
[PROOFSTEP]
have : ∀ X : SimplicialObject C, IsIso (Γ₂N₁.natTrans.app X) :=
  by
  intro X
  rw [compatibility_Γ₂N₁_Γ₂N₂_natTrans]
  infer_instance
[GOAL]
C : Type u_1
inst✝² : Category.{?u.212338, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ ∀ (X : SimplicialObject C), IsIso (NatTrans.app Γ₂N₁.natTrans X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u_1
inst✝² : Category.{?u.212338, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ IsIso (NatTrans.app Γ₂N₁.natTrans X)
[PROOFSTEP]
rw [compatibility_Γ₂N₁_Γ₂N₂_natTrans]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.212338, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ IsIso ((compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫ NatTrans.app Γ₂N₂.natTrans ((toKaroubi (SimplicialObject C)).obj X))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝² : Category.{?u.212338, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
this : ∀ (X : SimplicialObject C), IsIso (NatTrans.app Γ₂N₁.natTrans X)
⊢ IsIso Γ₂N₁.natTrans
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app