feat(chain_complex): lemmas about eq_to_hom (#6250)

Adds two lemmas relating `eq_to_hom` to differentials and chain maps. Useful in the ubiquitous circumstance of having to apply identities in the index of a chain complex.

Also add some `@[reassoc]` tags for convenience.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/homology/chain_complex.lean

@@ -65,7 +65,7 @@ namespace homological_complex
 variables {V}
 variables {β : Type} [add_comm_group β] {b : β}
 
-@[simp]
+@[simp, reassoc]
 lemma d_squared (C : homological_complex V b) (i : β) :
   C.d i ≫ C.d (i+b) = 0 :=
 congr_fun (C.d_squared) i
@@ -75,15 +75,32 @@ A convenience lemma for morphisms of cochain complexes,
 picking out one component of the commutation relation.
 -/
 -- I haven't been able to get this to work with projection notation: `f.comm_at i`
-@[simp]
+@[simp, reassoc]
 lemma comm_at {C D : homological_complex V b} (f : C ⟶ D) (i : β) :
     C.d i ≫ f.f (i+b) = f.f i ≫ D.d i :=
 congr_fun f.comm i
 
-@[simp]
+@[simp, reassoc]
 lemma comm {C D : homological_complex V b} (f : C ⟶ D) : C.d ≫ f.f⟦1⟧' = f.f ≫ D.d :=
 differential_object.hom.comm _
 
+@[reassoc]
+lemma eq_to_hom_d (C : homological_complex V b) {i j : β} (h : i = j) :
+  eq_to_hom (congr_arg C.X h) ≫ C.d j =
+  C.d i ≫ eq_to_hom (congr_arg C.X (congr_arg (λ a, a + b) h) : _) :=
+begin
+  induction h,
+  simp,
+end
+
+@[reassoc]
+lemma eq_to_hom_f {C D : homological_complex V b} (f : C ⟶ D) {n m : β} (h : n = m) :
+  eq_to_hom (congr_arg C.X h) ≫ f.f m = f.f n ≫ eq_to_hom (congr_arg D.X h) :=
+begin
+  induction h,
+  simp
+end
+
 variables (V)
 
 /-- The forgetful functor from cochain complexes to graded objects, forgetting the differential. -/