Lean4
/-- A homotopy between morphisms of homological complexes `K ⟶ L` induces a homotopy
between morphisms of short complexes `K.sc i ⟶ L.sc i`. -/
noncomputable def toShortComplex (ho : Homotopy f g) (i : ι) :
ShortComplex.Homotopy ((shortComplexFunctor C c i).map f) ((shortComplexFunctor C c i).map g)
where
h₀ := if c.Rel (c.prev i) i then ho.hom _ (c.prev (c.prev i)) ≫ L.d _ _ else f.f _ - g.f _ - K.d _ i ≫ ho.hom i _
h₁ := ho.hom _ _
h₂ := ho.hom _ _
h₃ := if c.Rel i (c.next i) then K.d _ _ ≫ ho.hom (c.next (c.next i)) _ else f.f _ - g.f _ - ho.hom _ i ≫ L.d _ _
h₀_f := by
split_ifs with h
· dsimp
simp only [assoc, d_comp_d, comp_zero]
· dsimp
rw [L.shape _ _ h, comp_zero]
g_h₃ := by
split_ifs with h
· simp
· dsimp
rw [K.shape _ _ h, zero_comp]
comm₁ := by
dsimp
split_ifs with h
· rw [ho.comm (c.prev i)]
dsimp [dFrom, dTo, fromNext, toPrev]
rw [congr_arg (fun j => d K (c.prev i) j ≫ ho.hom j (c.prev i)) (c.next_eq' h)]
· abel
comm₂ := ho.comm i
comm₃ := by
dsimp
split_ifs with h
· rw [ho.comm (c.next i)]
dsimp [dFrom, dTo, fromNext, toPrev]
rw [congr_arg (fun j => ho.hom (c.next i) j ≫ L.d j (c.next i)) (c.prev_eq' h)]
· abel
