-- Module: Mathlib.Topology.Sheaves.Functors
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f_1 : X ⟶ Y
ι : Type w
U : ι → Opens (↑Y : Type w)
A : Type u_1
inst_1 : Category.{w, u_1} A
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑Y : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := carrier) f) :
      (a : (↑X : Type w)) → (↑Y : Type w))
FA : A → A → Type u_2
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_2 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory A FA (CC := CA)
inst_4 : HasColimits.{w, u_1} A
inst_5 : HasLimits.{w, u_1} A
inst_6 : PreservesLimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_7 : PreservesFilteredColimits (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_8 : Functor.ReflectsIsomorphisms (CategoryTheory.forget A (FC := FA) (CC := CA))
refine_1 :
  (F : TopCat.Sheaf A Y) →
    Functor.obj
        (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A) F ≅
      Functor.obj (sheafPullback A hf) F
refine_2 :
  ∀ {X_1 Y_1 : TopCat.Sheaf A Y} (u : X_1 ⟶ Y_1),
    Eq (α :=
      Functor.obj
          (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A)
          X_1 ⟶
        Functor.obj (sheafPullback A hf) Y_1)
      (CategoryTheory.Functor.map
          (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A) u ≫
        Iso.hom
          ((fun (F : TopCat.Sheaf A Y) ↦
              (Functor.mapIso (presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A)
                    (Iso.app ⋯.pullbackIso (Functor.obj (Sheaf.forget A Y) F)) ≪≫
                  Functor.FullyFaithful.preimageIso
                    (fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology (↑X : Type w)) A)
                    (Iso.symm (isoSheafify (Opens.grothendieckTopology (↑X : Type w)) ⋯)) :
                Functor.obj
                    (Sheaf.forget A Y ⋙
                      Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A)
                    F ≅
                  Functor.obj (sheafPullback A hf) F))
            Y_1))
      (Iso.hom
          ((fun (F : TopCat.Sheaf A Y) ↦
              (Functor.mapIso (presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A)
                    (Iso.app ⋯.pullbackIso (Functor.obj (Sheaf.forget A Y) F)) ≪≫
                  Functor.FullyFaithful.preimageIso
                    (fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology (↑X : Type w)) A)
                    (Iso.symm (isoSheafify (Opens.grothendieckTopology (↑X : Type w)) ⋯)) :
                Functor.obj
                    (Sheaf.forget A Y ⋙
                      Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology (↑X : Type w)) A)
                    F ≅
                  Functor.obj (sheafPullback A hf) F))
            X_1) ≫
        CategoryTheory.Functor.map (sheafPullback A hf) u)
⊢ Iso (C := TopCat.Sheaf A Y ⥤ TopCat.Sheaf A X) (Sheaf.pullback A (FA := FA) (CA := CA) f) (sheafPullback A hf)

Tactic:
refine Sheaf.pullbackIso A f ≪≫ NatIso.ofComponents (fun F ↦ ?_) (fun u ↦ ?_)

Premises used: TopCat.Sheaf.pullbackIso, CategoryTheory.NatIso.ofComponents