Rest δ naturality

lemma rest_δ_naturality {S : ShortComplex (Rep R G)} (hS : S.ShortExact)    {H : Type u} [Group H] (φ : H →* G) (i j : ℕ) (hij : i + 1 = j) :    δ hS i j hij ≫ (rest φ j).app S.X₁ = (rest φ i).app S.X₃ ≫ δ ((shortExact_res φ).2 hS) i j hij    := by  let C₁ := S.map (cochainsFunctor R G)  let C₂ := (S.map (resFunctor φ)).map (cochainsFunctor R H)  have ses₁ : C₁.ShortExact := map_cochainsFunctor_shortExact hS  have ses₂ : C₂.ShortExact := by    apply map_cochainsFunctor_shortExact    rwa [shortExact_res]  let this : C₁ ⟶ C₂ := {    τ₁ := cochainsMap φ (𝟙 (res φ S.X₁))    τ₂ := cochainsMap φ (𝟙 (res φ S.X₂))    τ₃ := cochainsMap φ (𝟙 (res φ S.X₃))  }  exact HomologicalComplex.HomologySequence.δ_naturality this ses₁ ses₂ i j hij