Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_4, u_4} D₁
inst✝² : Category.{v_5, u_5} D₂
L₁ : C ⥤ D₁
L₂ : C ⥤ D₂
W' : MorphismProperty C
inst✝¹ : L₁.IsLocalization W'
inst✝ : L₂.IsLocalization W'
⊢ { functor := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
        inverse := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
        unitIso :=
          (equivalenceFromModel L₁ W').counitIso.symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₁ W').inverse.rightUnitor.symm ≪≫
                  (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso ≪≫
                    ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                        (equivalenceFromModel L₂ W').inverse).symm)
                (equivalenceFromModel L₁ W').functor ≪≫
              ((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
                (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor,
        counitIso :=
          (((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
                (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor).symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                    (equivalenceFromModel L₁ W').inverse ≪≫
                  (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso.symm ≪≫
                    (equivalenceFromModel L₂ W').inverse.rightUnitor)
                (equivalenceFromModel L₂ W').functor ≪≫
              (equivalenceFromModel L₂ W').counitIso,
        functor_unitIso_comp := ⋯ }.symm =
    { functor := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
      inverse := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
      unitIso :=
        (equivalenceFromModel L₂ W').counitIso.symm ≪≫
          isoWhiskerRight
              ((equivalenceFromModel L₂ W').inverse.rightUnitor.symm ≪≫
                (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso ≪≫
                  ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                      (equivalenceFromModel L₁ W').inverse).symm)
              (equivalenceFromModel L₂ W').functor ≪≫
            ((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
              (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor,
      counitIso :=
        (((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
              (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor).symm ≪≫
          isoWhiskerRight
              ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                  (equivalenceFromModel L₂ W').inverse ≪≫
                (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso.symm ≪≫
                  (equivalenceFromModel L₁ W').inverse.rightUnitor)
              (equivalenceFromModel L₁ W').functor ≪≫
            (equivalenceFromModel L₁ W').counitIso,
      functor_unitIso_comp := ⋯ }

Tactic:
ext

Goal state after:
case functor
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_4, u_4} D₁
inst✝² : Category.{v_5, u_5} D₂
L₁ : C ⥤ D₁
L₂ : C ⥤ D₂
W' : MorphismProperty C
inst✝¹ : L₁.IsLocalization W'
inst✝ : L₂.IsLocalization W'
⊢ { functor := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
          inverse := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
          unitIso :=
            (equivalenceFromModel L₁ W').counitIso.symm ≪≫
              isoWhiskerRight
                  ((equivalenceFromModel L₁ W').inverse.rightUnitor.symm ≪≫
                    (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso ≪≫
                      ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                          (equivalenceFromModel L₂ W').inverse).symm)
                  (equivalenceFromModel L₁ W').functor ≪≫
                ((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
                  (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor,
          counitIso :=
            (((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
                  (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor).symm ≪≫
              isoWhiskerRight
                  ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                      (equivalenceFromModel L₁ W').inverse ≪≫
                    (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso.symm ≪≫
                      (equivalenceFromModel L₂ W').inverse.rightUnitor)
                  (equivalenceFromModel L₂ W').functor ≪≫
                (equivalenceFromModel L₂ W').counitIso,
          functor_unitIso_comp := ⋯ }.symm.functor =
    { functor := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
        inverse := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
        unitIso :=
          (equivalenceFromModel L₂ W').counitIso.symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₂ W').inverse.rightUnitor.symm ≪≫
                  (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso ≪≫
                    ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                        (equivalenceFromModel L₁ W').inverse).symm)
                (equivalenceFromModel L₂ W').functor ≪≫
              ((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
                (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor,
        counitIso :=
          (((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
                (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor).symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                    (equivalenceFromModel L₂ W').inverse ≪≫
                  (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso.symm ≪≫
                    (equivalenceFromModel L₁ W').inverse.rightUnitor)
                (equivalenceFromModel L₁ W').functor ≪≫
              (equivalenceFromModel L₁ W').counitIso,
        functor_unitIso_comp := ⋯ }.functor

case inverse
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_4, u_4} D₁
inst✝² : Category.{v_5, u_5} D₂
L₁ : C ⥤ D₁
L₂ : C ⥤ D₂
W' : MorphismProperty C
inst✝¹ : L₁.IsLocalization W'
inst✝ : L₂.IsLocalization W'
⊢ { functor := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
          inverse := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
          unitIso :=
            (equivalenceFromModel L₁ W').counitIso.symm ≪≫
              isoWhiskerRight
                  ((equivalenceFromModel L₁ W').inverse.rightUnitor.symm ≪≫
                    (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso ≪≫
                      ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                          (equivalenceFromModel L₂ W').inverse).symm)
                  (equivalenceFromModel L₁ W').functor ≪≫
                ((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
                  (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor,
          counitIso :=
            (((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
                  (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor).symm ≪≫
              isoWhiskerRight
                  ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                      (equivalenceFromModel L₁ W').inverse ≪≫
                    (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso.symm ≪≫
                      (equivalenceFromModel L₂ W').inverse.rightUnitor)
                  (equivalenceFromModel L₂ W').functor ≪≫
                (equivalenceFromModel L₂ W').counitIso,
          functor_unitIso_comp := ⋯ }.symm.inverse =
    { functor := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
        inverse := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
        unitIso :=
          (equivalenceFromModel L₂ W').counitIso.symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₂ W').inverse.rightUnitor.symm ≪≫
                  (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso ≪≫
                    ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                        (equivalenceFromModel L₁ W').inverse).symm)
                (equivalenceFromModel L₂ W').functor ≪≫
              ((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
                (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor,
        counitIso :=
          (((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
                (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor).symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                    (equivalenceFromModel L₂ W').inverse ≪≫
                  (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso.symm ≪≫
                    (equivalenceFromModel L₁ W').inverse.rightUnitor)
                (equivalenceFromModel L₁ W').functor ≪≫
              (equivalenceFromModel L₁ W').counitIso,
        functor_unitIso_comp := ⋯ }.inverse

case unitIso
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_4, u_4} D₁
inst✝² : Category.{v_5, u_5} D₂
L₁ : C ⥤ D₁
L₂ : C ⥤ D₂
W' : MorphismProperty C
inst✝¹ : L₁.IsLocalization W'
inst✝ : L₂.IsLocalization W'
⊢ { functor := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
          inverse := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
          unitIso :=
            (equivalenceFromModel L₁ W').counitIso.symm ≪≫
              isoWhiskerRight
                  ((equivalenceFromModel L₁ W').inverse.rightUnitor.symm ≪≫
                    (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso ≪≫
                      ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                          (equivalenceFromModel L₂ W').inverse).symm)
                  (equivalenceFromModel L₁ W').functor ≪≫
                ((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
                  (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor,
          counitIso :=
            (((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
                  (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor).symm ≪≫
              isoWhiskerRight
                  ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                      (equivalenceFromModel L₁ W').inverse ≪≫
                    (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso.symm ≪≫
                      (equivalenceFromModel L₂ W').inverse.rightUnitor)
                  (equivalenceFromModel L₂ W').functor ≪≫
                (equivalenceFromModel L₂ W').counitIso,
          functor_unitIso_comp := ⋯ }.symm.unitIso ≍
    { functor := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
        inverse := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
        unitIso :=
          (equivalenceFromModel L₂ W').counitIso.symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₂ W').inverse.rightUnitor.symm ≪≫
                  (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso ≪≫
                    ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                        (equivalenceFromModel L₁ W').inverse).symm)
                (equivalenceFromModel L₂ W').functor ≪≫
              ((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
                (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor,
        counitIso :=
          (((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
                (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor).symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                    (equivalenceFromModel L₂ W').inverse ≪≫
                  (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso.symm ≪≫
                    (equivalenceFromModel L₁ W').inverse.rightUnitor)
                (equivalenceFromModel L₁ W').functor ≪≫
              (equivalenceFromModel L₁ W').counitIso,
        functor_unitIso_comp := ⋯ }.unitIso

case counitIso
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_4, u_4} D₁
inst✝² : Category.{v_5, u_5} D₂
L₁ : C ⥤ D₁
L₂ : C ⥤ D₂
W' : MorphismProperty C
inst✝¹ : L₁.IsLocalization W'
inst✝ : L₂.IsLocalization W'
⊢ { functor := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
          inverse := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
          unitIso :=
            (equivalenceFromModel L₁ W').counitIso.symm ≪≫
              isoWhiskerRight
                  ((equivalenceFromModel L₁ W').inverse.rightUnitor.symm ≪≫
                    (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso ≪≫
                      ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                          (equivalenceFromModel L₂ W').inverse).symm)
                  (equivalenceFromModel L₁ W').functor ≪≫
                ((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
                  (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor,
          counitIso :=
            (((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
                  (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor).symm ≪≫
              isoWhiskerRight
                  ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                      (equivalenceFromModel L₁ W').inverse ≪≫
                    (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso.symm ≪≫
                      (equivalenceFromModel L₂ W').inverse.rightUnitor)
                  (equivalenceFromModel L₂ W').functor ≪≫
                (equivalenceFromModel L₂ W').counitIso,
          functor_unitIso_comp := ⋯ }.symm.counitIso ≍
    { functor := (equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor,
        inverse := (equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor,
        unitIso :=
          (equivalenceFromModel L₂ W').counitIso.symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₂ W').inverse.rightUnitor.symm ≪≫
                  (equivalenceFromModel L₂ W').inverse.isoWhiskerLeft (equivalenceFromModel L₁ W').unitIso ≪≫
                    ((equivalenceFromModel L₂ W').inverse.associator (equivalenceFromModel L₁ W').functor
                        (equivalenceFromModel L₁ W').inverse).symm)
                (equivalenceFromModel L₂ W').functor ≪≫
              ((equivalenceFromModel L₂ W').inverse ⋙ (equivalenceFromModel L₁ W').functor).associator
                (equivalenceFromModel L₁ W').inverse (equivalenceFromModel L₂ W').functor,
        counitIso :=
          (((equivalenceFromModel L₁ W').inverse ⋙ (equivalenceFromModel L₂ W').functor).associator
                (equivalenceFromModel L₂ W').inverse (equivalenceFromModel L₁ W').functor).symm ≪≫
            isoWhiskerRight
                ((equivalenceFromModel L₁ W').inverse.associator (equivalenceFromModel L₂ W').functor
                    (equivalenceFromModel L₂ W').inverse ≪≫
                  (equivalenceFromModel L₁ W').inverse.isoWhiskerLeft (equivalenceFromModel L₂ W').unitIso.symm ≪≫
                    (equivalenceFromModel L₁ W').inverse.rightUnitor)
                (equivalenceFromModel L₁ W').functor ≪≫
              (equivalenceFromModel L₁ W').counitIso,
        functor_unitIso_comp := ⋯ }.counitIso