awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
h :
  J.W (whiskerRight (adj₁.unit.app P) F) ↔
    IsIso (Y := (G₁ ⋙ sheafCompose J F).obj P) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P)
h₁ :
  J.W (whiskerRight (adj₁.unit.app P) F) ↔
    J.W (X := obj (sheafToPresheaf J B) ((obj (whiskeringRight Cᵒᵖ A B) F ⋙ G₂).obj P)) (Y :=
      obj (sheafToPresheaf J B) ((G₁ ⋙ sheafCompose J F).obj P))
      (map (sheafToPresheaf J B) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P))
h₂ :
  J.W (X := obj (𝟭 (Functor.{v, v_1, u, u_1} Cᵒᵖ A)) P ⋙ F) (Y := (G₁ ⋙ sheafToPresheaf J A).obj P ⋙ F)
      (adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P)) ↔
    J.W (X := obj (sheafToPresheaf J B) ((obj (whiskeringRight Cᵒᵖ A B) F ⋙ G₂).obj P)) (Y :=
      obj (sheafToPresheaf J B) ((G₁ ⋙ sheafCompose J F).obj P))
      (map (sheafToPresheaf J B) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P))
h₃ h₄ :
  J.W (X := (G₂ ⋙ sheafToPresheaf J B).obj (P ⋙ F)) (Y := (G₁ ⋙ sheafToPresheaf J A).obj P ⋙ F)
      (map (sheafToPresheaf J B) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P) :
        obj (sheafToPresheaf J B) (G₂.obj (P ⋙ F)) ⟶ obj (sheafToPresheaf J B) ((G₁ ⋙ sheafCompose J F).obj P)) ↔
    J.W (X := obj (sheafToPresheaf J B) ((obj (whiskeringRight Cᵒᵖ A B) F ⋙ G₂).obj P)) (Y :=
      obj (sheafToPresheaf J B) ((G₁ ⋙ sheafCompose J F).obj P))
      (map (sheafToPresheaf J B) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P))
⊢ IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F)) ↔
    IsIso (Y := (G₁ ⋙ sheafCompose J F).obj P) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P)

Tactic:
rw [← J.W_iff_isIso_map_of_adjunction adj₂, ← J.W_sheafToPresheaf_map_iff_isIso,
    ← sheafComposeNatTrans_fac J F adj₁ adj₂,
    (W _).precomp_iff _ _ (J.W_adj_unit_app adj₂ (P ⋙ F))]

Premises used: CategoryTheory.GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso, CategoryTheory.Functor.comp, CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction, CategoryTheory.GrothendieckTopology.W_adj_unit_app, CategoryTheory.GrothendieckTopology.W, CategoryTheory.MorphismProperty.precomp_iff, CategoryTheory.sheafComposeNatTrans_fac
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
inst_4 rw : J.PreservesSheafification F
⊢ IsIso (Y := G₁ ⋙ sheafCompose J F) (sheafComposeNatTrans J F adj₁ adj₂)

Tactic:
rw [← J.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose]

Premises used: CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
G₁ : Functor.{v, v_1, u, u_1} Cᵒᵖ A ⥤ Sheaf.{v, v_1, u, u_1} J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : Functor.{v, v_2, u, u_2} Cᵒᵖ B ⥤ Sheaf.{v, v_2, u, u_2} J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst_3 : J.HasSheafCompose F
inst_4 : J.PreservesSheafification F
⊢ J.PreservesSheafification F

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : HasWeakSheafify.{v, v_1, u, u_1} J A
inst_4 : HasWeakSheafify.{v, v_2, u, u_2} J B
inst_5 : J.HasSheafCompose F
inst_6 : J.PreservesSheafification F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
⊢ Eq (α := P ⋙ F ⟶ sheafify J P ⋙ F)
    (CategoryStruct.comp (Y := sheafify J (P ⋙ F)) (toSheafify J (P ⋙ F)) (Iso.hom (sheafifyComposeIso J F P)))
    (whiskerRight (toSheafify J P) F)

Tactic:
sheafComposeNatTrans_fac J F (sheafificationAdjunction J A) (sheafificationAdjunction J B) P

Premises used: CategoryTheory.Functor.comp, CategoryTheory.sheafificationAdjunction, CategoryTheory.sheafComposeNatTrans_fac
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
inst_3 : HasWeakSheafify.{v, v_1, u, u_1} J A
inst_4 : HasWeakSheafify.{v, v_2, u, u_2} J B
inst_5 : J.HasSheafCompose F
inst_6 : J.PreservesSheafification F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
rw :
  Eq (α := P ⋙ F ⟶ sheafify J (P ⋙ F))
    (CategoryStruct.comp (Y := sheafify J P ⋙ F)
      (CategoryStruct.comp (Y := sheafify J (P ⋙ F)) (toSheafify J (P ⋙ F)) (Iso.hom (sheafifyComposeIso J F P)))
      (Iso.inv (sheafifyComposeIso J F P)))
    (toSheafify J (P ⋙ F))
