case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ), ιSummand s A ≫ 𝟙 (X.obj Δ) = ιSummand s A ≫ ∑ A : IndexSet Δ, πSummand s A ≫ ιSummand s A
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
⊢ 𝟙 (X.obj Δ) = ∑ A : IndexSet Δ, πSummand s A ≫ ιSummand s A
apply s.hom_ext'
case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ 𝟙 (X.obj Δ) = ιSummand s A ≫ ∑ A : IndexSet Δ, πSummand s A ≫ ιSummand s A
case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ), ιSummand s A ≫ 𝟙 (X.obj Δ) = ιSummand s A ≫ ∑ A : IndexSet Δ, πSummand s A ≫ ιSummand s A
intro A
case h.h₀
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ∀ (b : IndexSet Δ), b ∈ Finset.univ → b ≠ A → ιSummand s A ≫ πSummand s b ≫ ιSummand s b = 0

case h.h₁
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ¬A ∈ Finset.univ → ιSummand s A ≫ πSummand s A ≫ ιSummand s A = 0
case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ 𝟙 (X.obj Δ) = ιSummand s A ≫ ∑ A : IndexSet Δ, πSummand s A ≫ ιSummand s A
rw [comp_id, comp_sum, Finset.sum_eq_single A, ι_πSummand_eq_id_assoc]
case h.h₀
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
a✝ : B ∈ Finset.univ
h₂ : B ≠ A
⊢ ιSummand s A ≫ πSummand s B ≫ ιSummand s B = 0
case h.h₀
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ∀ (b : IndexSet Δ), b ∈ Finset.univ → b ≠ A → ιSummand s A ≫ πSummand s b ≫ ιSummand s b = 0
intro B _ h₂
no goals
case h.h₀
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
a✝ : B ∈ Finset.univ
h₂ : B ≠ A
⊢ ιSummand s A ≫ πSummand s B ≫ ιSummand s B = 0
rw [s.ι_πSummand_eq_zero_assoc _ _ h₂, zero_comp]
no goals
case h.h₁
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ¬A ∈ Finset.univ → ιSummand s A ≫ πSummand s A ≫ ιSummand s A = 0
simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff]