-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Predicate (goal)
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
⊢ 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) τ)
have 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 sorry :
                  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 sorry :
                  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)
Tactic: ext