-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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)))
⊢ 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)) ⋯))
have 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)) sorry))
          (IsColimit.desc (RightHomologyData.hp (hᵣ.map F)) (CokernelCofork.ofπ (g (S.map F)) sorry) :
            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)) sorry) ⟶
              Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0) (CokernelCofork.ofπ (g (S.map F)) sorry))
          0)
        (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) sorry))
      (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)) sorry)) (Y :=
            LeftHomologyData.K (S := S.map F) (hₗ.map F))
            (IsLimit.lift (LeftHomologyData.hi (hₗ.map F)) (KernelFork.ofι (f (S.map F)) sorry) :
              Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) sorry) ⟶
                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))
                    sorry))
            0)
          (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) sorry))
        (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) sorry))
        (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)))
      (Fork.ι (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) sorry)) :
    LeftHomologyData.K (S := S.map F) (hₗ.map F) ⟶ RightHomologyData.Q (S := S.map F) (hᵣ.map F))
Tactic: trans (hₗ.map F).π ≫ ShortComplex.leftRightHomologyComparison'
    (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι