-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst_5 : hₗ.IsPreservedBy F
inst_6 : hᵣ.IsPreservedBy F
trans :
  F.map (hₗ.i ≫ hᵣ.p) =
    CategoryStruct.comp (Y := LeftHomologyData.H (S := S.map F) (hₗ.map F)) (LeftHomologyData.π (hₗ.map F))
      (CategoryStruct.comp (Y := RightHomologyData.H (S := S.map F) (hᵣ.map F))
        (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)) (RightHomologyData.ι (hᵣ.map F)))
trans₁ :
  Eq (α := F.obj hₗ.K ⟶ F.obj hᵣ.Q)
    (CategoryStruct.comp (Y := LeftHomologyData.H (S := S.map F) (hₗ.map F)) (LeftHomologyData.π (hₗ.map F))
        (CategoryStruct.comp (Y := RightHomologyData.H (S := S.map F) (hᵣ.map F))
          (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)) (RightHomologyData.ι (hᵣ.map F))) :
      F.obj hₗ.K ⟶ F.obj hᵣ.Q)
    (CategoryStruct.comp (Y :=
        Cone.pt (F :=
          parallelPair (X := RightHomologyData.Q (S := S.map F) (hᵣ.map F)) (Y :=
            Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0) (CokernelCofork.ofπ (g (S.map F)) ⋯))
            (IsColimit.desc (RightHomologyData.hp (hᵣ.map F)) (CokernelCofork.ofπ (g (S.map F)) ⋯) :
              Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0)
                  (CokernelCofork.ofπ (Z := RightHomologyData.Q (S := S.map F) (hᵣ.map F))
                    (RightHomologyData.p (hᵣ.map F)) ⋯) ⟶
                Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0) (CokernelCofork.ofπ (g (S.map F)) ⋯))
            0)
          (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯))
        (CategoryStruct.comp (Y :=
          Cocone.pt (F :=
            parallelPair (X :=
              Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) ⋯)) (Y :=
              LeftHomologyData.K (S := S.map F) (hₗ.map F))
              (IsLimit.lift (LeftHomologyData.hi (hₗ.map F)) (KernelFork.ofι (f (S.map F)) ⋯) :
                Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) ⋯) ⟶
                  Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0)
                    (KernelFork.ofι (Z := LeftHomologyData.K (S := S.map F) (hₗ.map F)) (LeftHomologyData.i (hₗ.map F))
                      ⋯))
              0)
            (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯))
          (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯))
          (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)))
        (Fork.ι (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯)) :
      LeftHomologyData.K (S := S.map F) (hₗ.map F) ⟶ RightHomologyData.Q (S := S.map F) (hᵣ.map F))
⊢ F.map (hₗ.i ≫ hᵣ.p) =
    CategoryStruct.comp (Y :=
      Cone.pt (F :=
        parallelPair (X := RightHomologyData.Q (S := S.map F) (hᵣ.map F)) (Y :=
          Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0) (CokernelCofork.ofπ (g (S.map F)) ⋯))
          (IsColimit.desc (RightHomologyData.hp (hᵣ.map F)) (CokernelCofork.ofπ (g (S.map F)) ⋯) :
            Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0)
                (CokernelCofork.ofπ (Z := RightHomologyData.Q (S := S.map F) (hᵣ.map F))
                  (RightHomologyData.p (hᵣ.map F)) ⋯) ⟶
              Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0) (CokernelCofork.ofπ (g (S.map F)) ⋯))
          0)
        (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯))
      (CategoryStruct.comp (Y :=
        Cocone.pt (F :=
          parallelPair (X :=
            Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) ⋯)) (Y :=
            LeftHomologyData.K (S := S.map F) (hₗ.map F))
            (IsLimit.lift (LeftHomologyData.hi (hₗ.map F)) (KernelFork.ofι (f (S.map F)) ⋯) :
              Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) ⋯) ⟶
                Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0)
                  (KernelFork.ofι (Z := LeftHomologyData.K (S := S.map F) (hₗ.map F)) (LeftHomologyData.i (hₗ.map F))
                    ⋯))
            0)
          (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯))
        (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯))
        (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)))
      (Fork.ι (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯))

Tactic:
trans (hₗ.map F).π ≫ ShortComplex.leftRightHomologyComparison'
    (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι

Premises used: CategoryTheory.ShortComplex.RightHomologyData.map, CategoryTheory.ShortComplex.LeftHomologyData.map, CategoryTheory.ShortComplex.leftRightHomologyComparison', CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.ShortComplex.RightHomologyData.ι