awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
T : C
hT : IsTerminal.{v_1, u_1} T
X Y : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : X ⟶ Y
x : Cᵒᵖ
⊢ Eq (α :=
    obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X) x ⟶
      (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y).obj x)
    (NatTrans.app
      (map (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) f ≫
        {
          app := fun (x : Cᵒᵖ) ↦
            match (motive :=
              (x : Cᵒᵖ) →
                obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) Y) x ⟶
                  (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y).obj x)
              x with
            | Opposite.op X => Y.map (hT.from X).op,
          naturality := ⋯ })
      x)
    (NatTrans.app
      ({
          app := fun (x : Cᵒᵖ) ↦
            match (motive :=
              (x : Cᵒᵖ) →
                obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X) x ⟶
                  (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) X).obj x)
              x with
            | Opposite.op X_1 => X.map (hT.from X_1).op,
          naturality := ⋯ } ≫
        map (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) f)
      x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
F : Sheaf.{v_1, v_2, u_1, u_2} J D
inst_3 : IsConstant J F
⊢ essImage (constantSheaf J D) F

Tactic:
IsConstant.mem_essImage

Premises used: CategoryTheory.Sheaf.IsConstant.mem_essImage
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
F : Sheaf.{v_1, v_2, u_1, u_2} J D
X : D
i : F ≅ obj (constantSheaf J D) X
⊢ IsConstant J F

Tactic:
⟨_, ⟨i.symm⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Sheaf.IsConstant.mk
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
L : D ⥤ Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
adj : L ⊣ obj (sheafSections J D) (Opposite.op T)
F : Sheaf.{v_1, v_2, u_1, u_2} J D
rw : IsConstant J F ↔ essImage (constantSheaf J D) F
⊢ IsConstant J F ↔ L.essImage F

Tactic:
rw [essImage_eq_of_natIso (adj.leftAdjointUniq (constantSheafAdj J D hT))]

Premises used: CategoryTheory.Adjunction.leftAdjointUniq, CategoryTheory.Functor.essImage_eq_of_natIso, CategoryTheory.constantSheafAdj
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
L : D ⥤ Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
adj : L ⊣ obj (sheafSections J D) (Opposite.op T)
F : Sheaf.{v_1, v_2, u_1, u_2} J D
⊢ IsConstant J F ↔ essImage (constantSheaf J D) F

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: CategoryTheory.constantSheaf, CategoryTheory.Functor.essImage, _private.0.CategoryTheory.Sheaf.isConstant_iff_mem_essImage.match_1, Iff.intro, CategoryTheory.Sheaf.IsConstant.mk
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
L : D ⥤ Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
adj : L ⊣ obj (sheafSections J D) (Opposite.op T)
F : Sheaf.{v_1, v_2, u_1, u_2} J D
⊢ IsConstant J F ↔ essImage (constantSheaf J D) F

Tactic:
exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
inst_3 : Faithful (constantSheaf J D)
inst_4 : Full (constantSheaf J D)
F : Sheaf.{v_1, v_2, u_1, u_2} J D
inst_5 : IsConstant J F
T : C
hT : IsTerminal.{v_1, u_1} T
rw : essImage (constantSheaf J D) F
⊢ IsIso (X := obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F)
    (NatTrans.app (counit (constantSheafAdj J D hT)) F)

Tactic:
rw [isIso_counit_app_iff_mem_essImage]

Premises used: CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
inst_3 : Faithful (constantSheaf J D)
inst_4 : Full (constantSheaf J D)
F : Sheaf.{v_1, v_2, u_1, u_2} J D
inst_5 : IsConstant J F
T : C
hT : IsTerminal.{v_1, u_1} T
⊢ essImage (constantSheaf J D) F

Tactic:
F.mem_essImage_of_isConstant

Premises used: CategoryTheory.Sheaf.mem_essImage_of_isConstant
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
inst_3 : Faithful (constantSheaf J D)
inst_4 : Full (constantSheaf J D)
F : Sheaf.{v_1, v_2, u_1, u_2} J D
inst_5 : IsConstant J F
T : C
hT : IsTerminal.{v_1, u_1} T
⊢ essImage (constantSheaf J D) F

Tactic:
exact F.mem_essImage_of_isConstant

