Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: case e_a
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
⊢ F'.map ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X)) ≫
      F'.map (L.map ((shiftFunctorAdd C a b).inv.app X)) ≫
        (Lifting.iso L W F F').hom.app ((shiftFunctor C (a + b)).obj X) ≫
          F.map ((shiftFunctorAdd C a b).hom.app X) ≫
            (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
              (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
                (shiftFunctorAdd E a b).inv.app (F.obj X) ≫
                  (shiftFunctor E (a + b)).map ((Lifting.iso L W F F').inv.app X) =
    F'.map ((shiftFunctor D b).map ((commShiftIso L a).hom.app X)) ≫
      (commShiftOfLocalization.iso L W F F' b).hom.app ((shiftFunctor D a).obj (L.obj X)) ≫
        (shiftFunctor E b).map (F'.map ((commShiftIso L a).inv.app X)) ≫
          (shiftFunctor E b).map ((Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) ≫
            (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
              (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
                (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))

Tactic:
conv_lhs =>
      erw [← NatTrans.naturality_assoc]
      dsimp
      rw [← Functor.map_comp_assoc, ← map_comp_assoc, Category.assoc,
        ← map_comp, Iso.inv_hom_id_app]
      dsimp
      rw [map_id, Category.comp_id, ← NatTrans.naturality]
      dsimp

Goal state after:
case e_a
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
⊢ F'.map ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X)) ≫
      (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
            (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
              (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X)) =
    F'.map ((shiftFunctor D b).map ((commShiftIso L a).hom.app X)) ≫
      (commShiftOfLocalization.iso L W F F' b).hom.app ((shiftFunctor D a).obj (L.obj X)) ≫
        (shiftFunctor E b).map (F'.map ((commShiftIso L a).inv.app X)) ≫
          (shiftFunctor E b).map ((Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) ≫
            (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
              (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
                (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))