-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι_1
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 : ℤ), 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 : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
F : Functor.{v_1, v_3, u_1, u_3} C D
inst_13 : F.CommShift ℤ
inst_14 : F.IsTriangulated
ι : Type u_4
inst_15 : Category.{v_4, u_4} ι
X Y : Triangulated.SpectralObject.{v_1, u_1, v_4, u_4} C ι
α : X ⟶ Y
i j k : ι
f : i ⟶ j
g : j ⟶ k
hf :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ f))) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (map (shiftFunctor C (A := ℤ) 1) (α.hom.app (mk₁ f))) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
rw :
  Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (X.δ f g) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
        map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
rw₁ :
  Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (X.δ f g) ≫
      F.map (map (shiftFunctor C (A := ℤ) 1) (α.hom.app (mk₁ f))) ≫
        NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
rw₂ :
  Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (X.δ f g ≫ map (shiftFunctor C (A := ℤ) 1) (α.hom.app (mk₁ f))) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
rw₃ :
  Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (α.hom.app (mk₁ g) ≫ Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
⊢ Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    ((F.map (X.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f))) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
have rw₄ : Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
  (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
  (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
Tactic: rw [Category.assoc, ← hf, ← F.map_comp_assoc, α.comm, F.map_comp_assoc]