-- Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
theorem decomposition_id (Δ : SimplexCategoryᵒᵖ) :
    𝟙 (X.obj Δ) = ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A

Proof state:
case h.h₀
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
a✝ : B ∈ Finset.univ
h₂ : B ≠ A
⊢ (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0

Tactic:
rw [s.cofan_inj_πSummand_eq_zero_assoc _ _ h₂, zero_comp]

Result:
no goals

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ),
    (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A

Tactic:
intro A

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A

Proof state:
case h.h₀
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ∀ b ∈ Finset.univ, b ≠ A → (s.cofan Δ).inj A ≫ s.πSummand b ≫ (s.cofan Δ).inj b = 0

Tactic:
intro B _ h₂

Result:
case h.h₀
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
a✝ : B ∈ Finset.univ
h₂ : B ≠ A
⊢ (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
⊢ 𝟙 (X.obj Δ) = ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A

Tactic:
apply s.hom_ext'

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ),
    (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A

Tactic:
erw [comp_id, comp_sum, Finset.sum_eq_single A, cofan_inj_πSummand_eq_id_assoc]

Result:
case h.h₀
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ∀ b ∈ Finset.univ, b ≠ A → (s.cofan Δ).inj A ≫ s.πSummand b ≫ (s.cofan Δ).inj b = 0

case h.h₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A ∉ Finset.univ → (s.cofan Δ).inj A ≫ s.πSummand A ≫ (s.cofan Δ).inj A = 0

Proof state:
case h.h₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A ∉ Finset.univ → (s.cofan Δ).inj A ≫ s.πSummand A ≫ (s.cofan Δ).inj A = 0

Tactic:
simp

Result:
no goals