-- Mathlib/Algebra/Homology/Localization.lean
@[reassoc]
lemma mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app (K : HomologicalComplex C c) :
    (F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app
        ((HomotopyCategory.quotient _ _).obj K) =
      (F.mapHomologicalComplexUpToQuasiIso c).map
          ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
        (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
          (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app _ ≫
            HomologicalComplexUpToQuasiIso.Qh.map
              ((F.mapHomotopyCategoryFactors c).inv.app K)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_4, u_1} C
inst✝¹¹ : Category.{u_6, u_2} D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryWithHomology C
inst✝⁷ : CategoryWithHomology D
inst✝⁶ : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝⁵ : F.Additive
inst✝⁴ : F.PreservesHomology
inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝² : c.QFactorsThroughHomotopy C
inst✝¹ : c.QFactorsThroughHomotopy D
inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex C c
⊢ (F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient C c).obj K) =
    (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫
          HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)

Tactic:
dsimp [mapHomologicalComplexUpToQuasiIsoFactorsh]

Result:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_4, u_1} C
inst✝¹¹ : Category.{u_6, u_2} D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryWithHomology C
inst✝⁷ : CategoryWithHomology D
inst✝⁶ : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝⁵ : F.Additive
inst✝⁴ : F.PreservesHomology
inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝² : c.QFactorsThroughHomotopy C
inst✝¹ : c.QFactorsThroughHomotopy D
inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex C c
⊢ (Localization.liftNatTrans (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
          (HomotopyCategory.quotient C c ⋙ HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c)
          (HomotopyCategory.quotient C c ⋙ F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh)
          (HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c)
          (F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh)
          (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom).app
      ((HomotopyCategory.quotient C c).obj K) =
    (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫
          HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_4, u_1} C
inst✝¹¹ : Category.{u_6, u_2} D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryWithHomology C
inst✝⁷ : CategoryWithHomology D
inst✝⁶ : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝⁵ : F.Additive
inst✝⁴ : F.PreservesHomology
inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝² : c.QFactorsThroughHomotopy C
inst✝¹ : c.QFactorsThroughHomotopy D
inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex C c
⊢ (Localization.liftNatTrans (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
          (HomotopyCategory.quotient C c ⋙ HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c)
          (HomotopyCategory.quotient C c ⋙ F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh)
          (HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c)
          (F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh)
          (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom).app
      ((HomotopyCategory.quotient C c).obj K) =
    (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫
          HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)

Tactic:
rw [Localization.liftNatTrans_app]

Result:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_4, u_1} C
inst✝¹¹ : Category.{u_6, u_2} D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryWithHomology C
inst✝⁷ : CategoryWithHomology D
inst✝⁶ : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝⁵ : F.Additive
inst✝⁴ : F.PreservesHomology
inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝² : c.QFactorsThroughHomotopy C
inst✝¹ : c.QFactorsThroughHomotopy D
inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex C c
⊢ (Localization.Lifting.iso (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
              (HomotopyCategory.quotient C c ⋙
                HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c)
              (HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c)).hom.app
        K ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        (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)).inv.app
          K =
    (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫
          HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)