-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
a b : ℤ
inst_3 : X.IsStrictlyLE b
inst_4 : Y.IsStrictlyGE a
inst_5 : Y.IsStrictlyLE b
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
Y' : CochainComplex.{v, u, 0} C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
fac : f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncLE b)) (Y := Functor.obj Q (Y'.truncLE b))
    (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s b))
refine_2 :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y'))
    (CategoryTheory.Functor.map Q g)
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncLE b)) (inv (CategoryTheory.Functor.map Q (X.ιTruncLE b)))
      (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncLE b))
        (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap g b))
        (CategoryStruct.comp (Y := Functor.obj Q (Y.truncLE b))
          (inv (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s b)))
          (CategoryTheory.Functor.map Q (Y.ιTruncLE b ≫ s)))))
refine_2₁ :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y'))
    (CategoryTheory.Functor.map Q g)
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncLE b)) (inv (CategoryTheory.Functor.map Q (X.ιTruncLE b)))
      (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncLE b))
        (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap g b))
        (CategoryStruct.comp (Y := Functor.obj Q (Y.truncLE b))
          (inv (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s b)))
          (CategoryTheory.Functor.map Q
            (CategoryStruct.comp (Y := Y'.truncLE b) (CochainComplex.truncLEMap s b) (Y'.ιTruncLE b))))))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y'))
    (CategoryTheory.Functor.map Q g)
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncLE b)) (inv (CategoryTheory.Functor.map Q (X.ιTruncLE b)))
      (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncLE b))
        (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap g b))
        (CategoryStruct.comp (Y := Functor.obj Q (Y.truncLE b))
          (inv (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s b)))
          (CategoryTheory.Functor.map Q (Y.ιTruncLE b) ≫ CategoryTheory.Functor.map Q s))))
have refine_2₂ : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y'))
  (CategoryTheory.Functor.map Q g)
  (CategoryStruct.comp (Y := Functor.obj Q (X.truncLE b)) (inv (CategoryTheory.Functor.map Q (X.ιTruncLE b)))
    (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncLE b))
      (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap g b))
      (CategoryStruct.comp (Y := Functor.obj Q (Y.truncLE b))
        (inv (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s b)))
        (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncLE b))
          (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s b))
          (CategoryTheory.Functor.map Q (Y'.ιTruncLE b))))))
Tactic: rw [← Functor.map_comp, ← CochainComplex.ιTruncLE_naturality s b,
      Functor.map_comp, IsIso.inv_hom_id_assoc,
      ← Functor.map_comp, CochainComplex.ιTruncLE_naturality g b,
      Functor.map_comp, IsIso.inv_hom_id_assoc]