-- 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 L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
y : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₂ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₃ :
  (f.f i₁).f (i₂ + y) ≫
      HSMul.hSMul (β := (L.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    ((i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₄ :
  (f.f i₁).f (i₂ + y) ≫
      HSMul.hSMul (β := (L.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (K.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₅ :
  HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
      ((f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (K.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₆ :
  HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
      ((f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + y)) (K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯)
        (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)))
⊢ (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
have h₇ : HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
    ((f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry) =
  HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
    ((f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry)
Tactic: rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul,
    Linear.units_smul_comp, ιTotal_map]