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
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
mpr :
  J.W (Y := (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)
    (whiskerRight (adj₁.unit.app P₁ ≫ map (sheafToPresheaf J A) (G₁.map f)) F)
⊢ J.W (whiskerRight (adj₁.unit.app P₁ ≫ (G₁ ⋙ sheafToPresheaf J A).map f) F)

Tactic:
dsimp only [Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_map
-- 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
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
mpr :
  J.W (X := (G₁ ⋙ sheafToPresheaf J A).obj P₁ ⋙ F) (Y := (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)
    (whiskerRight (map (sheafToPresheaf J A) (G₁.map f)) F :
      (G₁ ⋙ sheafToPresheaf J A).obj P₁ ⋙ F ⟶ (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)
⊢ J.W (Y := (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)
    (whiskerRight (adj₁.unit.app P₁ ≫ map (sheafToPresheaf J A) (G₁.map f)) F)

Tactic:
rw [whiskerRight_comp, (W _).precomp_iff _ _ (h P₁)]

Premises used: CategoryTheory.GrothendieckTopology.W, CategoryTheory.MorphismProperty.precomp_iff, CategoryTheory.Functor.whiskerRight_comp
-- 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
h : ∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (X := (G₁ ⋙ sheafToPresheaf J A).obj P₁ ⋙ F) (Y := (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)
    (whiskerRight (map (sheafToPresheaf J A) (G₁.map f)) F :
      (G₁ ⋙ sheafToPresheaf J A).obj P₁ ⋙ F ⟶ (G₁ ⋙ sheafToPresheaf J A).obj P₂ ⋙ F)

Tactic:
apply ObjectProperty.isLocal_of_isIso

Premises used: CategoryTheory.ObjectProperty.isLocal_of_isIso
-- 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 Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
dsimp :
  Eq (α := G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
    (G₂.map (whiskerRight f F) ≫
      ((Equiv.symm (adj₂.homEquiv (Q ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
            (Q ⋙ F ⟶ (G₁.obj Q).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
              (G₂.obj (Q ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))) :
          (a : Q ⋙ F ⟶ (G₁.obj Q).obj ⋙ F) → G₂.obj (Q ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
        (whiskerRight (adj₁.unit.app Q) F))
    (((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) :
            (P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
              (G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))) :
          (a : P ⋙ F ⟶ (G₁.obj P).obj ⋙ F) → G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))
        (whiskerRight (adj₁.unit.app P) F) ≫
      (sheafCompose J F).map (G₁.map f))
⊢ Eq (α := (obj (whiskeringRight Cᵒᵖ A B) F ⋙ G₂).obj P ⟶ (G₁ ⋙ sheafCompose J F).obj Q)
    ((obj (whiskeringRight Cᵒᵖ A B) F ⋙ G₂).map f ≫
      (Equiv.symm (adj₂.homEquiv (obj (obj (whiskeringRight Cᵒᵖ A B) F) Q) ((G₁ ⋙ sheafCompose J F).obj Q)) :
          (a : ((whiskeringRight Cᵒᵖ A B).obj F).obj Q ⟶ (sheafToPresheaf J B).obj ((G₁ ⋙ sheafCompose J F).obj Q)) →
            G₂.obj (((whiskeringRight Cᵒᵖ A B).obj F).obj Q) ⟶ (G₁ ⋙ sheafCompose J F).obj Q)
        (whiskerRight (adj₁.unit.app Q) F))
    ((Equiv.symm (adj₂.homEquiv (obj (obj (whiskeringRight Cᵒᵖ A B) F) P) ((G₁ ⋙ sheafCompose J F).obj P)) :
          (a : ((whiskeringRight Cᵒᵖ A B).obj F).obj P ⟶ (sheafToPresheaf J B).obj ((G₁ ⋙ sheafCompose J F).obj P)) →
            G₂.obj (((whiskeringRight Cᵒᵖ A B).obj F).obj P) ⟶ (G₁ ⋙ sheafCompose J F).obj P)
        (whiskerRight (adj₁.unit.app P) F) ≫
      (G₁ ⋙ sheafCompose J F).map f)

Tactic:
dsimp
-- 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 Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
erw :
  Eq (α := G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
    ((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
          (a : P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj Q))) →
            G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
        (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F) :
      G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
    ((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
          (a : P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj Q))) →
            G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
        (whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))) :
      G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
⊢ Eq (α := G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
    (G₂.map (whiskerRight f F) ≫
      ((Equiv.symm (adj₂.homEquiv (Q ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
            (Q ⋙ F ⟶ (G₁.obj Q).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
              (G₂.obj (Q ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))) :
          (a : Q ⋙ F ⟶ (G₁.obj Q).obj ⋙ F) → G₂.obj (Q ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
        (whiskerRight (adj₁.unit.app Q) F))
    (((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) :
            (P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
              (G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))) :
          (a : P ⋙ F ⟶ (G₁.obj P).obj ⋙ F) → G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))
        (whiskerRight (adj₁.unit.app P) F) ≫
      (sheafCompose J F).map (G₁.map f))

Tactic:
erw [← adj₂.homEquiv_naturality_left_symm,
      ← adj₂.homEquiv_naturality_right_symm]

Premises used: CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_naturality_left_symm
-- 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 Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
h :
  whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F =
    whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))
⊢ Eq (α := G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
    ((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
          (a : P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj Q))) →
            G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
        (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F) :
      G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
    ((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))) :
          (a : P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj Q))) →
            G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))
        (whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))) :
      G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj Q))

Tactic:
congr 1
-- 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 Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
h :
  ∀ (X : Cᵒᵖ),
    (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F).app X =
      NatTrans.app (whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))) X
⊢ whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F =
    whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))