Premises used: CategoryTheory.Sheaf.mem_essImage_of_isConstant
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
inst_3 : Faithful (constantSheaf J D)
inst_4 : Full (constantSheaf J D)
F : Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
⊢ IsConstant J F ↔
    IsIso (X := obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F)
      (NatTrans.app (counit (constantSheafAdj J D hT)) F)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ ⟨_, ⟨asIso <| (constantSheafAdj J D hT).counit.app F⟩⟩⟩

Premises used: inferInstance, Nonempty.intro, CategoryTheory.constantSheafAdj, CategoryTheory.Adjunction.counit, Opposite.op, Iff.intro, Exists.intro, CategoryTheory.Sheaf.IsConstant.mk, CategoryTheory.sheafSections, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
L : D ⥤ Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
adj : L ⊣ obj (sheafSections J D) (Opposite.op T)
inst_3 : L.Faithful
inst_4 : L.Full
F : Sheaf.{v_1, v_2, u_1, u_2} J D
⊢ IsConstant J F ↔ IsIso (adj.counit.app F)

Tactic:
(isConstant_iff_mem_essImage J hT adj F).trans (isIso_counit_app_iff_mem_essImage adj).symm

Premises used: CategoryTheory.Sheaf.isConstant_iff_mem_essImage, Iff.trans, Iff.symm, CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
C' : Type u_3
inst_3 : Category.{v_3, u_3} C'
K : GrothendieckTopology.{v_3, u_3} C'
inst_4 : HasWeakSheafify.{v_3, v_2, u_3, u_2} K D
G : Functor.{v_1, v_3, u_1, u_3} C C'
inst_5 : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst_6 : IsDenseSubsite J K G
T : C
hT : IsTerminal.{v_1, u_1} T
hT' : IsTerminal.{v_3, u_3} (G.obj T)
F : Sheaf.{v_3, v_2, u_3, u_2} K D
mp : IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F) → IsConstant K F
mpr : IsConstant K F → IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F)
⊢ IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F) ↔ IsConstant K F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
C' : Type u_3
inst_3 : Category.{v_3, u_3} C'
K : GrothendieckTopology.{v_3, u_3} C'
inst_4 : HasWeakSheafify.{v_3, v_2, u_3, u_2} K D
G : Functor.{v_1, v_3, u_1, u_3} C C'
inst_5 : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst_6 : IsDenseSubsite J K G
T : C
hT : IsTerminal.{v_1, u_1} T
hT' : IsTerminal.{v_3, u_3} (G.obj T)
F : Sheaf.{v_3, v_2, u_3, u_2} K D
⊢ IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F) → IsConstant K F

Tactic:
fun ⟨Y, ⟨i⟩⟩ ↦ ⟨_, ⟨(equivCommuteConstant J D K G hT hT').symm.app _ ≪≫
      (sheafEquiv J K G D).functor.mapIso i ≪≫ (sheafEquiv J K G D).counitIso.app _⟩⟩

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Sheaf.IsConstant, Nonempty.intro, CategoryTheory.equivCommuteConstant, CategoryTheory.Iso.trans, _private.0.CategoryTheory.Sheaf.isConstant_iff_of_equivalence.match_1, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Sheaf.IsConstant.mk, CategoryTheory.Functor.IsDenseSubsite.sheafEquiv, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
C' : Type u_3
inst_3 : Category.{v_3, u_3} C'
K : GrothendieckTopology.{v_3, u_3} C'
inst_4 : HasWeakSheafify.{v_3, v_2, u_3, u_2} K D
G : Functor.{v_1, v_3, u_1, u_3} C C'
inst_5 : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst_6 : IsDenseSubsite J K G
T : C
hT : IsTerminal.{v_1, u_1} T
hT' : IsTerminal.{v_3, u_3} (G.obj T)
F : Sheaf.{v_3, v_2, u_3, u_2} K D
⊢ IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F) → IsConstant K F

Tactic:
exact fun ⟨Y, ⟨i⟩⟩ ↦ ⟨_, ⟨(equivCommuteConstant J D K G hT hT').symm.app _ ≪≫
      (sheafEquiv J K G D).functor.mapIso i ≪≫ (sheafEquiv J K G D).counitIso.app _⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
C' : Type u_3
inst_3 : Category.{v_3, u_3} C'
K : GrothendieckTopology.{v_3, u_3} C'
inst_4 : HasWeakSheafify.{v_3, v_2, u_3, u_2} K D
G : Functor.{v_1, v_3, u_1, u_3} C C'
inst_5 : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst_6 : IsDenseSubsite J K G
T : C
hT : IsTerminal.{v_1, u_1} T
hT' : IsTerminal.{v_3, u_3} (G.obj T)
F : Sheaf.{v_3, v_2, u_3, u_2} K D
⊢ IsConstant K F → IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F)

