-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_4 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
inst_5 : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst_6 : HasWeakSheafify K AddCommGrpCat
inst_7 :
  K.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
X' X : SheafOfModules.{v, v₁, u₁, u} S
Y : SheafOfModules.{v, v₂, u₂, u} R
f : X' ⟶ X
g : X ⟶ (pushforward φ).obj Y
dsimp :
  Eq (α :=
    (PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).obj
        ((PresheafOfModules.pullback φ.hom).obj X'.val) ⟶
      Y)
    ((Equiv.symm
            (Adjunction.homEquiv (PresheafOfModules.sheafificationAdjunction (𝟙 (R.obj (P := Presheaf.IsSheaf K))))
              ((PresheafOfModules.pullback φ.hom).obj X'.val) Y) :
          (a : (PresheafOfModules.pullback φ.hom).obj X'.val ⟶ Y.val.restrictScalarsObj (𝟙 R.obj)) →
            (PresheafOfModules.sheafification (𝟙 R.obj)).obj ((PresheafOfModules.pullback φ.hom).obj X'.val) ⟶ Y)
        ((Equiv.symm (Adjunction.homEquiv (PresheafOfModules.pullbackPushforwardAdjunction φ.hom) X'.val Y.val) :
            (a : X'.val ⟶ (PresheafOfModules.pushforward φ.hom).obj Y.val) →
              (PresheafOfModules.pullback φ.hom).obj X'.val ⟶ Y.val.restrictScalarsObj (𝟙 R.obj))
          (f.val ≫ g.val)) :
      (PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).obj
          ((PresheafOfModules.pullback φ.hom).obj X'.val) ⟶
        Y)
    ((PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).map
          ((PresheafOfModules.pullback φ.hom).map f.val) ≫
        (Equiv.symm
              (Adjunction.homEquiv (PresheafOfModules.sheafificationAdjunction (𝟙 (R.obj (P := Presheaf.IsSheaf K))))
                ((PresheafOfModules.pullback φ.hom).obj X.val) Y) :
            (a : (PresheafOfModules.pullback φ.hom).obj X.val ⟶ Y.val.restrictScalarsObj (𝟙 R.obj)) →
              (PresheafOfModules.sheafification (𝟙 R.obj)).obj ((PresheafOfModules.pullback φ.hom).obj X.val) ⟶ Y)
          ((Equiv.symm (Adjunction.homEquiv (PresheafOfModules.pullbackPushforwardAdjunction φ.hom) X.val Y.val) :
              (a : X.val ⟶ (PresheafOfModules.pushforward φ.hom).obj Y.val) →
                (PresheafOfModules.pullback φ.hom).obj X.val ⟶ Y.val.restrictScalarsObj (𝟙 R.obj))
            g.val) :
      (PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).obj
          ((PresheafOfModules.pullback φ.hom).obj X'.val) ⟶
        Y)
⊢ Eq (α :=
    (forget S ⋙
            PresheafOfModules.pullback φ.hom ⋙
              PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).obj
        X' ⟶
      Y)
    (((Equiv.symm
              (Equiv.trans
                (Adjunction.homEquiv (PresheafOfModules.sheafificationAdjunction (𝟙 (R.obj (P := Presheaf.IsSheaf K))))
                  ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X')) Y)
                (Equiv.trans (Adjunction.homEquiv (PresheafOfModules.pullbackPushforwardAdjunction φ.hom) X'.val Y.val)
                  (Equiv.symm (fullyFaithfulForget S).homEquiv))) :
            (X' ⟶ (pushforward φ).obj Y) ≃
              ((forget S ⋙
                      PresheafOfModules.pullback φ.hom ⋙
                        PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).obj
                  X' ⟶
                Y)) :
          (a : X' ⟶ (pushforward φ).obj Y) →
            (forget S ⋙ PresheafOfModules.pullback φ.hom ⋙ PresheafOfModules.sheafification (𝟙 R.obj)).obj X' ⟶ Y)
        (f ≫ g) :
      (forget S ⋙
              PresheafOfModules.pullback φ.hom ⋙
                PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).obj
          X' ⟶
        Y)
    ((forget S ⋙
              PresheafOfModules.pullback φ.hom ⋙
                PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).map
          f ≫
        ((Equiv.symm
                (Equiv.trans
                  (Adjunction.homEquiv
                    (PresheafOfModules.sheafificationAdjunction (𝟙 (R.obj (P := Presheaf.IsSheaf K))))
                    ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X)) Y)
                  (Equiv.trans (Adjunction.homEquiv (PresheafOfModules.pullbackPushforwardAdjunction φ.hom) X.val Y.val)
                    (Equiv.symm (fullyFaithfulForget S).homEquiv))) :
              (X ⟶ (pushforward φ).obj Y) ≃
                ((forget S ⋙
                        PresheafOfModules.pullback φ.hom ⋙
                          PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).obj
                    X ⟶
                  Y)) :
            (a : X ⟶ (pushforward φ).obj Y) →
              (forget S ⋙ PresheafOfModules.pullback φ.hom ⋙ PresheafOfModules.sheafification (𝟙 R.obj)).obj X ⟶ Y)
          g :
      (forget S ⋙
              PresheafOfModules.pullback φ.hom ⋙
                PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf K)))).obj
          X' ⟶
        Y)

Tactic:
dsimp [Functor.FullyFaithful.homEquiv]

Premises used: CategoryTheory.Functor.FullyFaithful.homEquiv