case zero
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (P Nat.zero) n) = HomologicalComplex.Hom.f (P Nat.zero) n

case succ
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n q : ℕ
hq : G.map (HomologicalComplex.Hom.f (P q) n) = HomologicalComplex.Hom.f (P q) n
⊢ G.map (HomologicalComplex.Hom.f (P (Nat.succ q)) n) = HomologicalComplex.Hom.f (P (Nat.succ q)) n
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (P q) n) = HomologicalComplex.Hom.f (P q) n
induction' q with q hq
case zero
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (P Nat.zero) n) = HomologicalComplex.Hom.f (P Nat.zero) n
case zero
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (P Nat.zero) n) = HomologicalComplex.Hom.f (P Nat.zero) n
simp only [P_zero]
no goals
case zero
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (P Nat.zero) n) = HomologicalComplex.Hom.f (P Nat.zero) n
apply G.map_id
no goals
case succ
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n q : ℕ
hq : G.map (HomologicalComplex.Hom.f (P q) n) = HomologicalComplex.Hom.f (P q) n
⊢ G.map (HomologicalComplex.Hom.f (P (Nat.succ q)) n) = HomologicalComplex.Hom.f (P (Nat.succ q)) n
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
  comp_id, Functor.map_add, Functor.map_comp, hq, map_Hσ]