-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
pos :
  CategoryStruct.comp (Y :=
      GradedObject.mapObj.{0, 0, v_1, u_1} (Functor.obj (shiftFunctor₁ C x) K).toGradedObject ((up ℤ).π (up ℤ) (up ℤ))
        n₁)
      (HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.X (p + 1 + x)).X q) x.negOnePow
            (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q) ≫
          (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯ :
        (K.X (p + x)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₁)
      ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      HSMul.hSMul (α := ℤˣ) (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') 1
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯)
pos₁ :
  HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.X (p + 1 + x)).X q) x.negOnePow
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q) ≫
      CategoryStruct.comp (Y :=
        GradedObject.mapObj.{0, 0, v_1, u_1} (Functor.obj (shiftFunctor₁ C x) K).toGradedObject ((up ℤ).π (up ℤ) (up ℤ))
          n₁)
        ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯ :
          ((Functor.obj (shiftFunctor₁ C x) K).X (p + 1)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₁)
        ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
          K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      HSMul.hSMul (α := ℤˣ) (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') 1
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯)
pos₂ :
  HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.X (p + 1 + x)).X q) x.negOnePow
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q) ≫
      K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯ =
    x.negOnePow •
      HSMul.hSMul (α := ℤˣ) (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') 1
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯)
pos₃ :
  HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.X (p + 1 + x)).X q) x.negOnePow
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q) ≫
      K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯ =
    HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') x.negOnePow
      (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯)
⊢ (HSMul.hSMul (α := ℤˣ) (β := (K.X (p + x)).X q ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n₁) 1
        (HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.X (p + 1 + x)).X q) x.negOnePow
            (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q) ≫
          (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      (Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n₁) ↦
        K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      HSMul.hSMul (α := ℤˣ) (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') 1
        (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯)
have pos₄ : HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') x.negOnePow
    (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' sorry) =
  HSMul.hSMul (β := (K.X (p + x)).X q ⟶ (K.total (up ℤ)).X n₁') x.negOnePow
    (HomologicalComplex.Hom.f (K.d (p + x) (p + 1 + x)) q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' sorry)
Tactic: rw [one_smul, Category.assoc, ι_totalDesc, one_smul, Linear.units_smul_comp]