-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
X Y : Functor.{v_2, v_3, u_2, u_3} D E
τ : X ⟶ Y
h :
  ∀ (x : C),
    Eq (α :=
      (obj
                  (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                    Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                  X).obj
              (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦ W.IsInvertedBy F).obj
          x ⟶
        (obj (whiskeringLeftFunctor L W E) Y).obj (P := fun (F : Functor.{v_1, v_3, u_1, u_3} C E) ↦
              W.IsInvertedBy F).obj
          x)
      (NatTrans.app
        (InducedCategory.Hom.hom
          (map
              (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
              τ ≫
            Iso.hom
              ((fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦
                  (eqToIso ⋯ :
                    obj
                        (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                          Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                        F ≅
                      obj (whiskeringLeftFunctor L W E) F))
                Y)))
        x)
      (NatTrans.app
        (InducedCategory.Hom.hom
          (Iso.hom
              ((fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦
                  (eqToIso ⋯ :
                    obj
                        (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                          Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                        F ≅
                      obj (whiskeringLeftFunctor L W E) F))
                X) ≫
            map (whiskeringLeftFunctor L W E) τ))
        x)
⊢ Eq (α :=
    obj
        (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
          Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
        X ⟶
      obj (whiskeringLeftFunctor L W E) Y)
    (map
        (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
          Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
        τ ≫
      Iso.hom
        ((fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦
            (eqToIso ⋯ :
              obj
                  (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                    Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                  F ≅
                obj (whiskeringLeftFunctor L W E) F))
          Y))
    (Iso.hom
        ((fun (F : Functor.{v_2, v_3, u_2, u_3} D E) ↦
            (eqToIso ⋯ :
              obj
                  (obj (whiskeringLeft W.Localization D E) (equivalenceFromModel L W).functor ⋙
                    Equivalence.functor (Construction.whiskeringLeftEquivalence W E))
                  F ≅
                obj (whiskeringLeftFunctor L W E) F))
          X) ≫
      map (whiskeringLeftFunctor L W E) τ)

Tactic:
ext