-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasLeftHomology
inst_6 : S₂.HasLeftHomology
inst_7 : F.PreservesLeftHomologyOf S₁
inst_8 : F.PreservesLeftHomologyOf S₂
rw :
  Eq (α := leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F))
        (CategoryStruct.comp (Y := F.obj S₂.leftHomology) (F.map (leftHomologyMap φ))
          (Iso.inv (S₂.mapLeftHomologyIso F))) :
      leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F))
        (CategoryStruct.comp (Y := leftHomology (S₁.map F))
          (Iso.inv (S₁.mapLeftHomologyIso F) : F.obj S₁.leftHomology ⟶ leftHomology (S₁.map F))
          (leftHomologyMap (Functor.map F.mapShortComplex φ) :
            leftHomology (S₁.map F) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))) :
      leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
rw₁ :
  Eq (α := leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := leftHomology (Functor.obj F.mapShortComplex S₂))
        (leftHomologyMap (Functor.map F.mapShortComplex φ) :
          leftHomology (Functor.obj F.mapShortComplex S₁) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))
        (CategoryStruct.comp (Y := F.obj S₂.leftHomology) (Iso.hom (S₂.mapLeftHomologyIso F))
            (Iso.inv (S₂.mapLeftHomologyIso F)) :
          leftHomology (Functor.obj F.mapShortComplex S₂) ⟶ leftHomology (S₂.map F)) :
      leftHomology (Functor.obj F.mapShortComplex S₁) ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F))
      (CategoryStruct.comp (Y := leftHomology (S₁.map F))
        (Iso.inv (S₁.mapLeftHomologyIso F) : F.obj S₁.leftHomology ⟶ leftHomology (S₁.map F))
        (leftHomologyMap (Functor.map F.mapShortComplex φ) :
          leftHomology (S₁.map F) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))))
⊢ Eq (α := F.obj S₁.leftHomology ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.leftHomology) (F.map (leftHomologyMap φ)) (Iso.inv (S₂.mapLeftHomologyIso F)) :
      F.obj S₁.leftHomology ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := leftHomology (S₁.map F))
        (Iso.inv (S₁.mapLeftHomologyIso F) : F.obj S₁.leftHomology ⟶ leftHomology (S₁.map F))
        (leftHomologyMap (Functor.map F.mapShortComplex φ) :
          leftHomology (S₁.map F) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂)) :
      F.obj S₁.leftHomology ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))
have rw₂ : Eq (α := leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
  (leftHomologyMap (Functor.map F.mapShortComplex φ) ≫ 𝟙 (leftHomology (Functor.obj F.mapShortComplex S₂)) :
    leftHomology (Functor.obj F.mapShortComplex S₁) ⟶ leftHomology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F))
      (CategoryStruct.comp (Y := leftHomology (S₁.map F))
        (Iso.inv (S₁.mapLeftHomologyIso F) : F.obj S₁.leftHomology ⟶ leftHomology (S₁.map F))
        (leftHomologyMap (Functor.map F.mapShortComplex φ) :
          leftHomology (S₁.map F) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))) :
    leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapLeftHomologyIso F).hom, ← mapLeftHomologyIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]