awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
⊢ Eq (α := P ⟶ sheafify J Q) (η ≫ toSheafify J Q) (toSheafify J P ≫ sheafifyMap J η)

Tactic:
sheafificationAdjunction J D |>.unit.naturality η

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.sheafificationAdjunction, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
⊢ Functor.obj (sheafification J D) P = sheafify J P

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
⊢ Eq (α := Functor.obj (sheafification J D) P ⟶ Functor.obj (sheafification J D) Q) (Functor.map (sheafification J D) η)
    (sheafifyMap J η)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
⊢ Eq (α := Functor.obj (𝟭 (Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D)) P ⟶ Functor.obj (sheafification J D) P)
    (NatTrans.app (toSheafification J D) P) (toSheafify J P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (Y := sheafify J P) (toSheafify J P)

Tactic:
⟨(sheafificationAdjunction J D |>.counit.app ⟨P, hP⟩).hom, ?_, ?_⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.counit, And.intro, Exists.intro, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.IsIso.mk, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
refine_1 :
  CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    𝟙 P
refine_2 :
  InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      toSheafify J P =
    𝟙 (sheafify J P)
⊢ IsIso (Y := sheafify J P) (toSheafify J P)

Tactic:
refine ⟨(sheafificationAdjunction J D |>.counit.app ⟨P, hP⟩).hom, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
refine_1 :
  CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    NatTrans.app (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D)))
      (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    𝟙 P

Tactic:
change _ = (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Cᵒᵖ ⥤ D)) :).app ⟨P, hP⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Functor, Opposite, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.CategoryStruct.id, CategoryTheory.NatTrans.app, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
refine_1 :
  CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    NatTrans.app
      (CategoryStruct.comp (Y := sheafToPresheaf J D ⋙ presheafToSheaf J D ⋙ sheafToPresheaf J D)
        (Functor.whiskerLeft (sheafToPresheaf J D) (Adjunction.unit (sheafificationAdjunction J D)))
        (Functor.whiskerRight (Adjunction.counit (sheafificationAdjunction J D)) (sheafToPresheaf J D)))
      (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    NatTrans.app (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D)))
      (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)

