-- 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.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))
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.truncGE a)) (CategoryTheory.Functor.map Q (s ≫ X.πTruncGE a))
      (CategoryStruct.comp (Y := Functor.obj Q (X'.truncGE a))
        (inv (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a)))
        (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE a))
          (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g a))
          (inv (CategoryTheory.Functor.map Q (Y.πTruncGE a))))))
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.truncGE a))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := X'.truncGE a) (X'.πTruncGE a) (CochainComplex.truncGEMap s a)))
      (CategoryStruct.comp (Y := Functor.obj Q (X'.truncGE a))
        (inv (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a)))
        (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE a))
          (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g a))
          (inv (CategoryTheory.Functor.map Q (Y.πTruncGE a))))))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X') (Functor.obj Q Y))
    (CategoryTheory.Functor.map Q g)
    (CategoryTheory.Functor.map Q s ≫
      CategoryStruct.comp (Y := Functor.obj Q (X.truncGE a)) (CategoryTheory.Functor.map Q (X.πTruncGE a))
        (CategoryStruct.comp (Y := Functor.obj Q (X'.truncGE a))
          (inv (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a)))
          (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE a))
            (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g a))
            (inv (CategoryTheory.Functor.map Q (Y.πTruncGE a))))))
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.truncGE a))
    (CategoryStruct.comp (Y := Functor.obj Q (X'.truncGE a)) (CategoryTheory.Functor.map Q (X'.πTruncGE a))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a)))
    (CategoryStruct.comp (Y := Functor.obj Q (X'.truncGE a))
      (inv (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a)))
      (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE a))
        (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g a))
        (inv (CategoryTheory.Functor.map Q (Y.πTruncGE a))))))
Tactic: rw [← Functor.map_comp_assoc, ← CochainComplex.πTruncGE_naturality s a,
      Functor.map_comp, assoc, IsIso.hom_inv_id_assoc,
      ← Functor.map_comp_assoc, CochainComplex.πTruncGE_naturality g a,
      Functor.map_comp, assoc, IsIso.hom_inv_id, comp_id]