-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D₁ : Type u_4
D₂ : Type u_5
inst_1 : Category.{v_4, u_4} D₁
inst_2 : Category.{v_5, u_5} D₂
L₁ : Functor.{v_1, v_4, u_1, u_4} C D₁
L₂ : Functor.{v_1, v_5, u_1, u_5} C D₂
W' : MorphismProperty.{v_1, u_1} C
inst_3 : L₁.IsLocalization W'
inst_4 : L₂.IsLocalization W'
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 := ⋯ : Equivalence.{v_4, v_5, u_4, u_5} D₁ D₂ }.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
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 := ⋯ : Equivalence.{v_4, v_5, u_4, u_5} D₁ D₂ }.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
⊢ { 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 := ⋯ : Equivalence.{v_4, v_5, u_4, u_5} D₁ D₂ }.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 := ⋯ }
have 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 := sorry : Equivalence.{v_4, v_5, u_4, u_5} D₁ D₂ }.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 := sorry : Equivalence.{v_5, v_4, u_5, u_4} D₂ D₁ }.unitIso
Tactic: ext