-- 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
⊢ Eq (α := LeftHomologyData.K (S := S.map F) (hₗ.map F) ⟶ F.obj hᵣ.H)
    (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ))
    (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)))
have apply : 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)) 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))
    (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) sorry) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ))
    (Fork.ι (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) sorry)))
  (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: apply Fork.IsLimit.hom_ext (hᵣ.map F).hι