[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) ↔ i = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) → i = 0
[PROOFSTEP]
rintro ⟨_, h₂⟩
[GOAL]
case mp.intro
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
left✝ : len [j + 1] = len [j] + 1
h₂ : ↑(Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
⊢ i = 0
[PROOFSTEP]
by_contra h
[GOAL]
case mp.intro
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
left✝ : len [j + 1] = len [j] + 1
h₂ : ↑(Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
h : ¬i = 0
⊢ False
[PROOFSTEP]
exact h₂ (Fin.succAbove_ne_zero_zero h)
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ i = 0 → Isδ₀ (SimplexCategory.δ i)
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)
[PROOFSTEP]
exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ ↑(Hom.toOrderHom (SimplexCategory.δ 0)) 0 ≠ 0
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ ¬↑(Hom.toOrderHom (SimplexCategory.δ 0)) 0 = 0
[PROOFSTEP]
exact Fin.succ_ne_zero (0 : Fin (j + 1))
[GOAL]
C : Type u_1
inst✝² : Category.{?u.2609, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
n : ℕ
i : [n] ⟶ [n + 1]
inst✝ : Mono i
hi : Isδ₀ i
⊢ i = SimplexCategory.δ 0
[PROOFSTEP]
obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono i
[GOAL]
case intro
C : Type u_1
inst✝² : Category.{?u.2609, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : Isδ₀ (SimplexCategory.δ j)
⊢ SimplexCategory.δ j = SimplexCategory.δ 0
[PROOFSTEP]
rw [iff] at hi
[GOAL]
case intro
C : Type u_1
inst✝² : Category.{?u.2609, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : j = 0
⊢ SimplexCategory.δ j = SimplexCategory.δ 0
[PROOFSTEP]
rw [hi]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
by_cases Δ = Δ'
[GOAL]
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
by_cases Δ = Δ'
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h : Δ = Δ'
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
exact eqToHom (by congr)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h : Δ = Δ'
⊢ HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ')
[PROOFSTEP]
congr
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h : ¬Δ = Δ'
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
by_cases Isδ₀ i
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h : ¬Δ = Δ'
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
by_cases Isδ₀ i
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : ¬Δ = Δ'
h : Isδ₀ i
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
exact K.d Δ.len Δ'.len
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : ¬Δ = Δ'
h : ¬Isδ₀ i
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
exact 0
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
⊢ mapMono K (𝟙 Δ) = 𝟙 (HomologicalComplex.X K (len Δ))
[PROOFSTEP]
unfold mapMono
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
⊢ (if h : Δ = Δ then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ))
    else if h : Isδ₀ (𝟙 Δ) then HomologicalComplex.d K (len Δ) (len Δ) else 0) =
    𝟙 (HomologicalComplex.X K (len Δ))
[PROOFSTEP]
simp only [eq_self_iff_true, eqToHom_refl, dite_eq_ite, if_true]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ mapMono K i = HomologicalComplex.d K (len Δ) (len Δ')
[PROOFSTEP]
unfold mapMono
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ'))
    else if h : Isδ₀ i then HomologicalComplex.d K (len Δ) (len Δ') else 0) =
    HomologicalComplex.d K (len Δ) (len Δ')
[PROOFSTEP]
suffices Δ ≠ Δ' by simp only [dif_neg this, dif_pos hi]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
this : Δ ≠ Δ'
⊢ (if h : Δ = Δ' then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ'))
    else if h : Isδ₀ i then HomologicalComplex.d K (len Δ) (len Δ') else 0) =
    HomologicalComplex.d K (len Δ) (len Δ')
[PROOFSTEP]
simp only [dif_neg this, dif_pos hi]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ Δ ≠ Δ'
[PROOFSTEP]
rintro rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ'' : SimplexCategory
i : Δ ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ False
[PROOFSTEP]
simpa only [self_eq_add_right, Nat.one_ne_zero] using hi.1
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
n : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)
[PROOFSTEP]
rw [Isδ₀.iff]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ mapMono K i = 0
[PROOFSTEP]
unfold mapMono
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ'))
    else if h : Isδ₀ i then HomologicalComplex.d K (len Δ) (len Δ') else 0) =
    0
[PROOFSTEP]
rw [Ne.def] at h₁
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ'))
    else if h : Isδ₀ i then HomologicalComplex.d K (len Δ) (len Δ') else 0) =
    0
[PROOFSTEP]
split_ifs
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ mapMono K i ≫ HomologicalComplex.Hom.f f (len Δ) = HomologicalComplex.Hom.f f (len Δ') ≫ mapMono K' i
[PROOFSTEP]
unfold mapMono
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ (if h : Δ' = Δ then eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ))
      else if h : Isδ₀ i then HomologicalComplex.d K (len Δ') (len Δ) else 0) ≫
      HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫
      if h : Δ' = Δ then eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ))
      else if h : Isδ₀ i then HomologicalComplex.d K' (len Δ') (len Δ) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : Δ' = Δ
⊢ eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ)) ≫ HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫
      eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ))
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ'
inst✝ : Mono i
⊢ eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ')) ≫
      HomologicalComplex.Hom.f f (len Δ') =
    HomologicalComplex.Hom.f f (len Δ') ≫
      eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ'))
[PROOFSTEP]
simp only [id_comp, eqToHom_refl, comp_id]
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ HomologicalComplex.d K (len Δ') (len Δ) ≫ HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫ HomologicalComplex.d K' (len Δ') (len Δ)
[PROOFSTEP]
rw [HomologicalComplex.Hom.comm]
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : ¬Isδ₀ i
⊢ 0 ≫ HomologicalComplex.Hom.f f (len Δ) = HomologicalComplex.Hom.f f (len Δ') ≫ 0
[PROOFSTEP]
rw [zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
by_cases h₁ : Δ = Δ'
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
subst h₁
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ
i : Δ ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
simp only [SimplexCategory.eq_id_of_mono i, comp_id, id_comp, mapMono_id K, eqToHom_refl]
  -- case where i' : Δ'' ⟶ Δ' is the identity
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
by_cases h₂ : Δ' = Δ''
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
subst h₂
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝¹ : Mono i
h₁ : ¬Δ = Δ'
i' : Δ' ⟶ Δ'
inst✝ : Mono i'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
simp only [SimplexCategory.eq_id_of_mono i', comp_id, id_comp, mapMono_id K, eqToHom_refl]
  -- then the RHS is always zero
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i h₁)
[GOAL]
case neg.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
obtain ⟨k', hk'⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i' h₂)
[GOAL]
case neg.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
have eq : Δ.len = Δ''.len + (k + k' + 2) := by linarith
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
⊢ len Δ = len Δ'' + (k + k' + 2)
[PROOFSTEP]
linarith
[GOAL]
case neg.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
rw [mapMono_eq_zero K (i' ≫ i) _ _]
[GOAL]
case neg.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ Δ ≠ Δ''
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)
[PROOFSTEP]
rotate_left
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ Δ ≠ Δ''
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h : Δ = Δ''
⊢ False
[PROOFSTEP]
simp only [self_eq_add_right, h, add_eq_zero_iff, and_false] at eq
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h : Isδ₀ (i' ≫ i)
⊢ False
[PROOFSTEP]
simp only [h.1, add_right_inj] at eq
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
h : Isδ₀ (i' ≫ i)
eq : 1 = k + k' + 2
⊢ False
[PROOFSTEP]
linarith
  -- in all cases, the LHS is also zero, either by definition, or because d ≫ d = 0
[GOAL]
case neg.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
by_cases h₃ : Isδ₀ i
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
by_cases h₄ : Isδ₀ i'
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : ¬Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
simp only [mapMono_eq_zero K i' h₂ h₄, comp_zero]
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : ¬Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
simp only [mapMono_eq_zero K i h₁ h₃, zero_comp]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Sigma.ι (summand K Δ) A ≫ map K θ = Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
[PROOFSTEP]
simp only [map, colimit.ι_desc, Cofan.mk_ι_app]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
[PROOFSTEP]
have h := SimplexCategory.image_eq fac
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
h : image (θ.unop ≫ Splitting.IndexSet.e A) = Δ''
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_i
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ image.ι (θ.unop ≫ Splitting.IndexSet.e A) = i
[PROOFSTEP]
exact SimplexCategory.image_ι_eq fac
[GOAL]
case e_a.h.e_6.h
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.IndexSet.pull A θ = Splitting.IndexSet.mk e
[PROOFSTEP]
dsimp only [SimplicialObject.Splitting.IndexSet.pull]
[GOAL]
case e_a.h.e_6.h
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ Splitting.IndexSet.e A)) = Splitting.IndexSet.mk e
[PROOFSTEP]
congr
[GOAL]
case e_a.h.e_6.h.e_f
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ factorThruImage (θ.unop ≫ Splitting.IndexSet.e A) = e
[PROOFSTEP]
exact SimplexCategory.factorThruImage_eq fac
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (𝟙 Δ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫
      𝟙 ({ obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.obj Δ)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)
[PROOFSTEP]
have fac : A.e ≫ 𝟙 A.1.unop = (𝟙 Δ).unop ≫ A.e := by rw [unop_id, comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ Splitting.IndexSet.e A ≫ 𝟙 A.fst.unop = (𝟙 Δ).unop ≫ Splitting.IndexSet.e A
[PROOFSTEP]
rw [unop_id, comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : Splitting.IndexSet.e A ≫ 𝟙 A.fst.unop = (𝟙 Δ).unop ≫ Splitting.IndexSet.e A
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)
[PROOFSTEP]
erw [Obj.map_on_summand₀ K A fac, Obj.Termwise.mapMono_id, id_comp, comp_id]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : Splitting.IndexSet.e A ≫ 𝟙 A.fst.unop = (𝟙 Δ).unop ≫ Splitting.IndexSet.e A
⊢ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk (Splitting.IndexSet.e A)) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A }
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ' ≫
        { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ
[PROOFSTEP]
have fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e := by rw [unop_comp, assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ θ.unop ≫ θ'.unop ≫ Splitting.IndexSet.e A = (θ' ≫ θ).unop ≫ Splitting.IndexSet.e A
[PROOFSTEP]
rw [unop_comp, assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac : θ.unop ≫ θ'.unop ≫ Splitting.IndexSet.e A = (θ' ≫ θ).unop ≫ Splitting.IndexSet.e A
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ' ≫
        { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ
[PROOFSTEP]
rw [← image.fac (θ'.unop ≫ A.e), ← assoc, ← image.fac (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)), assoc] at fac
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
      image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
        image.ι (θ'.unop ≫ Splitting.IndexSet.e A) =
    (θ' ≫ θ).unop ≫ Splitting.IndexSet.e A
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ' ≫
        { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ
[PROOFSTEP]
simp only [Obj.map_on_summand₀'_assoc K A θ', Obj.map_on_summand₀' K _ θ, Obj.Termwise.mapMono_comp_assoc,
  Obj.map_on_summand₀ K A fac]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
      image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
        image.ι (θ'.unop ≫ Splitting.IndexSet.e A) =
    (θ' ≫ θ).unop ≫ Splitting.IndexSet.e A
⊢ Obj.Termwise.mapMono K
        (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
          image.ι (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (Obj.summand K Δ)
        (Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)))) =
    Obj.Termwise.mapMono K
        (image.ι (θ.unop ≫ Splitting.IndexSet.e (Splitting.IndexSet.pull A θ')) ≫
          image.ι (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.pull (Splitting.IndexSet.pull A θ') θ)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) Δ))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K (op [n])) (Splitting.IndexSet.id (op [n]))) Δ =
    colimit.ι
        (Discrete.functor (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) Δ))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) Δ)
[PROOFSTEP]
induction' Δ using Opposite.rec' with Δ
[GOAL]
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝¹ : Discrete (Splitting.IndexSet Δ✝)
A✝ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝ : Discrete (Splitting.IndexSet (op Δ))
A : Splitting.IndexSet (op Δ)
⊢ colimit.ι
        (Discrete.functor (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op Δ)))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K (op [n])) (Splitting.IndexSet.id (op [n]))) (op Δ) =
    colimit.ι
        (Discrete.functor (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op Δ)))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (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
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ colimit.ι
        (Discrete.functor
          (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n])))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K (op [n])) (Splitting.IndexSet.id (op [n]))) (op [n]) =
    colimit.ι
        (Discrete.functor
          (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n])))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n]))
[PROOFSTEP]
dsimp [Splitting.map]
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ (colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      Sigma.desc fun A =>
        Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K (Splitting.IndexSet.e A).op) =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n]))
[PROOFSTEP]
simp only [colimit.ι_desc, Cofan.mk_ι_app, Γ₀.obj_map]
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K (Splitting.IndexSet.e A).op =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n]))
[PROOFSTEP]
erw [Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1) (show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl),
  Γ₀.Obj.Termwise.mapMono_id, A.ext', id_comp, comp_id]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ Splitting.IndexSet.e A ≫ 𝟙 A.fst.unop = (Splitting.IndexSet.e A).op.unop ≫ 𝟙 (op A.fst.unop).unop
[PROOFSTEP]
rfl
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ Sigma.ι (Obj.summand K (op [n]))
      (Splitting.IndexSet.mk
        (Splitting.IndexSet.e
          { fst := A.fst, snd := { val := Splitting.IndexSet.e A, property := (_ : Epi ↑A.snd) } })) =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst))
      { as := { fst := A.fst, snd := { val := Splitting.IndexSet.e A, property := (_ : Epi ↑A.snd) } } }
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{?u.135855, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
⊢ IsIso (Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K (op [n])) (Splitting.IndexSet.id (op [n]))) Δ)
[PROOFSTEP]
rw [Γ₀.splitting_map_eq_id]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.135855, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
⊢ IsIso (𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) Δ))
[PROOFSTEP]
apply IsIso.id
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.ιSummand (splitting K) A ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ Splitting.ιSummand (splitting K) (Splitting.IndexSet.mk e)
[PROOFSTEP]
dsimp only [SimplicialObject.Splitting.ιSummand, SimplicialObject.Splitting.ιCoprod]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ (Sigma.ι (Splitting.summand (splitting K).N Δ) A ≫ (Splitting.iso (splitting K) Δ).hom) ≫ (obj K).map θ =
    Termwise.mapMono K i ≫
      Sigma.ι (Splitting.summand (splitting K).N (op Δ'.unop)) (Splitting.IndexSet.mk e) ≫
        (Splitting.iso (splitting K) (op Δ'.unop)).hom
[PROOFSTEP]
simp only [assoc, Γ₀.splitting_iso_hom_eq_id, id_comp, comp_id]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Sigma.ι (Splitting.summand (splitting K).N Δ) A ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ Sigma.ι (Splitting.summand (splitting K).N (op Δ'.unop)) (Splitting.IndexSet.mk e)
[PROOFSTEP]
exact Γ₀.Obj.map_on_summand₀ K A fac
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ Splitting.ιSummand (splitting K) A ≫ (obj K).map θ =
    Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Splitting.ιSummand (splitting K) (Splitting.IndexSet.pull A θ)
[PROOFSTEP]
apply Obj.map_on_summand
[GOAL]
case fac
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ factorThruImage (θ.unop ≫ Splitting.IndexSet.e A) ≫ image.ι (θ.unop ≫ Splitting.IndexSet.e A) =
    θ.unop ≫ Splitting.IndexSet.e A
[PROOFSTEP]
apply image.fac
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝¹ : HasFiniteCoproducts C
Δ Δ' : SimplexCategory
e : Δ' ⟶ Δ
inst✝ : Epi e
⊢ Splitting.ιSummand (splitting K) (Splitting.IndexSet.id (op Δ)) ≫ (obj K).map e.op =
    Splitting.ιSummand (splitting K) (Splitting.IndexSet.mk e)
[PROOFSTEP]
simpa only [Γ₀.Obj.map_on_summand K (Splitting.IndexSet.id (op Δ)) e.op (rfl : e ≫ 𝟙 Δ = e ≫ 𝟙 Δ),
  Γ₀.Obj.Termwise.mapMono_id] using id_comp _
[GOAL]
C : Type u_1
inst✝² : Category.{?u.164164, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
⊢ (obj K).map θ ≫
      (fun Δ =>
          Splitting.desc (splitting K) Δ fun A =>
            HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
        Δ =
    (fun Δ =>
          Splitting.desc (splitting K) Δ fun A =>
            HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
        Δ' ≫
      (obj K').map θ
[PROOFSTEP]
apply (Γ₀.splitting K).hom_ext'
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.164164, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
⊢ ∀ (A : Splitting.IndexSet Δ'),
    Splitting.ιSummand (splitting K) A ≫
        (obj K).map θ ≫
          (fun Δ =>
              Splitting.desc (splitting K) Δ fun A =>
                HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
            Δ =
      Splitting.ιSummand (splitting K) A ≫
        (fun Δ =>
              Splitting.desc (splitting K) Δ fun A =>
                HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
            Δ' ≫
          (obj K').map θ
[PROOFSTEP]
intro A
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.164164, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
A : Splitting.IndexSet Δ'
⊢ Splitting.ιSummand (splitting K) A ≫
      (obj K).map θ ≫
        (fun Δ =>
            Splitting.desc (splitting K) Δ fun A =>
              HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
          Δ =
    Splitting.ιSummand (splitting K) A ≫
      (fun Δ =>
            Splitting.desc (splitting K) Δ fun A =>
              HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
          Δ' ≫
        (obj K').map θ
[PROOFSTEP]
simp only [(splitting K).ι_desc_assoc, Obj.map_on_summand'_assoc K _ θ, (splitting K).ι_desc, assoc,
  Obj.map_on_summand' K' _ θ]
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.164164, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
A : Splitting.IndexSet Δ'
⊢ Obj.Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      HomologicalComplex.Hom.f f (len (Splitting.IndexSet.pull A θ).fst.unop) ≫
        Splitting.ιSummand (splitting K') (Splitting.IndexSet.pull A θ) =
    HomologicalComplex.Hom.f f (len A.fst.unop) ≫
      Obj.Termwise.mapMono K' (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
        Splitting.ιSummand (splitting K') (Splitting.IndexSet.pull A θ)
[PROOFSTEP]
apply Obj.Termwise.mapMono_naturality_assoc
[GOAL]
C : Type u_1
inst✝² : Category.{?u.167032, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
n : ℕ
⊢ Splitting.ι ((fun K => Split.mk' (Γ₀.splitting K)) K).s n ≫ NatTrans.app (Γ₀.map f) (op [n]) =
    HomologicalComplex.Hom.f f n ≫ Splitting.ι ((fun K => Split.mk' (Γ₀.splitting K)) K').s n
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.167032, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
n : ℕ
⊢ (Splitting.ι (Γ₀.splitting K) n ≫
      Splitting.desc (Γ₀.splitting K) (op [n]) fun A =>
        HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (Γ₀.splitting K') A) =
    HomologicalComplex.Hom.f f n ≫ Splitting.ι (Γ₀.splitting K') n
[PROOFSTEP]
simp only [← Splitting.ιSummand_id, (Γ₀.splitting K).ι_desc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.167032, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
n : ℕ
⊢ HomologicalComplex.Hom.f f (len (Splitting.IndexSet.id (op [n])).fst.unop) ≫
      Splitting.ιSummand (Γ₀.splitting K') (Splitting.IndexSet.id (op [n])) =
    HomologicalComplex.Hom.f f n ≫ Splitting.ιSummand (Γ₀.splitting K') (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HigherFacesVanish (n + 1) (Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])))
[PROOFSTEP]
intro j _
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
[PROOFSTEP]
have eq := Γ₀.Obj.mapMono_on_summand_id K (SimplexCategory.δ j.succ)
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
[PROOFSTEP]
rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
case h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ [n + 1] ≠ [n]
case h₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ ¬Isδ₀ (SimplexCategory.δ (Fin.succ j))
[PROOFSTEP]
rotate_left
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ [n + 1] ≠ [n]
[PROOFSTEP]
intro h
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
h : [n + 1] = [n]
⊢ False
[PROOFSTEP]
exact (Nat.succ_ne_self n) (congr_arg SimplexCategory.len h)
[GOAL]
case h₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ ¬Isδ₀ (SimplexCategory.δ (Fin.succ j))
[PROOFSTEP]
exact fun h => Fin.succ_ne_zero j (by simpa only [Isδ₀.iff] using h)
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
h : Isδ₀ (SimplexCategory.δ (Fin.succ j))
⊢ Fin.succ j = 0
[PROOFSTEP]
simpa only [Isδ₀.iff] using h
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
[PROOFSTEP]
exact eq
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) ≫ HomologicalComplex.Hom.f PInfty n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
rw [PInfty_f]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) ≫ HomologicalComplex.Hom.f (P n) n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case zero
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [Nat.zero])) ≫
      HomologicalComplex.Hom.f (P Nat.zero) Nat.zero =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [Nat.zero]))
[PROOFSTEP]
simpa only [P_f_0_eq] using comp_id _
[GOAL]
case succ
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [Nat.succ n])) ≫
      HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n) =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [Nat.succ n]))
[PROOFSTEP]
exact (HigherFacesVanish.on_Γ₀_summand_id K n).comp_P_eq_self


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.28, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
⊢ b < n + 1 + 1
[PROOFSTEP]
simp only [hnbq, Nat.lt_add_one_iff, le_add_iff_nonneg_right, zero_le]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ (φ ≫ SimplicialObject.σ X { val := b, isLt := (_ : b < n + 1 + 1) }) ≫ SimplicialObject.δ X (Fin.succ j) = 0
[PROOFSTEP]
rw [assoc, SimplicialObject.δ_comp_σ_of_gt', Fin.pred_succ, v.comp_δ_eq_zero_assoc _ _ hj, zero_comp]
[GOAL]
case H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ Fin.succ { val := b, isLt := (_ : b < n + 1 + 1) } < Fin.succ j
[PROOFSTEP]
dsimp
[GOAL]
case H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ { val := b + 1, isLt := (_ : Nat.succ b < Nat.succ (n + 2)) } < Fin.succ j
[PROOFSTEP]
rw [Fin.lt_iff_val_lt_val, Fin.val_succ]
[GOAL]
case H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ↑{ val := b + 1, isLt := (_ : Nat.succ b < Nat.succ (n + 2)) } < ↑j + 1
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ j ≠ 0
[PROOFSTEP]
intro hj'
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
hj' : j = 0
⊢ False
[PROOFSTEP]
simp only [hnbq, add_comm b, add_assoc, hj', Fin.val_zero, zero_add, add_le_iff_nonpos_right, nonpos_iff_eq_zero,
  add_eq_zero, false_and] at hj
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
[PROOFSTEP]
revert i hi
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
⊢ ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ∀ (i : Fin (n + 1)),
    n + 1 ≤ ↑i + Nat.zero → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = 0
[PROOFSTEP]
intro i (hi : n + 1 ≤ i)
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = 0
[PROOFSTEP]
exfalso
[GOAL]
case zero.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i
⊢ False
[PROOFSTEP]
linarith [Fin.is_lt i]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
⊢ ∀ (i : Fin (n + 1)),
    n + 1 ≤ ↑i + Nat.succ q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
intro i (hi : n + 1 ≤ i + q + 1)
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
by_cases n + 1 ≤ (i : ℕ) + q
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
by_cases n + 1 ≤ (i : ℕ) + q
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
h : n + 1 ≤ ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
h : ¬n + 1 ≤ ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
replace hi : n = i + q := by
  obtain ⟨j, hj⟩ := le_iff_exists_add.mp hi
  rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, hj, not_lt, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at h
  rw [← add_left_inj 1, hj, self_eq_add_right, h]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
h : ¬n + 1 ≤ ↑i + q
⊢ n = ↑i + q
[PROOFSTEP]
obtain ⟨j, hj⟩ := le_iff_exists_add.mp hi
[GOAL]
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
h : ¬n + 1 ≤ ↑i + q
j : ℕ
hj : ↑i + q + 1 = n + 1 + j
⊢ n = ↑i + q
[PROOFSTEP]
rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, hj, not_lt, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at h
[GOAL]
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
j : ℕ
h : j = 0
hj : ↑i + q + 1 = n + 1 + j
⊢ n = ↑i + q
[PROOFSTEP]
rw [← add_left_inj 1, hj, self_eq_add_right, h]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
h : ¬n + 1 ≤ ↑i + q
hi : n = ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case neg.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
i : Fin (Nat.zero + 1)
h : ¬Nat.zero + 1 ≤ ↑i + q
hi : Nat.zero = ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (Nat.zero + 1) = 0
[PROOFSTEP]
fin_cases i
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬Nat.zero + 1 ≤ ↑{ val := 0, isLt := (_ : 0 < Nat.zero + 1) } + q
hi : Nat.zero = ↑{ val := 0, isLt := (_ : 0 < Nat.zero + 1) } + q
⊢ SimplicialObject.σ X { val := 0, isLt := (_ : 0 < Nat.zero + 1) } ≫
      HomologicalComplex.Hom.f (P (Nat.succ q)) (Nat.zero + 1) =
    0
[PROOFSTEP]
dsimp at h hi
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X { val := 0, isLt := (_ : 0 < Nat.zero + 1) } ≫
      HomologicalComplex.Hom.f (P (Nat.succ q)) (Nat.zero + 1) =
    0
[PROOFSTEP]
rw [show q = 0 by linarith]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ q = 0
[PROOFSTEP]
linarith
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X { val := 0, isLt := (_ : 0 < Nat.zero + 1) } ≫
      HomologicalComplex.Hom.f (P (Nat.succ 0)) (Nat.zero + 1) =
    0
[PROOFSTEP]
change X.σ 0 ≫ (P 1).f 1 = 0
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 ≫ HomologicalComplex.Hom.f (P 1) 1 = 0
[PROOFSTEP]
simp only [P_succ, HomologicalComplex.add_f_apply, comp_add, HomologicalComplex.id_f,
  AlternatingFaceMapComplex.obj_d_eq, Hσ, HomologicalComplex.comp_f,
  Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl), comp_id]
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 ≫ HomologicalComplex.Hom.f (P 0) 1 +
      (SimplicialObject.σ X 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            (Finset.sum Finset.univ fun i => (-1) ^ ↑i • SimplicialObject.δ X i) ≫
              hσ' 0 0 1 (_ : ComplexShape.Rel c 1 0) +
        SimplicialObject.σ X 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            hσ' 0 1 2 (_ : ComplexShape.Rel c 2 1) ≫
              Finset.sum Finset.univ fun i => (-1) ^ ↑i • SimplicialObject.δ X i) =
    0
[PROOFSTEP]
erw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm, comp_id, Fin.sum_univ_two, Fin.sum_univ_succ,
  Fin.sum_univ_two]
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 +
      (SimplicialObject.σ X 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            ((-1) ^ ↑0 • SimplicialObject.δ X 0 + (-1) ^ ↑1 • SimplicialObject.δ X 1) ≫
              ((-1) ^ 0 • SimplicialObject.σ X { val := 0, isLt := (_ : 0 < Nat.succ 0) }) +
        SimplicialObject.σ X 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            ((-1) ^ 1 • SimplicialObject.σ X { val := 1, isLt := (_ : 1 < Nat.succ 1) }) ≫
              ((-1) ^ ↑0 • SimplicialObject.δ X 0 +
                ((-1) ^ ↑(Fin.succ 0) • SimplicialObject.δ X (Fin.succ 0) +
                  (-1) ^ ↑(Fin.succ 1) • SimplicialObject.δ X (Fin.succ 1)))) =
    0
[PROOFSTEP]
simp only [Fin.val_zero, pow_zero, pow_one, pow_add, one_smul, neg_smul, Fin.mk_one, Fin.val_succ, Fin.val_one,
  Fin.succ_one_eq_two, P_zero, HomologicalComplex.id_f, Fin.val_two, pow_two, mul_neg, one_mul, neg_mul, neg_neg,
  id_comp, add_comp, comp_add, Fin.mk_zero, neg_comp, comp_neg, Fin.succ_zero_eq_one]
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 +
      (SimplicialObject.σ X 0 ≫ SimplicialObject.δ X 0 ≫ SimplicialObject.σ X 0 +
          -SimplicialObject.σ X 0 ≫ SimplicialObject.δ X 1 ≫ SimplicialObject.σ X 0 +
        (-SimplicialObject.σ X 0 ≫ SimplicialObject.σ X 1 ≫ SimplicialObject.δ X 0 +
          (SimplicialObject.σ X 0 ≫ SimplicialObject.σ X 1 ≫ SimplicialObject.δ X 1 +
            -SimplicialObject.σ X 0 ≫ SimplicialObject.σ X 1 ≫ SimplicialObject.δ X 2))) =
    0
[PROOFSTEP]
erw [SimplicialObject.δ_comp_σ_self, SimplicialObject.δ_comp_σ_self_assoc, SimplicialObject.δ_comp_σ_succ, comp_id,
  SimplicialObject.δ_comp_σ_of_le X (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
  SimplicialObject.δ_comp_σ_self_assoc, SimplicialObject.δ_comp_σ_succ_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ 0 ≤ Fin.castSucc 0
[PROOFSTEP]
rw [Fin.castSucc_zero]
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 +
      (SimplicialObject.σ X 0 + -SimplicialObject.σ X 0 +
        (-SimplicialObject.σ X 0 + (SimplicialObject.σ X 0 + -SimplicialObject.σ X 0))) =
    0
[PROOFSTEP]
simp only [add_right_neg, add_zero, zero_add]
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (Nat.succ n + 1) = 0
[PROOFSTEP]
rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp, P_succ]
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
⊢ (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i) ≫
        HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) +
      (HomologicalComplex.Hom.f (Q q) (Nat.succ n) ≫ SimplicialObject.σ X i) ≫
        HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) := (HigherFacesVanish.of_P q n).comp_σ hi
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
⊢ (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i) ≫
        HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) +
      (HomologicalComplex.Hom.f (Q q) (Nat.succ n) ≫ SimplicialObject.σ X i) ≫
        HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
erw [← assoc, v.comp_P_eq_self, HomologicalComplex.add_f_apply, Preadditive.comp_add, comp_id, v.comp_Hσ_eq hi, assoc,
  SimplicialObject.δ_comp_σ_succ_assoc, Fin.eta, decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero,
  add_neg_eq_zero]
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
⊢ ∀ (x : Fin (n + 1)),
    x ∈ Finset.filter (fun i => ↑i < q) Finset.univ →
      ((HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
              SimplicialObject.δ X (Fin.succ (↑Fin.revPerm x)) ≫ SimplicialObject.σ X (↑Fin.revPerm x)) ≫
            SimplicialObject.σ X i) ≫
          HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
        0
[PROOFSTEP]
intro j hj
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : j ∈ Finset.filter (fun i => ↑i < q) Finset.univ
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
simp only [true_and_iff, Finset.mem_univ, Finset.mem_filter] at hj
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
simp only [Nat.succ_eq_add_one] at hi
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))
[GOAL]
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : ↑j + k = n
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
rw [add_comm] at hk
[GOAL]
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
have hi' : i = Fin.castSucc ⟨i, by linarith⟩ := by
  ext
  simp only [Fin.castSucc_mk, Fin.eta]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ ↑i < n + 1
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ ↑i = ↑(Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) })
[PROOFSTEP]
simp only [Fin.castSucc_mk, Fin.eta]
[GOAL]
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
have eq :=
  hq j.revPerm.succ
    (by
      simp only [← hk, Fin.revPerm_eq j hk.symm, Nat.succ_eq_add_one, Fin.succ_mk, Fin.val_mk]
      linarith)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
⊢ Nat.succ n + 1 ≤ ↑(Fin.succ (↑Fin.revPerm j)) + q
[PROOFSTEP]
simp only [← hk, Fin.revPerm_eq j hk.symm, Nat.succ_eq_add_one, Fin.succ_mk, Fin.val_mk]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
⊢ k + ↑j + 1 + 1 ≤ k + 1 + q
[PROOFSTEP]
linarith
[GOAL]
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
eq : SimplicialObject.σ X (Fin.succ (↑Fin.revPerm j)) ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
rw [HomologicalComplex.comp_f, assoc, assoc, assoc, hi', SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp,
  comp_zero, comp_zero, comp_zero]
[GOAL]
case neg.succ.intro.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
eq : SimplicialObject.σ X (Fin.succ (↑Fin.revPerm j)) ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
⊢ { val := ↑i, isLt := (_ : ↑i < n + 1) } ≤ ↑Fin.revPerm j
[PROOFSTEP]
simp only [Fin.revPerm_eq j hk.symm, Fin.le_iff_val_le_val, Fin.val_mk]
[GOAL]
case neg.succ.intro.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
eq : SimplicialObject.σ X (Fin.succ (↑Fin.revPerm j)) ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
⊢ ↑i ≤ k
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f PInfty (n + 1) = 0
[PROOFSTEP]
rw [PInfty_f, σ_comp_P_eq_zero X i]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ n + 1 ≤ ↑i + (n + 1)
[PROOFSTEP]
simp only [le_add_iff_nonneg_left, zero_le]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : [n] ⟶ Δ'
hθ : ¬Mono θ
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n = 0
[PROOFSTEP]
rw [SimplexCategory.mono_iff_injective] at hθ
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : [n] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty Nat.zero = 0
[PROOFSTEP]
exfalso
[GOAL]
case zero.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ False
[PROOFSTEP]
apply hθ
[GOAL]
case zero.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
[PROOFSTEP]
intro x y h
[GOAL]
case zero.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
x y : Fin (SimplexCategory.len [Nat.zero] + 1)
h : ↑(SimplexCategory.Hom.toOrderHom θ) x = ↑(SimplexCategory.Hom.toOrderHom θ) y
⊢ x = y
[PROOFSTEP]
fin_cases x
[GOAL]
case zero.h.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
y : Fin (SimplexCategory.len [Nat.zero] + 1)
h :
  ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    ↑(SimplexCategory.Hom.toOrderHom θ) y
⊢ { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } = y
[PROOFSTEP]
fin_cases y
[GOAL]
case zero.h.head.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
h :
  ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) }
⊢ { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) }
[PROOFSTEP]
rfl
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n✝) = 0
[PROOFSTEP]
obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
[GOAL]
case succ.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : [n✝] ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n✝) = 0
[PROOFSTEP]
rw [h, op_comp, X.map_comp, assoc, show X.map (SimplexCategory.σ i).op = X.σ i by rfl, σ_comp_PInfty, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : [n✝] ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map (SimplexCategory.σ i).op = SimplicialObject.σ X i
[PROOFSTEP]
rfl


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.42, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Homotopy (P (q + 1)) (𝟙 K[X])
[PROOFSTEP]
refine'
  Homotopy.trans (Homotopy.ofEq _)
    (Homotopy.trans (Homotopy.add (homotopyPToId q) (Homotopy.compLeft (homotopyHσToZero q) (P q))) (Homotopy.ofEq _))
[GOAL]
case refine'_1
C : Type u_1
inst✝¹ : Category.{?u.42, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P (q + 1) = P q + P q ≫ Hσ q
[PROOFSTEP]
simp only [P_succ, comp_add, comp_id]
[GOAL]
case refine'_2
C : Type u_1
inst✝¹ : Category.{?u.42, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] + P q ≫ 0 = 𝟙 K[X]
[PROOFSTEP]
simp only [add_zero, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n < q
⊢ Homotopy.hom (homotopyPToId X (q + 1)) n (n + 1) = Homotopy.hom (homotopyPToId X q) n (n + 1)
[PROOFSTEP]
simp only [homotopyHσToZero, AlternatingFaceMapComplex.obj_X, Nat.add_eq, Homotopy.trans_hom, Homotopy.ofEq_hom,
  Pi.zero_apply, Homotopy.add_hom, Homotopy.compLeft_hom, add_zero, Homotopy.nullHomotopy'_hom, ComplexShape.down_Rel,
  hσ'_eq_zero hqn (c_mk (n + 1) n rfl), dite_eq_ite, ite_self, comp_zero, zero_add, homotopyPToId]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n < q
⊢ Homotopy.hom (homotopyPToId X (q + 0)) n (n + 1) = Homotopy.hom (homotopyPToId X q) n (n + 1)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n =
    ((↑(dNext n) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
        ↑(prevD n) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
      HomologicalComplex.Hom.f (𝟙 K[X]) n
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f PInfty Nat.zero =
    ((↑(dNext Nat.zero) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
        ↑(prevD Nat.zero) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
      HomologicalComplex.Hom.f (𝟙 K[X]) Nat.zero
[PROOFSTEP]
simpa only [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex, PInfty_f, Nat.zero_eq, P_f_0_eq,
  zero_add] using (homotopyPToId X 2).comm 0
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty (Nat.succ n) =
    ((↑(dNext (Nat.succ n)) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
        ↑(prevD (Nat.succ n)) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
rw [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex, PInfty_f, ←
  P_is_eventually_constant (rfl.le : n + 1 ≤ n + 1)]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (P (n + 1 + 1)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 1 + 1)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (Nat.succ n + 1 + 1)) (Nat.succ n) (Nat.succ n + 1) ≫
          HomologicalComplex.d K[X] (Nat.succ n + 1) (Nat.succ n) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
erw [homotopyPToId_eventually_constant X (lt_add_one (Nat.succ n))]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (P (n + 1 + 1)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 1 + 1)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (Nat.succ n + 1)) (Nat.succ n) (Nat.succ n + 1) ≫
          HomologicalComplex.d K[X] (Nat.succ n + 1) (Nat.succ n) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
have := (homotopyPToId X (n + 2)).comm (n + 1)
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
this :
  HomologicalComplex.Hom.f (P (n + 2)) (n + 1) =
    ↑(dNext (n + 1)) (homotopyPToId X (n + 2)).hom + ↑(prevD (n + 1)) (homotopyPToId X (n + 2)).hom +
      HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1)
⊢ HomologicalComplex.Hom.f (P (n + 1 + 1)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 1 + 1)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (Nat.succ n + 1)) (Nat.succ n) (Nat.succ n + 1) ≫
          HomologicalComplex.d K[X] (Nat.succ n + 1) (Nat.succ n) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
rw [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex] at this
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
this :
  HomologicalComplex.Hom.f (P (n + 2)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 2)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (n + 2)) (n + 1) (n + 1 + 1) ≫ HomologicalComplex.d K[X] (n + 1 + 1) (n + 1) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1)
⊢ HomologicalComplex.Hom.f (P (n + 1 + 1)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 1 + 1)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (Nat.succ n + 1)) (Nat.succ n) (Nat.succ n + 1) ≫
          HomologicalComplex.d K[X] (Nat.succ n + 1) (Nat.succ n) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
exact this