Tactic:
fun ⟨Y, ⟨i⟩⟩ ↦ ⟨_, ⟨(equivCommuteConstant' J D K G hT hT').app _ ≪≫
      (sheafEquiv J K G D).inverse.mapIso i⟩⟩

Premises used: _private.0.CategoryTheory.Sheaf.isConstant_iff_of_equivalence.match_2, CategoryTheory.equivCommuteConstant', CategoryTheory.Sheaf.IsConstant, Nonempty.intro, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Sheaf.IsConstant.mk, CategoryTheory.Functor.IsDenseSubsite.sheafEquiv, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
C' : Type u_3
inst_3 : Category.{v_3, u_3} C'
K : GrothendieckTopology.{v_3, u_3} C'
inst_4 : HasWeakSheafify.{v_3, v_2, u_3, u_2} K D
G : Functor.{v_1, v_3, u_1, u_3} C C'
inst_5 : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst_6 : IsDenseSubsite J K G
T : C
hT : IsTerminal.{v_1, u_1} T
hT' : IsTerminal.{v_3, u_3} (G.obj T)
F : Sheaf.{v_3, v_2, u_3, u_2} K D
⊢ IsConstant K F → IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F)

Tactic:
exact fun ⟨Y, ⟨i⟩⟩ ↦ ⟨_, ⟨(equivCommuteConstant' J D K G hT hT').app _ ≪≫
      (sheafEquiv J K G D).inverse.mapIso i⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
B : Type u_3
inst_3 : Category.{v_3, u_3} B
U : Functor.{v_2, v_3, u_2, u_3} D B
inst_4 : HasWeakSheafify.{v_1, v_3, u_1, u_3} J B
inst_5 : J.PreservesSheafification U
inst_6 : J.HasSheafCompose U
X : D
⊢ Eq (α :=
    ((constantSheaf J D ⋙ sheafCompose J U).obj X).obj (P := Presheaf.IsSheaf J) ⟶
      ((U ⋙ constantSheaf J B).obj X).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (NatTrans.app (Iso.hom (constantCommuteCompose J U)) X))
    (Iso.inv (sheafifyComposeIso J U (obj (const Cᵒᵖ) X)) ≫ sheafifyMap J (Iso.hom (constComp Cᵒᵖ X U)))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
B : Type u_3
inst_3 : Category.{v_3, u_3} B
U : Functor.{v_2, v_3, u_2, u_3} D B
inst_4 : HasWeakSheafify.{v_1, v_3, u_1, u_3} J B
inst_5 : J.PreservesSheafification U
inst_6 : J.HasSheafCompose U
F : Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
h :
  Eq (α :=
    ((constantSheaf J D ⋙ sheafCompose J U).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))).obj (P :=
        Presheaf.IsSheaf J) ⟶
      (obj (𝟭 (Sheaf.{v_1, v_3, u_1, u_3} J B)) ((sheafCompose J U).obj F)).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := (U ⋙ constantSheaf J B).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
        (NatTrans.app (Iso.hom (constantCommuteCompose J U)) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
        (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F))))
    (InducedCategory.Hom.hom ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F)))
⊢ Eq (α :=
    (constantSheaf J D ⋙ sheafCompose J U).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) ⟶
      obj (𝟭 (Sheaf.{v_1, v_3, u_1, u_3} J B)) ((sheafCompose J U).obj F))
    (CategoryStruct.comp (Y := (U ⋙ constantSheaf J B).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
      (NatTrans.app (Iso.hom (constantCommuteCompose J U)) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
      (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F)))
    ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F))

Tactic:
apply Sheaf.hom_ext

