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 ((shiftFunctor D b).map ((commShiftIso L a).hom.app X ≫ (commShiftIso L a).inv.app X)) ≫
      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:
Iso.hom_inv_id_app,

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 ((shiftFunctor D b).map (𝟙 ((shiftFunctor C a ⋙ L).obj X))) ≫
      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))