-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_3
E : Type u_4
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_4, u_4} E
F : Functor.{v_3, v_4, u_3, u_4} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_3, u, u_3} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst_9 : (X Y : D) → FunLike.{u_5 + 1, u_6 + 1, u_6 + 1} (FD X Y) (CD X) (CD Y)
inst_10 : (X Y : E) → FunLike.{u_7 + 1, u_8 + 1, u_8 + 1} (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory.{u_6, v_3, u_3, u_5} D FD (CC := CD)
instCCE : ConcreteCategory.{u_8, v_4, u_4, u_7} E FE (CC := CE)
inst_11 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_12 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E (FC := FE) (CC := CE))
inst_13 : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_14 : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E (FC := FE) (CC := CE))
inst_15 : ReflectsIsomorphisms.{v_3, u_3, u_6, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_16 : ReflectsIsomorphisms.{v_4, u_4, u_8, u_8 + 1} (forget E (FC := FE) (CC := CE))
P : Functor.{v, v_3, u, u_3} Cᵒᵖ D
e_1 :
  (obj (obj (whiskeringRight Cᵒᵖ D E) F) P ⟶
      obj (sheafToPresheaf J E) ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P)) =
    (obj (𝟭 (Functor.{v, v_4, u, u_4} Cᵒᵖ E)) (P ⋙ F) ⟶
      obj (sheafToPresheaf J E) ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P))
h :
  (Adjunction.homEquiv
          (Adjunction.mkOfHomEquiv
            {
              homEquiv := fun (P : Functor.{v, v_4, u, u_4} Cᵒᵖ E) (Q : Sheaf.{v, v_4, u, u_4} J E) ↦
                { toFun := fun (e : obj (plusPlusSheaf J E (FD := FE) (CD := CE)) P ⟶ Q) ↦ J.toSheafify P ≫ e.hom,
                  invFun := fun (e : P ⟶ Q.obj (P := Presheaf.IsSheaf J)) ↦ { hom := J.sheafifyLift e ⋯ },
                  left_inv := ⋯, right_inv := ⋯ },
              homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ })
          (P ⋙ F) ((sheafCompose J F).obj (obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P)) :
        (a : (plusPlusSheaf J E).obj (P ⋙ F) ⟶ (sheafCompose J F).obj ((plusPlusSheaf J D).obj P)) →
          P ⋙ F ⟶ J.sheafify P ⋙ F)
      { hom := Iso.inv (J.sheafifyCompIso F P) } =
    whiskerRight (J.toSheafify P ≫ 𝟙 (J.sheafify P)) F
⊢ Eq (α :=
    obj (obj (whiskeringRight Cᵒᵖ D E) F) P ⟶
      obj (sheafToPresheaf J E) ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P))
    ((Adjunction.homEquiv (plusPlusAdjunction J E (FD := FE) (CD := CE)) (obj (obj (whiskeringRight Cᵒᵖ D E) F) P)
            ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P) :
          (a :
              (plusPlusSheaf J E).obj (((whiskeringRight Cᵒᵖ D E).obj F).obj P) ⟶
                (plusPlusSheaf J D ⋙ sheafCompose J F).obj P) →
            ((whiskeringRight Cᵒᵖ D E).obj F).obj P ⟶
              (sheafToPresheaf J E).obj ((plusPlusSheaf J D ⋙ sheafCompose J F).obj P))
        { hom := Iso.inv (J.sheafifyCompIso F P) } :
      obj (obj (whiskeringRight Cᵒᵖ D E) F) P ⟶
        obj (sheafToPresheaf J E) ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P))
    (whiskerRight (NatTrans.app (Adjunction.unit (plusPlusAdjunction J D (FD := FD) (CD := CD))) P) F :
      obj (𝟭 (Functor.{v, v_3, u, u_3} Cᵒᵖ D)) P ⋙ F ⟶
        obj (plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafToPresheaf J D) P ⋙ F)

Tactic:
dsimp [plusPlusAdjunction]

Premises used: CategoryTheory.plusPlusAdjunction