Premises used: CategoryTheory.Sheaf.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
B : Type u_3
inst_3 : Category.{v_3, u_3} B
U : Functor.{v_2, v_3, u_2, u_3} D B
inst_4 : HasWeakSheafify.{v_1, v_3, u_1, u_3} J B
inst_5 : J.PreservesSheafification U
inst_6 : J.HasSheafCompose U
F : Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
h :
  Eq (α :=
    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
          (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
        U ⟶
      F.obj (P := Presheaf.IsSheaf J) ⋙ U)
    (CategoryStruct.comp (Y :=
        ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
          (obj (constantSheaf J B) (U.obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))))
        (InducedCategory.Hom.hom
          (NatTrans.app (Iso.hom (constantCommuteCompose J U)) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))))
        (InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F))) :
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
            (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
          U ⟶
        F.obj (P := Presheaf.IsSheaf J) ⋙ U)
    (whiskerRight (InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J D hT)) F)) U :
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
            (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
          U ⟶
        F.obj (P := Presheaf.IsSheaf J) ⋙ U)
⊢ Eq (α :=
    ((constantSheaf J D ⋙ sheafCompose J U).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))).obj (P :=
        Presheaf.IsSheaf J) ⟶
      (obj (𝟭 (Sheaf.{v_1, v_3, u_1, u_3} J B)) ((sheafCompose J U).obj F)).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := (U ⋙ constantSheaf J B).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
        (NatTrans.app (Iso.hom (constantCommuteCompose J U)) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
        (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F))))
    (InducedCategory.Hom.hom ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
B : Type u_3
inst_3 : Category.{v_3, u_3} B
U : Functor.{v_2, v_3, u_2, u_3} D B
inst_4 : HasWeakSheafify.{v_1, v_3, u_1, u_3} J B
inst_5 : J.PreservesSheafification U
inst_6 : J.HasSheafCompose U
F : Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
h :
  Eq (α :=
    sheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) ⋙ U) ⟶
      F.obj (P := Presheaf.IsSheaf J) ⋙ U)
    (sheafifyMap J (Iso.hom (constComp Cᵒᵖ (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) U)) ≫
      InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F)))
    (CategoryStruct.comp (Y :=
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
          (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
        U)
      (Iso.hom (sheafifyComposeIso J U (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))))
      (whiskerRight (InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J D hT)) F)) U))
⊢ Eq (α :=
    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
          (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
        U ⟶
      F.obj (P := Presheaf.IsSheaf J) ⋙ U)
    (CategoryStruct.comp (Y :=
        ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
          (obj (constantSheaf J B) (U.obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))))
        (InducedCategory.Hom.hom
          (NatTrans.app (Iso.hom (constantCommuteCompose J U)) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))))
        (InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F))) :
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
            (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
          U ⟶
        F.obj (P := Presheaf.IsSheaf J) ⋙ U)
    (whiskerRight (InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J D hT)) F)) U :
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
            (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
          U ⟶
        F.obj (P := Presheaf.IsSheaf J) ⋙ U)

Tactic:
rw [constantCommuteCompose_hom_app_hom, assoc, Iso.inv_comp_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_comp_eq, CategoryTheory.constantCommuteCompose_hom_app_hom
-- Module: Mathlib.CategoryTheory.Sites.ConstantSheaf
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
B : Type u_3
inst_3 : Category.{v_3, u_3} B
U : Functor.{v_2, v_3, u_2, u_3} D B
inst_4 : HasWeakSheafify.{v_1, v_3, u_1, u_3} J B
inst_5 : J.PreservesSheafification U
inst_6 : J.HasSheafCompose U
F : Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
h :
  CategoryStruct.comp (Y := sheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) ⋙ U))
      (toSheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) ⋙ U))
      (sheafifyMap J (Iso.hom (constComp Cᵒᵖ (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) U)) ≫
        InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F))) =
    CategoryStruct.comp (Y := sheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) ⋙ U))
      (toSheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) ⋙ U))
      (CategoryStruct.comp (Y :=
        ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
            (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
          U)
        (Iso.hom (sheafifyComposeIso J U (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))))
        (whiskerRight (InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J D hT)) F)) U))
⊢ Eq (α :=
    sheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) ⋙ U) ⟶
      F.obj (P := Presheaf.IsSheaf J) ⋙ U)
    (sheafifyMap J (Iso.hom (constComp Cᵒᵖ (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) U)) ≫
      InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F)))
    (CategoryStruct.comp (Y :=
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
          (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
        U)
      (Iso.hom (sheafifyComposeIso J U (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))))
      (whiskerRight (InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J D hT)) F)) U))

Tactic:
apply sheafify_hom_ext _ _ _ ((sheafCompose J U).obj F).property

Premises used: CategoryTheory.sheafCompose, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.obj, CategoryTheory.sheafify_hom_ext