case mp
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
⊢ f ≫ HomologicalComplex.Hom.f PInfty n = 0 → f ≫ πSummand s (IndexSet.id [n].op) = 0

case mpr
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
⊢ f ≫ πSummand s (IndexSet.id [n].op) = 0 → f ≫ HomologicalComplex.Hom.f PInfty n = 0
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
⊢ f ≫ HomologicalComplex.Hom.f PInfty n = 0 ↔ f ≫ πSummand s (IndexSet.id [n].op) = 0
constructor
case mp
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ HomologicalComplex.Hom.f PInfty n = 0
⊢ f ≫ πSummand s (IndexSet.id [n].op) = 0
case mp
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
⊢ f ≫ HomologicalComplex.Hom.f PInfty n = 0 → f ≫ πSummand s (IndexSet.id [n].op) = 0
intro h
case mp.zero
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
f : Z ⟶ X.obj [Nat.zero].op
h : f ≫ HomologicalComplex.Hom.f PInfty Nat.zero = 0
⊢ f ≫ πSummand s (IndexSet.id [Nat.zero].op) = 0

case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
⊢ f ≫ πSummand s (IndexSet.id [Nat.succ n].op) = 0
case mp
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ HomologicalComplex.Hom.f PInfty n = 0
⊢ f ≫ πSummand s (IndexSet.id [n].op) = 0
rcases n with _|n
case mp.zero
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
f : Z ⟶ X.obj [Nat.zero].op
h : f ≫ 𝟙 (X.obj [0].op) = 0
⊢ f ≫ πSummand s (IndexSet.id [Nat.zero].op) = 0
case mp.zero
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
f : Z ⟶ X.obj [Nat.zero].op
h : f ≫ HomologicalComplex.Hom.f PInfty Nat.zero = 0
⊢ f ≫ πSummand s (IndexSet.id [Nat.zero].op) = 0
dsimp at h
case mp.zero
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
f : Z ⟶ X.obj [Nat.zero].op
h : f = 0
⊢ f ≫ πSummand s (IndexSet.id [Nat.zero].op) = 0
case mp.zero
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
f : Z ⟶ X.obj [Nat.zero].op
h : f ≫ 𝟙 (X.obj [0].op) = 0
⊢ f ≫ πSummand s (IndexSet.id [Nat.zero].op) = 0
rw [comp_id] at h
no goals
case mp.zero
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
f : Z ⟶ X.obj [Nat.zero].op
h : f = 0
⊢ f ≫ πSummand s (IndexSet.id [Nat.zero].op) = 0
rw [h, zero_comp]
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' :
  f ≫ (HomologicalComplex.Hom.f PInfty (n + 1) + HomologicalComplex.Hom.f QInfty (n + 1)) =
    f ≫ 𝟙 (HomologicalComplex.X K[X] (n + 1))
⊢ f ≫ πSummand s (IndexSet.id [Nat.succ n].op) = 0
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
⊢ f ≫ πSummand s (IndexSet.id [Nat.succ n].op) = 0
have h' := f ≫= PInfty_f_add_QInfty_f (n + 1)
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' : f ≫ (HomologicalComplex.Hom.f PInfty (n + 1) + HomologicalComplex.Hom.f QInfty (n + 1)) = f ≫ 𝟙 (X.obj [n + 1].op)
⊢ f ≫ πSummand s (IndexSet.id [Nat.succ n].op) = 0
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' :
  f ≫ (HomologicalComplex.Hom.f PInfty (n + 1) + HomologicalComplex.Hom.f QInfty (n + 1)) =
    f ≫ 𝟙 (HomologicalComplex.X K[X] (n + 1))
