-- 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
a :
  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))
        (NatTrans.app
          (sheafComposeNatTrans J F (plusPlusAdjunction J D (FD := FD) (CD := CD))
            (plusPlusAdjunction J E (FD := FE) (CD := CE)))
          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))
    ((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))
⊢ Eq (α :=
    (obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)).obj P ⟶
      (plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P)
    (NatTrans.app
      (sheafComposeNatTrans J F (plusPlusAdjunction J D (FD := FD) (CD := CD))
        (plusPlusAdjunction J E (FD := FE) (CD := CE)))
      P)
    { hom := Iso.inv (J.sheafifyCompIso F P) }

Tactic:
apply ((plusPlusAdjunction J E).homEquiv _ _).injective

Premises used: CategoryTheory.plusPlusAdjunction, CategoryTheory.Adjunction.homEquiv, Equiv.injective