C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫ SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
C : Type u_2
inst✝² : Category 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 [n + 1].op))
intro j _
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n + 1].op) ≫ SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫ SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
have eq := Γ₀.Obj.mapMono_on_summand_id K (SimplexCategory.δ j.succ)
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n + 1].op) ≫ SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0

case h₁
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ [n + 1] ≠ [n]

case h₂
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ ¬Isδ₀ (SimplexCategory.δ (Fin.succ j))
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n + 1].op) ≫ SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq
case h₁
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ [n + 1] ≠ [n]

case h₂
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ ¬Isδ₀ (SimplexCategory.δ (Fin.succ j))

C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n + 1].op) ≫ SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n + 1].op) ≫ SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0

case h₁
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ [n + 1] ≠ [n]

case h₂
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ ¬Isδ₀ (SimplexCategory.δ (Fin.succ j))
rotate_left
no goals
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n + 1].op) ≫ SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
exact eq
case h₁
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
h : [n + 1] = [n]
⊢ False
case h₁
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ [n + 1] ≠ [n]
intro h
no goals
case h₁
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
h : [n + 1] = [n]
⊢ False
exact (Nat.succ_ne_self n) (congr_arg SimplexCategory.len h)
no goals
case h₂
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
⊢ ¬Isδ₀ (SimplexCategory.δ (Fin.succ j))
exact fun h => Fin.succ_ne_zero j (by simpa only [Isδ₀.iff] using h)
no goals
C : Type u_2
inst✝² : Category 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 [n + 1].op) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id [n].op)
h : Isδ₀ (SimplexCategory.δ (Fin.succ j))
⊢ Fin.succ j = 0
simpa only [Isδ₀.iff] using h