-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
D₁ D₂ : ComposableArrows.{u_5, u_4} ι' 2
f : D₁ ⟶ D₂
this :
  Eq (α :=
    X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).obj
        (Functor.obj (F.mapComposableArrows 2) D₂))
    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      (functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).map (Functor.map (F.mapComposableArrows 2) f) ≫
        X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂))
    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
        (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).map
          (Functor.map (F.mapComposableArrows 2) f))
⊢ (functorArrows ι' 1 2 2 _proof_2 _proof_4 ⋙ F.mapComposableArrows 1 ⋙ X.ω₁).map f ≫
      X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map' 1 2 _proof_2 _proof_4)).hom ≫
        X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂) ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).inv) =
    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map' 1 2 _proof_2 _proof_4)).hom ≫
        X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
          Functor.map (shiftFunctor C (A := ℤ) 1)
            (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv)) ≫
      (functorArrows ι' 0 1 2 _proof_6 _proof_2 ⋙ (F.mapComposableArrows 1 ⋙ X.ω₁) ⋙ shiftFunctor C (A := ℤ) 1).map f
have rw : ((functorArrows ι' 1 2 2 _proof_2 _proof_4 ⋙ F.mapComposableArrows 1 ⋙ X.ω₁).map f ≫
      X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map' 1 2 _proof_2 _proof_4)).hom ≫
        X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂) ≫
          Functor.map (shiftFunctor C (A := ℤ) 1)
            (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE sorry))).inv)) ≫
    Functor.map (shiftFunctor C (A := ℤ) 1)
      (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map' 0 1 _proof_6 _proof_2)).hom) =
  ((X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map' 1 2 _proof_2 _proof_4)).hom ≫
        X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
          Functor.map (shiftFunctor C (A := ℤ) 1)
            (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE sorry))).inv)) ≫
      (functorArrows ι' 0 1 2 _proof_6 _proof_2 ⋙ (F.mapComposableArrows 1 ⋙ X.ω₁) ⋙ shiftFunctor C (A := ℤ) 1).map f) ≫
    Functor.map (shiftFunctor C (A := ℤ) 1)
      (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map' 0 1 _proof_6 _proof_2)).hom)
Tactic: rw [← cancel_mono ((X.ω₁.map (F.mapComposableArrowsObjMk₁Iso _).hom)⟦(1 : ℤ)⟧')]