Tactic:
ext X
-- 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 Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
X : Cᵒᵖ
⊢ (map (𝟭 (Functor.{v, v_1, u, u_1} Cᵒᵖ A)) f ≫ adj₁.unit.app Q).app X =
    (adj₁.unit.app P ≫ (G₁ ⋙ sheafToPresheaf J A).map f).app X

Tactic:
have := NatTrans.congr_app (adj₁.unit.naturality f) X
-- 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 Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
X : Cᵒᵖ
this :
  (map (𝟭 (Functor.{v, v_1, u, u_1} Cᵒᵖ A)) f ≫ adj₁.unit.app Q).app X =
    (adj₁.unit.app P ≫ (G₁ ⋙ sheafToPresheaf J A).map f).app X
h : F.map (f.app X) ≫ F.map ((adj₁.unit.app Q).app X) = F.map ((adj₁.unit.app P).app X) ≫ F.map ((G₁.map f).hom.app X)
⊢ (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F).app X =
    NatTrans.app (whiskerRight (adj₁.unit.app P) F ≫ map (sheafToPresheaf J B) ((sheafCompose J F).map (G₁.map f))) X

Tactic:
dsimp at this ⊢
-- 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 Q : Functor.{v, v_1, u, u_1} Cᵒᵖ A
f : P ⟶ Q
X : Cᵒᵖ
this : f.app X ≫ (adj₁.unit.app Q).app X = (adj₁.unit.app P).app X ≫ (G₁.map f).hom.app X
⊢ F.map (f.app X) ≫ F.map ((adj₁.unit.app Q).app X) = F.map ((adj₁.unit.app P).app X) ≫ F.map ((G₁.map f).hom.app X)

Tactic:
grind
-- 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
⊢ adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P) =
    whiskerRight (adj₁.unit.app P) F

Tactic:
simp [sheafComposeNatTrans, -ObjectProperty.ι_obj, -ObjectProperty.ι_map,
    Adjunction.homEquiv_counit]

Premises used: CategoryTheory.ObjectProperty.ι_map, CategoryTheory.ObjectProperty.ι_obj, CategoryTheory.sheafComposeNatTrans, CategoryTheory.Adjunction.homEquiv_counit
-- 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
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α = whiskerRight (adj₁.unit.app P) F
a :
  Eq (α := P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) →
            P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj P)))
        α :
      P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) →
            P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj P)))
        (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P) :
      P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
