awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : Abelian.{w', w} D
J : GrothendieckTopology.{v, u} C
inst_3 : HasSheafify.{v, w', u, w} J D
⊢ Functor.Additive (D := Sheaf.{v, w', u, w} J D) (constantSheaf J D)

Tactic:
inferInstanceAs (Functor.const _ ⋙ presheafToSheaf _ _).Additive

Premises used: _private.0.CategoryTheory.instAdditiveSheafConstantSheaf._proof_1
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
inst_3 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J D
inst_4 : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf.{v₁, v_1, u₁, u_1} J E
change :
  Eq (α :=
    obj (sheafToPresheaf J E) (obj (𝟭 (Sheaf.{v₁, v_1, u₁, u_1} J E)) X) ⟶
      obj (sheafToPresheaf J E) ((composeAndSheafify J G ⋙ sheafCompose J F).obj X))
    (map (sheafToPresheaf J E) (NatTrans.app (Adjunction.unit (adjunction J adj)) X))
    (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (X.obj (P := Presheaf.IsSheaf J)) ≫
      whiskerRight (toSheafify J (X.obj (P := Presheaf.IsSheaf J) ⋙ G)) F)
⊢ Eq (α :=
    (obj (𝟭 (Sheaf.{v₁, v_1, u₁, u_1} J E)) X).obj (P := Presheaf.IsSheaf J) ⟶
      ((composeAndSheafify J G ⋙ sheafCompose J F).obj X).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.unit (adjunction J adj)) X))
    (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (X.obj (P := Presheaf.IsSheaf J)) ≫
      whiskerRight (toSheafify J (X.obj (P := Presheaf.IsSheaf J) ⋙ G)) F)

Tactic:
change (sheafToPresheaf _ _).map ((adjunction J adj).unit.app X) = _

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Sheaf.adjunction, CategoryTheory.Functor.map, CategoryTheory.NatTrans.app, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
inst_3 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J D
inst_4 : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf.{v₁, v_1, u₁, u_1} J E
simp :
  Eq (α :=
    obj (sheafToPresheaf J E) X ⟶
      obj (sheafToPresheaf J E) ((sheafCompose J F).obj (obj (presheafToSheaf J D) (obj (sheafToPresheaf J E) X ⋙ G))))
    (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (obj (sheafToPresheaf J E) X) ≫
      whiskerRight (toSheafify J (obj (sheafToPresheaf J E) X ⋙ G)) F)
    (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (X.obj (P := Presheaf.IsSheaf J)) ≫
      whiskerRight (toSheafify J (X.obj (P := Presheaf.IsSheaf J) ⋙ G)) F)
⊢ Eq (α :=
    obj (sheafToPresheaf J E) (obj (𝟭 (Sheaf.{v₁, v_1, u₁, u_1} J E)) X) ⟶
      obj (sheafToPresheaf J E) ((composeAndSheafify J G ⋙ sheafCompose J F).obj X))
    (map (sheafToPresheaf J E) (NatTrans.app (Adjunction.unit (adjunction J adj)) X))
    (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (X.obj (P := Presheaf.IsSheaf J)) ≫
      whiskerRight (toSheafify J (X.obj (P := Presheaf.IsSheaf J) ⋙ G)) F)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, whiskeringRight_obj_obj, adjunction,
    Adjunction.map_restrictFullyFaithful_unit_app, Adjunction.comp_unit_app,
    sheafificationAdjunction_unit_app, whiskeringRight_obj_map, Iso.refl_hom, NatTrans.id_app,
    Functor.comp_map, Functor.map_id, whiskerRight_id', Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.whiskerRight_id', CategoryTheory.Sheaf.adjunction, CategoryTheory.Category.comp_id, CategoryTheory.sheafificationAdjunction_unit_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.whiskeringRight_obj_map, CategoryTheory.Functor.id_obj, CategoryTheory.NatTrans.id_app, CategoryTheory.Functor.whiskeringRight_obj_obj, CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app, CategoryTheory.Iso.refl_hom, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.comp_unit_app
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
inst_3 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J D
inst_4 : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf.{v₁, v_1, u₁, u_1} J E
⊢ Eq (α :=
    obj (sheafToPresheaf J E) X ⟶
      obj (sheafToPresheaf J E) ((sheafCompose J F).obj (obj (presheafToSheaf J D) (obj (sheafToPresheaf J E) X ⋙ G))))
    (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (obj (sheafToPresheaf J E) X) ≫
      whiskerRight (toSheafify J (obj (sheafToPresheaf J E) X ⋙ G)) F)
    (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (X.obj (P := Presheaf.IsSheaf J)) ≫
      whiskerRight (toSheafify J (X.obj (P := Presheaf.IsSheaf J) ⋙ G)) F)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
inst_3 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J D
inst_4 : F.IsRightAdjoint
⊢ (sheafCompose J F).IsRightAdjoint

Tactic:
(adjunction J (Adjunction.ofIsRightAdjoint F)).isRightAdjoint

Premises used: CategoryTheory.Sheaf.adjunction, CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.Adjunction.ofIsRightAdjoint
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
inst_3 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J D
inst_4 : G.IsLeftAdjoint
⊢ (composeAndSheafify J G).IsLeftAdjoint

Tactic:
(adjunction J (Adjunction.ofIsLeftAdjoint G)).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Sheaf.adjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
⊢ F.IsRightAdjoint

Tactic:
have := adj.isRightAdjoint
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
rw :
  Function.Bijective (α := Q ⋙ G ⟶ R) (β := P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R)
    (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
      (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
        (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
      fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g)
⊢ Function.Bijective (β := P ⋙ G ⟶ R) fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g

Tactic:
rw [← ((adj.whiskerRight Cᵒᵖ).homEquiv P R).comp_bijective]

Premises used: Opposite, Equiv.comp_bijective, CategoryTheory.Adjunction.whiskerRight, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
⊢ Function.Bijective (α := obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R) (β := P ⟶ R ⋙ F)
    (⇑((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R).trans
          (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) hf (R ⋙ F) ⋯)) :
      (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R) → P ⟶ R ⋙ F)

Tactic:
(((adj.whiskerRight Cᵒᵖ).homEquiv Q R).trans
          (hf.homEquiv (R ⋙ F) ((sheafCompose J F).obj ⟨R, hR⟩).property)).bijective

Premises used: CategoryTheory.sheafCompose, CategoryTheory.ObjectProperty.FullSubcategory.mk, Opposite, Equiv.bijective, Equiv.trans, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.isLocal.homEquiv, CategoryTheory.Adjunction.whiskerRight, CategoryTheory.Adjunction.homEquiv, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
h :
  (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R) →
    (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F) →
      Eq (α := (Q ⋙ G ⟶ R) → (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R))
        (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
          (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
            (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
          fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g)
        (⇑((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R).trans
              (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) hf (R ⋙ F) ⋯)) :
          (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R) → P ⟶ R ⋙ F)
⊢ Function.Bijective (α := Q ⋙ G ⟶ R) (β := P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R)
    (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
      (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
        (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
      fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g)

Tactic:
convert!
      (((adj.whiskerRight Cᵒᵖ).homEquiv Q R).trans
          (hf.homEquiv (R ⋙ F) ((sheafCompose J F).obj ⟨R, hR⟩).property)).bijective

Premises used: CategoryTheory.sheafCompose, CategoryTheory.ObjectProperty.FullSubcategory.mk, Opposite, Equiv.bijective, Equiv.trans, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.isLocal.homEquiv, CategoryTheory.Adjunction.whiskerRight, CategoryTheory.Adjunction.homEquiv, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
h :
  ∀ (g : Q ⋙ G ⟶ R) (X : Cᵒᵖ),
    Eq.{v_1 + 1} (α := P.obj X ⟶ (obj (obj (whiskeringRight Cᵒᵖ D E) F) R).obj X)
      (NatTrans.app
        (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
          (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
            (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
          (fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g) g)
        X)
      (NatTrans.app
        (((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R).trans
              (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) hf (R ⋙ F) ⋯) :
            (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R) → P ⟶ R ⋙ F)
          g)
        X)
⊢ Eq (α := (Q ⋙ G ⟶ R) → (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R))
    (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
      (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
        (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
      fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g)
    (⇑((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R).trans
          (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) hf (R ⋙ F) ⋯)) :
      (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R) → P ⟶ R ⋙ F)

Tactic:
ext g X
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
h :
  Eq (α := P.obj X ⟶ F.obj (R.obj X))
    (NatTrans.app
        ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F)
          (whiskerRight f G ≫ g))
        X :
      P.obj X ⟶ (R ⋙ F).obj X)
    (f.app X ≫
      NatTrans.app ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g) X)
⊢ Eq.{v_1 + 1} (α := P.obj X ⟶ (obj (obj (whiskeringRight Cᵒᵖ D E) F) R).obj X)
    (NatTrans.app
      (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
        (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
          (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
        (fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g) g)
      X)
    (NatTrans.app
      (((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R).trans
            (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) hf (R ⋙ F) ⋯) :
          (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R) → P ⟶ R ⋙ F)
        g)
      X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
h :
  Eq (α := P.obj X ⟶ F.obj (R.obj X))
    (NatTrans.app
        ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F)
          (whiskerRight f G ≫ g))
        X :
      P.obj X ⟶ (R ⋙ F).obj X)
    (NatTrans.app (f ≫ (Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g) X)
⊢ Eq (α := P.obj X ⟶ F.obj (R.obj X))
    (NatTrans.app
        ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F)
          (whiskerRight f G ≫ g))
        X :
      P.obj X ⟶ (R ⋙ F).obj X)
    (f.app X ≫
      NatTrans.app ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g) X)

Tactic:
rw [← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
h :
  Eq (α := NatTrans P (R ⋙ F))
    ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F) (whiskerRight f G ≫ g) :
      P ⟶ R ⋙ F)
    (f ≫ (Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g : P ⟶ R ⋙ F)
⊢ Eq (α := P.obj X ⟶ F.obj (R.obj X))
    (NatTrans.app
        ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F)
          (whiskerRight f G ≫ g))
        X :
      P.obj X ⟶ (R ⋙ F).obj X)
    (NatTrans.app (f ≫ (Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g) X)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
⊢ Eq (α := NatTrans P (R ⋙ F))
    ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F) (whiskerRight f G ≫ g) :
      P ⟶ R ⋙ F)
    (f ≫ (Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g : P ⟶ R ⋙ F)

Tactic:
Adjunction.homEquiv_naturality_left _ _ _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
⊢ Eq (α := NatTrans P (R ⋙ F))
    ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F) (whiskerRight f G ≫ g) :
      P ⟶ R ⋙ F)
    (f ≫ (Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g : P ⟶ R ⋙ F)

Tactic:
exact Adjunction.homEquiv_naturality_left _ _ _

Premises used: CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
inst_3 : G.IsLeftAdjoint
⊢ J.PreservesSheafification G

Tactic:
preservesSheafification_of_adjunction J (Adjunction.ofIsLeftAdjoint G)

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Sheaf.preservesSheafification_of_adjunction
-- Module: Mathlib.CategoryTheory.Sites.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
inst_3 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J D
FD : D → D → Type u_2
CD : D → Type (max u₁ v₁)
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : J.HasSheafCompose (forget D (FC := FD) (CC := CD))
inst_7 : IsRightAdjoint (forget D (FC := FD) (CC := CD))
⊢ IsRightAdjoint (D := Sheaf.{v₁, v₂, u₁, u₂} J D) (sheafForget J (FD := FD) (CD := CD))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
rw : Presieve.IsSheafFor (X := Y) P (arrows ⊤)
⊢ Presieve.IsSheafFor P (Sieve.pullback f ⊤).arrows

Tactic:
rw [Sieve.pullback_top]

Premises used: CategoryTheory.Sieve.pullback_top
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor (X := Y) P (arrows ⊤)

Tactic:
Presieve.isSheafFor_top P

Premises used: CategoryTheory.Presieve.isSheafFor_top
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor (X := Y) P (arrows ⊤)

Tactic:
exact Presieve.isSheafFor_top P

Premises used: CategoryTheory.Presieve.isSheafFor_top
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
Z : C
g : Z ⟶ Y
rw : Presieve.IsSheafFor P (Sieve.pullback (g ≫ f) S).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback g (Sieve.pullback f S)).arrows

Tactic:
rw [← pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSheafFor P (Sieve.pullback (g ≫ f) S).arrows

Tactic:
apply hS
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback g R).arrows

Tactic:
Presieve.isSheafFor_trans P (pullback g S) _ (hS Z g) ?_ ?_

Premises used: CategoryTheory.Presieve.isSheafFor_trans, CategoryTheory.Sieve.pullback