-- 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))))))
    (𝟙
        (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))) ≫
      NatTrans.app (Iso.hom (F.mapHomologicalComplexUpToQuasiIsoFactors 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))))))
    (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 simp : 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 (Iso.hom (F.mapHomologicalComplexUpToQuasiIsoFactors 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)))
Tactic: simp only [Category.comp_id, Category.id_comp]