Tactic:
rw [← sheafificationAdjunction J D |>.right_triangle]

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.right_triangle
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))) =
    NatTrans.app
      (CategoryStruct.comp (Y := sheafToPresheaf J D ⋙ presheafToSheaf J D ⋙ sheafToPresheaf J D)
        (Functor.whiskerLeft (sheafToPresheaf J D) (Adjunction.unit (sheafificationAdjunction J D)))
        (Functor.whiskerRight (Adjunction.counit (sheafificationAdjunction J D)) (sheafToPresheaf J D)))
      (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
refine_2 :
  Eq (α :=
    Functor.obj (sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
      sheafify J P)
    (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      toSheafify J P)
    (𝟙 (sheafify J P))
⊢ InducedCategory.Hom.hom
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      toSheafify J P =
    𝟙 (sheafify J P)

Tactic:
change (sheafToPresheaf _ _).map _ ≫ _ = _

Premises used: CategoryTheory.Functor.map, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
refine_2 :
  Eq (α :=
    Functor.obj (sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
      Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
    (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
    (𝟙 (sheafify J P))
⊢ Eq (α :=
    Functor.obj (sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
      sheafify J P)
    (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      toSheafify J P)
    (𝟙 (sheafify J P))

Tactic:
change _ ≫ (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj ⟨P, hP⟩) = _

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Adjunction.unit, CategoryTheory.sheafificationAdjunction, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
refine_2 :
  Eq (α :=
    Functor.obj (sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
      Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
    (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      inv
        (Functor.map (sheafToPresheaf J D)
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))))
    (𝟙 (sheafify J P))
⊢ Eq (α :=
    Functor.obj (sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
      Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
    (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
    (𝟙 (sheafify J P))

Tactic:
rw [← (sheafificationAdjunction J D).inv_counit_map (X := ⟨P, hP⟩)]

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.inv_counit_map
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ Eq (α :=
    Functor.obj (sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D)
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ⟶
      Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
        (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)))
    (Functor.map (sheafToPresheaf J D)
        (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP)) ≫
      inv
        (Functor.map (sheafToPresheaf J D)
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) P hP))))
    (𝟙 (sheafify J P))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ Eq (α := P ⟶ sheafify J P) (Iso.hom (isoSheafify J hP)) (toSheafify J P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Sheaf.{v₁, v_1, u₁, u_1} J D
⊢ Eq (α :=
    (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) P).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (𝟭 (Sheaf.{v₁, v_1, u₁, u_1} J D)) P).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) P))
    (InducedCategory.Hom.hom
      (Functor.map (presheafToSheaf J D) (𝟙 (P.obj (P := Presheaf.IsSheaf J))) ≫
        NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
          (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) (P.obj (P := Presheaf.IsSheaf J)) ⋯)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
change :
  CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D) (Functor.obj (presheafToSheaf J D) P))
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P)
      (Functor.map (sheafToPresheaf J D) (Functor.map (presheafToSheaf J D) η) ≫
        InducedCategory.Hom.hom
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η
⊢ CategoryStruct.comp (Y := sheafify J P) (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P)
      (InducedCategory.Hom.hom
        (Functor.map (presheafToSheaf J D) η ≫
          NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η

Tactic:
change _ ≫ (sheafToPresheaf J D).map _ ≫ _ = _

Premises used: CategoryTheory.Functor.map, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
simp :
  η ≫
      CategoryStruct.comp (Y :=
        Functor.obj (sheafToPresheaf J D)
          (Functor.obj (presheafToSheaf J D)
            (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))))
        (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (InducedCategory.Hom.hom
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η
⊢ CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D) (Functor.obj (presheafToSheaf J D) P))
      (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P)
      (Functor.map (sheafToPresheaf J D) (Functor.map (presheafToSheaf J D) η) ≫
        InducedCategory.Hom.hom
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η

Tactic:
simp only [Adjunction.unit_naturality_assoc]

Premises used: CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
change :
  η ≫
      CategoryStruct.comp (Y :=
        Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (InducedCategory.Hom.hom
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η
⊢ η ≫
      CategoryStruct.comp (Y :=
        Functor.obj (sheafToPresheaf J D)
          (Functor.obj (presheafToSheaf J D)
            (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))))
        (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (InducedCategory.Hom.hom
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η

Tactic:
change _ ≫ (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj ⟨Q, hQ⟩) ≫ _ = _

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Adjunction.unit, CategoryTheory.sheafificationAdjunction, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
change :
  η ≫
      CategoryStruct.comp (Y :=
        Functor.obj (sheafToPresheaf J D)
          (Functor.obj (presheafToSheaf J D)
            (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))))
        (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (Functor.map (sheafToPresheaf J D)
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η
⊢ η ≫
      CategoryStruct.comp (Y :=
        Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D)
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (InducedCategory.Hom.hom
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η

Tactic:
change _ ≫ _ ≫ (sheafToPresheaf J D).map _ = _

Premises used: CategoryTheory.Functor.map, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
rw : η ≫ 𝟙 (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)) = η
⊢ η ≫
      CategoryStruct.comp (Y :=
        Functor.obj (sheafToPresheaf J D)
          (Functor.obj (presheafToSheaf J D)
            (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))))
        (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D))
          (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)))
        (Functor.map (sheafToPresheaf J D)
          (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D))
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ))) =
    η

Tactic:
rw [sheafificationAdjunction J D |>.right_triangle_components (Y := ⟨Q, hQ⟩)]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ η ≫ 𝟙 (Functor.obj (sheafToPresheaf J D) (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)) = η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : toSheafify J P ≫ γ = η
⊢ NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P ≫ γ = η

Tactic:
rw [toSheafify] at h

Premises used: CategoryTheory.toSheafify
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P ≫ γ = η
γ' : Functor.obj (presheafToSheaf J D) P ⟶ ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ :=
  { hom := γ }
change :
  γ'.hom =
    InducedCategory.Hom.hom
      ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J D) P
              (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)) :
          (a : P ⟶ (sheafToPresheaf J D).obj { obj := Q, property := hQ }) →
            (presheafToSheaf J D).obj P ⟶ { obj := Q, property := hQ })
        η)
⊢ γ =
    InducedCategory.Hom.hom
      ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J D) P
              (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) Q hQ)) :
          (a : P ⟶ (sheafToPresheaf J D).obj { obj := Q, property := hQ }) →
            (presheafToSheaf J D).obj P ⟶ { obj := Q, property := hQ })
        η)

Tactic:
change γ'.hom = _

Premises used: CategoryTheory.InducedCategory.Hom.hom