case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f (P Nat.zero) 0 = 𝟙 (HomologicalComplex.X K[X] 0)

case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
⊢ HomologicalComplex.Hom.f (P (Nat.succ q)) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
induction' q with q hq
no goals
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f (P Nat.zero) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
rfl
no goals
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
⊢ HomologicalComplex.Hom.f (P (Nat.succ q)) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
  HomologicalComplex.id_f, id_comp, hq, Hσ_eq_zero, add_zero]