⊢ f ≫ πSummand s (IndexSet.id [Nat.succ n].op) = 0
dsimp at h'
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
⊢ f ≫ πSummand s (IndexSet.id [Nat.succ n].op) = 0
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' : f ≫ (HomologicalComplex.Hom.f PInfty (n + 1) + HomologicalComplex.Hom.f QInfty (n + 1)) = f ≫ 𝟙 (X.obj [n + 1].op)
⊢ f ≫ πSummand s (IndexSet.id [Nat.succ n].op) = 0
rw [comp_id, comp_add, h, zero_add] at h'
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
⊢ ∀ (x : Fin (n + 1)),
    x ∈ Finset.filter (fun i => ↑i < n + 1) Finset.univ →
      f ≫
          (HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
              SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ SimplicialObject.σ X (↑Fin.rev x)) ≫
            πSummand s (IndexSet.id [Nat.succ n].op) =
        0
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
⊢ f ≫ πSummand s (IndexSet.id [Nat.succ n].op) = 0
rw [← h', assoc, QInfty_f, decomposition_Q, Preadditive.sum_comp, Preadditive.comp_sum,
  Finset.sum_eq_zero]
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
i : Fin (n + 1)
a✝ : i ∈ Finset.filter (fun i => ↑i < n + 1) Finset.univ
⊢ f ≫
      (HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)) ≫
        πSummand s (IndexSet.id [Nat.succ n].op) =
    0
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
⊢ ∀ (x : Fin (n + 1)),
    x ∈ Finset.filter (fun i => ↑i < n + 1) Finset.univ →
      f ≫
          (HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
              SimplicialObject.δ X (Fin.succ (↑Fin.rev x)) ≫ SimplicialObject.σ X (↑Fin.rev x)) ≫
            πSummand s (IndexSet.id [Nat.succ n].op) =
        0
intro i _
no goals
case mp.succ
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [Nat.succ n].op
h : f ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n) = 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
i : Fin (n + 1)
a✝ : i ∈ Finset.filter (fun i => ↑i < n + 1) Finset.univ
⊢ f ≫
      (HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.rev i)) ≫ SimplicialObject.σ X (↑Fin.rev i)) ≫
        πSummand s (IndexSet.id [Nat.succ n].op) =
    0
simp only [assoc, σ_comp_πSummand_id_eq_zero, comp_zero]
case mpr
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
⊢ f ≫ HomologicalComplex.Hom.f PInfty n = 0
case mpr
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
⊢ f ≫ πSummand s (IndexSet.id [n].op) = 0 → f ≫ HomologicalComplex.Hom.f PInfty n = 0
intro h
case mpr.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
⊢ ∀ (a : IndexSet [n].op), f ≫ (πSummand s a ≫ ιSummand s a) ≫ HomologicalComplex.Hom.f PInfty n = 0
case mpr
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
⊢ f ≫ HomologicalComplex.Hom.f PInfty n = 0
rw [← comp_id f, assoc, s.decomposition_id, Preadditive.sum_comp, Preadditive.comp_sum,
  Fintype.sum_eq_zero]
case mpr.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
A : IndexSet [n].op
⊢ f ≫ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0
case mpr.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
⊢ ∀ (a : IndexSet [n].op), f ≫ (πSummand s a ≫ ιSummand s a) ≫ HomologicalComplex.Hom.f PInfty n = 0
intro A
case pos
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
A : IndexSet [n].op
hA : IndexSet.EqId A
⊢ f ≫ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0

case neg
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
A : IndexSet [n].op
hA : ¬IndexSet.EqId A
⊢ f ≫ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0
case mpr.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
A : IndexSet [n].op
⊢ f ≫ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0
by_cases hA : A.EqId
case pos
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
A : IndexSet [n].op
hA : A = IndexSet.id [n].op
⊢ f ≫ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0
case pos
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
A : IndexSet [n].op
hA : IndexSet.EqId A
⊢ f ≫ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0
dsimp at hA
case pos
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
⊢ f ≫ (πSummand s (IndexSet.id [n].op) ≫ ιSummand s (IndexSet.id [n].op)) ≫ HomologicalComplex.Hom.f PInfty n = 0
case pos
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
A : IndexSet [n].op
hA : A = IndexSet.id [n].op
⊢ f ≫ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0
subst hA
no goals
case pos
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
⊢ f ≫ (πSummand s (IndexSet.id [n].op) ≫ ιSummand s (IndexSet.id [n].op)) ≫ HomologicalComplex.Hom.f PInfty n = 0
rw [assoc, reassoc_of% h, zero_comp]
no goals
case neg
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X.obj [n].op
h : f ≫ πSummand s (IndexSet.id [n].op) = 0
A : IndexSet [n].op
hA : ¬IndexSet.EqId A
⊢ f ≫ (πSummand s A ≫ ιSummand s A) ≫ HomologicalComplex.Hom.f PInfty n = 0
simp only [assoc, s.ιSummand_comp_PInfty_eq_zero A hA, comp_zero]