-- 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} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
this :
  Eq (α :=
    X.ω₁.obj (mk₁ (F.map g)) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := X.ω₁.obj (mk₁ (F.map g))) (X.ω₁.map (homMk₁ (𝟙 (F.obj w_1)) (𝟙 (F.obj w_2)) ⋯))
        (X.δ'.app (mk₂ (F.map f) (F.map g))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
        (X.δ'.app (Functor.obj (F.mapComposableArrows 2) (mk₂ f g)))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (𝟙 (F.obj w)) (𝟙 (F.obj w_1)) ⋯))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
⊢ Eq (α :=
    X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ g)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
          (X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ f))))
        (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso g).hom ≫
          X.δ'.app (Functor.obj (F.mapComposableArrows 2) (mk₂ f g)) ≫
            Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso f).inv))
        (Functor.map (shiftFunctor C (A := ℤ) 1)
          (X.ω₁.map (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) ⋯).hom)) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (X.ω₁.map (isoMk₁ (Iso.refl (F.obj w_1)) (Iso.refl (F.obj w_2)) ⋯).hom ≫ X.δ'.app (mk₂ (F.map f) (F.map g)) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
have refine_3 : Eq (α :=
  X.ω₁.obj (mk₁ (F.map g)) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
  (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso g).inv ≫
    CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ f))))
      (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso g).hom ≫
        X.δ'.app (Functor.obj (F.mapComposableArrows 2) (mk₂ f g)) ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso f).inv))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) sorry).hom)))
  (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso g).inv ≫
    X.ω₁.map (isoMk₁ (Iso.refl (F.obj w_1)) (Iso.refl (F.obj w_2)) sorry).hom ≫ X.δ'.app (mk₂ (F.map f) (F.map g)))
Tactic: rw [← cancel_epi (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso _).inv)]