Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
X Y : HomologicalComplex C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map f)
h₂ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map (r • f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map (r • f))
⊢ (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map (r • f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    r •
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
        (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
X Y : HomologicalComplex C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map f)
h₂ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map (r • f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map (r • f))
⊢ (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map (r • f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    r •
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
        (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y