-- 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 :
  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)) ⋯))
      (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ))
      (Fork.ι (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯)) =
    F.map (hₗ.i ≫ hᵣ.p)
trans₁ :
  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)) ⋯))
⊢ Eq (α := LeftHomologyData.K (S := S.map F) (hₗ.map F) ⟶ RightHomologyData.Q (S := S.map F) (hᵣ.map F))
    (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)) ⋯))
      (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ))
      (Fork.ι (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯)))
    (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 F.map (hₗ.i ≫ hᵣ.p)

Premises used: CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.LeftHomologyData.i, CategoryTheory.ShortComplex.RightHomologyData.p