-- 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 :
  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)
⊢ 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)) ⋯)))
have 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)) 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))
Tactic: trans F.map (hₗ.i ≫ hᵣ.p)