-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h : c₁₂.Rel i₁₂ i₁₂'
rw :
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') ≫
      GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
rw₁ :
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
      (K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
rw₂ :
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
      (K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫
      HAdd.hAdd (α := L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (L.D₁ c₁₂ i₁₂ i₁₂') (L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') ≫
      GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
have rw₃ : HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂') =
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
Tactic: rw [comp_add, add_comp, mapAux.mapMap_D₁, mapAux.mapMap_D₂]