rw₁ :
  Eq (α := P ⋙ F ⟶ sheafify J (P ⋙ F))
    (CategoryStruct.comp (Y := sheafify J (P ⋙ F)) (toSheafify J (P ⋙ F))
      (CategoryStruct.comp (Y := sheafify J P ⋙ F) (Iso.hom (sheafifyComposeIso J F P))
        (Iso.inv (sheafifyComposeIso J F P))))
    (toSheafify J (P ⋙ F))
rw₂ : toSheafify J (P ⋙ F) ≫ 𝟙 (sheafify J (P ⋙ F)) = toSheafify J (P ⋙ F)
rw₃ rw₄ : Eq (α := P ⋙ F ⟶ sheafify J (P ⋙ F)) (toSheafify J (P ⋙ F)) (toSheafify J (P ⋙ F))
⊢ Eq (α := P ⋙ F ⟶ sheafify J (P ⋙ F))
    (CategoryStruct.comp (Y := sheafify J P ⋙ F) (whiskerRight (toSheafify J P) F) (Iso.inv (sheafifyComposeIso J F P)))
    (toSheafify J (P ⋙ F))

Tactic:
rw [← sheafComposeIso_hom_fac, assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.sheafComposeIso_hom_fac, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- 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
this :
  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) }
rw :
  Eq (α :=
    obj (sheafToPresheaf J E) ((obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)).obj P) ⟶
      obj (sheafToPresheaf J E) ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P))
    (map (sheafToPresheaf J E) { hom := Iso.inv (J.sheafifyCompIso F P) }) (Iso.inv (J.sheafifyCompIso F P))
⊢ Eq (α :=
    obj (sheafToPresheaf J E) ((obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)).obj P) ⟶
      obj (sheafToPresheaf J E) ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P))
    (map (sheafToPresheaf J E)
      (NatTrans.app
        (sheafComposeNatTrans J F (plusPlusAdjunction J D (FD := FD) (CD := CD))
          (plusPlusAdjunction J E (FD := FE) (CD := CE)))
        P))
    (Iso.inv (J.sheafifyCompIso F P))

Tactic:
rw [this]
-- 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
this :
  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) }
⊢ Eq (α :=
    obj (sheafToPresheaf J E) ((obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)).obj P) ⟶
      obj (sheafToPresheaf J E) ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P))
    (map (sheafToPresheaf J E) { hom := Iso.inv (J.sheafifyCompIso F P) }) (Iso.inv (J.sheafifyCompIso F P))

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

Tactic:
suffices (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P =
    ⟨(sheafifyCompIso J F P).inv⟩ by
    rw [this]
    rfl
-- 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
⊢ Eq (α :=
    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))
    (CategoryStruct.comp (Y := obj (plusPlusSheaf J E (FD := FE) (CD := CE) ⋙ sheafToPresheaf J E) (P ⋙ F))
        (NatTrans.app (Adjunction.unit (plusPlusAdjunction J E (FD := FE) (CD := CE))) (P ⋙ F))
        (map (sheafToPresheaf J E)
          (NatTrans.app
            (sheafComposeNatTrans J F (plusPlusAdjunction J D (FD := FD) (CD := CD))
              (plusPlusAdjunction J E (FD := FE) (CD := CE)))
            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))
    (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:
sheafComposeNatTrans_fac J F (plusPlusAdjunction J D) (plusPlusAdjunction J E) P

Premises used: CategoryTheory.plusPlusAdjunction, CategoryTheory.sheafComposeNatTrans_fac
-- 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))
⊢ (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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
D : Type u_3
E : Type u_4
inst_3 : Category.{v_3, u_3} D
inst_4 : Category.{v_4, u_4} E
F : Functor.{v_3, v_4, u_3, u_4} D E
inst_5 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_6 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_8 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_10 : ∀ (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_11 : (X Y : D) → FunLike.{u_5 + 1, u_6 + 1, u_6 + 1} (FD X Y) (CD X) (CD Y)
inst_12 : (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_13 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_14 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E (FC := FE) (CC := CE))
inst_15 : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_16 : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E (FC := FE) (CC := CE))
inst_17 : ReflectsIsomorphisms.{v_3, u_3, u_6, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_18 : 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
rw :
  IsIso (X :=
    obj (sheafToPresheaf J E) ((obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)).obj P)) (Y :=
    obj (sheafToPresheaf J E) ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P))
    (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
⊢ IsIso (X := (obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)).obj P) (Y :=
    (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)

Tactic:
rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf J E),
    sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv]

Premises used: CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.sheafToPresheaf