⊢ α = NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P

Tactic:
apply (adj₂.homEquiv _ _).injective

Premises used: CategoryTheory.Adjunction.homEquiv, Equiv.injective
-- 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
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α = whiskerRight (adj₁.unit.app P) F
a :
  Eq (α := P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
        α :
      P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
        (((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) :
              (P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
                (G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))) :
            (a : P ⋙ F ⟶ (G₁.obj P).obj ⋙ F) → G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))
          (whiskerRight (adj₁.unit.app P) F)) :
      P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
⊢ Eq (α := P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) →
            P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj P)))
        α :
      P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) →
            P ⋙ F ⟶ (sheafToPresheaf J B).obj ((sheafCompose J F).obj (G₁.obj P)))
        (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) P) :
      P ⋙ F ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))

Tactic:
dsimp [sheafComposeNatTrans]

Premises used: CategoryTheory.sheafComposeNatTrans
-- 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
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α = whiskerRight (adj₁.unit.app P) F
a :
  (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
        (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
      α =
    whiskerRight (adj₁.unit.app P) F
⊢ Eq (α := P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
        α :
      P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
        (((Equiv.symm (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) :
              (P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F) ≃
                (G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))) :
            (a : P ⋙ F ⟶ (G₁.obj P).obj ⋙ F) → G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P))
          (whiskerRight (adj₁.unit.app P) F)) :
      P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)

Tactic:
erw [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- 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
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α = whiskerRight (adj₁.unit.app P) F
a :
  Eq (α := P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
        α :
      P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    (adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α :
      obj (𝟭 (Functor.{v, v_2, u, u_2} Cᵒᵖ B)) (P ⋙ F) ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
        (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
      α =
    whiskerRight (adj₁.unit.app P) F

Tactic:
rw [← hα]
-- 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
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α = whiskerRight (adj₁.unit.app P) F
⊢ Eq (α := P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)) :
          (a : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)) → P ⋙ F ⟶ (G₁.obj P).obj ⋙ F)
        α :
      P ⋙ F ⟶ (G₁.obj P).obj (P := Presheaf.IsSheaf J) ⋙ F)
    (adj₂.unit.app (P ⋙ F) ≫ map (sheafToPresheaf J B) α :
      obj (𝟭 (Functor.{v, v_2, u, u_2} Cᵒᵖ B)) (P ⋙ F) ⟶ obj (sheafToPresheaf J B) ((sheafCompose J F).obj (G₁.obj P)))

Tactic:
apply adj₂.homEquiv_unit

Premises used: CategoryTheory.Adjunction.homEquiv_unit
-- 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
rw :
  (∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))) ↔
    ∀ (X : Functor.{v, v_1, u, u_1} Cᵒᵖ A),
      IsIso (Y := (G₁ ⋙ sheafCompose J F).obj X) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) X)
⊢ J.PreservesSheafification F ↔ IsIso (Y := G₁ ⋙ sheafCompose J F) (sheafComposeNatTrans J F adj₁ adj₂)

Tactic:
rw [J.preservesSheafification_iff_of_adjunctions F adj₁ adj₂,
    NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions, CategoryTheory.NatTrans.isIso_iff_isIso_app
-- 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
h :
  ∀ (a : Functor.{v, v_1, u, u_1} Cᵒᵖ A),
    IsIso (G₂.map (whiskerRight (adj₁.unit.app a) F)) ↔
      IsIso (Y := (G₁ ⋙ sheafCompose J F).obj a) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) a)
⊢ (∀ (P : Functor.{v, v_1, u, u_1} Cᵒᵖ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))) ↔
    ∀ (X : Functor.{v, v_1, u, u_1} Cᵒᵖ A),
      IsIso (Y := (G₁ ⋙ sheafCompose J F).obj X) (NatTrans.app (sheafComposeNatTrans J F adj₁ adj₂) X)

Tactic:
apply forall_congr'

Premises used: forall_congr'