-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (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
F : Functor.{v_1, v_2, u_1, u_2} C D
ι : Type u_3
c : ComplexShape ι
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : CategoryWithHomology.{v_2, u_2} D
inst_6 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_2, u_2, u_3} D c) (HomologicalComplex.quasiIso D c)
inst_7 : F.Additive
inst_8 : F.PreservesHomology
inst_9 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_3} C c) (HomologicalComplex.quasiIso C c)
inst_10 : ComplexShape.QFactorsThroughHomotopy.{u_3, v_1, u_1} c C
inst_11 : ComplexShape.QFactorsThroughHomotopy.{u_3, v_2, u_2} c D
inst_12 :
  IsLocalization (C := HomologicalComplex.{v_1, u_1, u_3} C c) (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex.{v_1, u_1, u_3} C c
⊢ Eq.{u_4 + 1} (α :=
    Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_2, u_2, u_3, u_4} D c)
      (obj (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) (F.mapHomologicalComplexUpToQuasiIso c)
        (obj HomologicalComplexUpToQuasiIso.Qh (obj (HomotopyCategory.quotient C c) K)))
      (obj HomologicalComplexUpToQuasiIso.Qh
        (obj (HomotopyCategory.quotient D c)
          (obj (F.mapHomologicalComplex c) ((obj (HomotopyCategory.quotient C c) K).as (r := homotopic C c))))))
    (NatTrans.app
        (Localization.liftNatTrans (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
          (HomotopyCategory.quotient C c ⋙
            comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) HomologicalComplexUpToQuasiIso.Qh
              (F.mapHomologicalComplexUpToQuasiIso c))
          (HomotopyCategory.quotient C c ⋙ F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh)
          (comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) HomologicalComplexUpToQuasiIso.Qh
            (F.mapHomologicalComplexUpToQuasiIso c))
          (F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh)
          (Iso.hom (F.mapHomologicalComplexUpToQuasiIsoFactors c)))
        (obj (HomotopyCategory.quotient C c) K) :
      Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_2, u_2, u_3, u_4} D c)
        (obj
          (comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) HomologicalComplexUpToQuasiIso.Qh
            (F.mapHomologicalComplexUpToQuasiIso c))
          (obj (HomotopyCategory.quotient C c) K))
        (obj (F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh) (obj (HomotopyCategory.quotient C c) K)))
    (map (F.mapHomologicalComplexUpToQuasiIso c)
        (NatTrans.app (Iso.hom (HomologicalComplexUpToQuasiIso.quotientCompQhIso C c)) K) ≫
      NatTrans.app (Iso.hom (F.mapHomologicalComplexUpToQuasiIsoFactors c)) K ≫
        CategoryStruct.comp (Y :=
          obj HomologicalComplexUpToQuasiIso.Qh
            (obj (HomotopyCategory.quotient D c) (obj (F.mapHomologicalComplex c) K)))
          (NatTrans.app (Iso.inv (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c))
              (obj (F.mapHomologicalComplex c) K) :
            Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_2, u_2, u_3, u_4} D c)
              (obj HomologicalComplexUpToQuasiIso.Q (obj (F.mapHomologicalComplex c) K))
              (obj (HomotopyCategory.quotient D c ⋙ HomologicalComplexUpToQuasiIso.Qh)
                (obj (F.mapHomologicalComplex c) K)))
          (map HomologicalComplexUpToQuasiIso.Qh (NatTrans.app (Iso.inv (F.mapHomotopyCategoryFactors c)) K)))
have rw : Eq.{u_4 + 1} (α :=
  Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_2, u_2, u_3, u_4} D c)
    (obj (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) (F.mapHomologicalComplexUpToQuasiIso c)
      (obj HomologicalComplexUpToQuasiIso.Qh (obj (HomotopyCategory.quotient C c) K)))
    (obj HomologicalComplexUpToQuasiIso.Qh
      (obj (HomotopyCategory.quotient D c)
        (obj (F.mapHomologicalComplex c) ((obj (HomotopyCategory.quotient C c) K).as (r := homotopic C c))))))
  (CategoryStruct.comp (Y :=
      obj
        (HomotopyCategory.quotient C c ⋙
          comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) HomologicalComplexUpToQuasiIso.Qh
            (F.mapHomologicalComplexUpToQuasiIso c))
        K)
      (NatTrans.app
        (Iso.hom
          (Localization.Lifting.iso (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
            (HomotopyCategory.quotient C c ⋙
              comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) HomologicalComplexUpToQuasiIso.Qh
                (F.mapHomologicalComplexUpToQuasiIso c))
            (comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) HomologicalComplexUpToQuasiIso.Qh
              (F.mapHomologicalComplexUpToQuasiIso c))))
        K)
      (NatTrans.app (Iso.hom (F.mapHomologicalComplexUpToQuasiIsoFactors c)) K ≫
        NatTrans.app
          (Iso.inv
            (Localization.Lifting.iso (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
              (HomotopyCategory.quotient C c ⋙ F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh)
              (F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh)))
          K) :
    Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_2, u_2, u_3, u_4} D c)
      (obj
        (HomotopyCategory.quotient C c ⋙
          comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) HomologicalComplexUpToQuasiIso.Qh
            (F.mapHomologicalComplexUpToQuasiIso c))
        K)
      (obj (HomotopyCategory.quotient C c ⋙ F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh) K))
  (map (F.mapHomologicalComplexUpToQuasiIso c)
      (NatTrans.app (Iso.hom (HomologicalComplexUpToQuasiIso.quotientCompQhIso C c)) K) ≫
    NatTrans.app (Iso.hom (F.mapHomologicalComplexUpToQuasiIsoFactors c)) K ≫
      CategoryStruct.comp (Y :=
        obj HomologicalComplexUpToQuasiIso.Qh (obj (HomotopyCategory.quotient D c) (obj (F.mapHomologicalComplex c) K)))
        (NatTrans.app (Iso.inv (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c))
            (obj (F.mapHomologicalComplex c) K) :
          Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_2, u_2, u_3, u_4} D c)
            (obj HomologicalComplexUpToQuasiIso.Q (obj (F.mapHomologicalComplex c) K))
            (obj (HomotopyCategory.quotient D c ⋙ HomologicalComplexUpToQuasiIso.Qh)
              (obj (F.mapHomologicalComplex c) K)))
        (map HomologicalComplexUpToQuasiIso.Qh (NatTrans.app (Iso.inv (F.mapHomotopyCategoryFactors c)) K)))
Tactic: rw [Localization.liftNatTrans_app]