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
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 :
  ∀ (x : Cᵒᵖ),
    (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)))).app
        x =
      (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))).app
        x
⊢ 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))

Tactic:
ext x
-- 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
x : Cᵒᵖ
h :
  U.map (F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (hT.from (Opposite.unop x)))) =
    CategoryStruct.comp (Y :=
      U.obj
        (obj.{v_1, v_2, u_1, u_2} (sheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))))
          x))
      (U.map (NatTrans.app (toSheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))) x))
      (U.map
        (NatTrans.app
          (sheafifyLift J (NatTrans.app (counit (constantPresheafAdj D hT)) (F.obj (P := Presheaf.IsSheaf J))) ⋯) x))
⊢ (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)))).app
      x =
    (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))).app
      x

Tactic:
simp [NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_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
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
x : Cᵒᵖ
⊢ U.map (F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (hT.from (Opposite.unop x)))) =
    CategoryStruct.comp (Y :=
      U.obj
        (obj.{v_1, v_2, u_1, u_2} (sheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))))
          x))
      (U.map (NatTrans.app (toSheafify J (obj (const Cᵒᵖ) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))) x))
      (U.map
        (NatTrans.app
          (sheafifyLift J (NatTrans.app (counit (constantPresheafAdj D hT)) (F.obj (P := Presheaf.IsSheaf J))) ⋯) x))

Tactic:
simp [← map_comp, ← NatTrans.comp_app]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_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
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
inst_7 : Faithful (constantSheaf J D)
inst_8 : Full (constantSheaf J D)
inst_9 : Faithful (constantSheaf J B)
inst_10 : Full (constantSheaf J B)
inst_11 : (sheafCompose J U).ReflectsIsomorphisms
inst_12 : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal.{v_1, u_1} T
rw :
  IsIso (X := (sheafCompose J U).obj (obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) 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)) :
      (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))
⊢ IsIso (X := (sheafCompose J U).obj (obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F))
    ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F))

Tactic:
rw [← constantSheafAdj_counit_w]

Premises used: CategoryTheory.constantSheafAdj_counit_w
-- 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
inst_7 : Faithful (constantSheaf J D)
inst_8 : Full (constantSheaf J D)
inst_9 : Faithful (constantSheaf J B)
inst_10 : Full (constantSheaf J B)
inst_11 : (sheafCompose J U).ReflectsIsomorphisms
inst_12 : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal.{v_1, u_1} T
⊢ IsIso (X := (sheafCompose J U).obj (obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) 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)) :
      (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))

Tactic:
infer_instance
-- 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
inst_7 : Faithful (constantSheaf J D)
inst_8 : Full (constantSheaf J D)
inst_9 : Faithful (constantSheaf J B)
inst_10 : Full (constantSheaf J B)
inst_11 : (sheafCompose J U).ReflectsIsomorphisms
inst_12 : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal.{v_1, u_1} T
⊢ IsIso (X := (sheafCompose J U).obj (obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F))
    ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F))

Tactic:
have : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)) := by
    rw [← constantSheafAdj_counit_w]
    infer_instance
-- 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
inst_7 : Faithful (constantSheaf J D)
inst_8 : Full (constantSheaf J D)
inst_9 : Faithful (constantSheaf J B)
inst_10 : Full (constantSheaf J B)
inst_11 : (sheafCompose J U).ReflectsIsomorphisms
inst_12 : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal.{v_1, u_1} T
this :
  IsIso (X := (sheafCompose J U).obj (obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F))
    ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F))
rw :
  IsIso (X := obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F)
    (NatTrans.app (counit (constantSheafAdj J D hT)) F)
⊢ IsConstant J F

Tactic:
rw [F.isConstant_iff_isIso_counit_app (hT := hT)]

Premises used: CategoryTheory.Sheaf.isConstant_iff_isIso_counit_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
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
inst_7 : Faithful (constantSheaf J D)
inst_8 : Full (constantSheaf J D)
inst_9 : Faithful (constantSheaf J B)
inst_10 : Full (constantSheaf J B)
inst_11 : (sheafCompose J U).ReflectsIsomorphisms
inst_12 : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal.{v_1, u_1} T
this :
  IsIso (X := (sheafCompose J U).obj (obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F))
    ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F))
⊢ IsIso (X := obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F)
    (NatTrans.app (counit (constantSheafAdj J D hT)) F)

Tactic:
isIso_of_reflects_iso _ (sheafCompose J U)

Premises used: CategoryTheory.sheafCompose, CategoryTheory.isIso_of_reflects_iso
-- 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
inst_7 : Faithful (constantSheaf J D)
inst_8 : Full (constantSheaf J D)
inst_9 : Faithful (constantSheaf J B)
inst_10 : Full (constantSheaf J B)
inst_11 : (sheafCompose J U).ReflectsIsomorphisms
inst_12 : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal.{v_1, u_1} T
this :
  IsIso (X := (sheafCompose J U).obj (obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F))
    ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F))
⊢ IsIso (X := obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F)
    (NatTrans.app (counit (constantSheafAdj J D hT)) F)

Tactic:
exact isIso_of_reflects_iso _ (sheafCompose J U)

Premises used: CategoryTheory.sheafCompose, CategoryTheory.isIso_of_reflects_iso
-- 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
h : IsConstant J F
obtain : ∀ (Y : D) (i : obj (constantSheaf J D) Y ≅ F), IsConstant J ((sheafCompose J U).obj F)
⊢ IsConstant J ((sheafCompose J U).obj F)

Tactic:
obtain ⟨Y, ⟨i⟩⟩ := 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
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
Y : D
i : obj (constantSheaf J D) Y ≅ F
⊢ IsConstant J ((sheafCompose J U).obj F)

Tactic:
⟨U.obj Y, ⟨(fullyFaithfulSheafToPresheaf _ _).preimageIso
    (((sheafifyComposeIso J U ((const Cᵒᵖ).obj Y)).symm ≪≫
      (presheafToSheaf J B ⋙ sheafToPresheaf J B).mapIso (constComp Cᵒᵖ Y U)).symm ≪≫
        (sheafToPresheaf _ _).mapIso ((sheafCompose J U).mapIso i))⟩⟩

Premises used: CategoryTheory.sheafCompose, Opposite, CategoryTheory.Functor.constComp, CategoryTheory.Functor.comp, CategoryTheory.presheafToSheaf, Nonempty.intro, CategoryTheory.sheafifyComposeIso, CategoryTheory.Functor.FullyFaithful.preimageIso, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.fullyFaithfulSheafToPresheaf, CategoryTheory.Sheaf.IsConstant.mk, CategoryTheory.Functor.const, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.sheafToPresheaf
-- 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
Y : D
i : obj (constantSheaf J D) Y ≅ F
⊢ IsConstant J ((sheafCompose J U).obj F)

Tactic:
exact ⟨U.obj Y, ⟨(fullyFaithfulSheafToPresheaf _ _).preimageIso
    (((sheafifyComposeIso J U ((const Cᵒᵖ).obj Y)).symm ≪≫
      (presheafToSheaf J B ⋙ sheafToPresheaf J B).mapIso (constComp Cᵒᵖ Y U)).symm ≪≫
        (sheafToPresheaf _ _).mapIso ((sheafCompose J U).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
F : Sheaf.{v_1, v_2, u_1, u_2} J D
inst_7 : Faithful (constantSheaf J D)
inst_8 : Full (constantSheaf J D)
inst_9 : Faithful (constantSheaf J B)
inst_10 : Full (constantSheaf J B)
inst_11 : (sheafCompose J U).ReflectsIsomorphisms
T : C
hT : IsTerminal.{v_1, u_1} T
⊢ IsConstant J F ↔ IsConstant J ((sheafCompose J U).obj F)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ Sheaf.isConstant_of_forget _ U F hT⟩

Premises used: inferInstance, CategoryTheory.Sheaf.isConstant_of_forget, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
x x_1 : (PreZeroHypercover.map F E.toPreZeroHypercover).I₀
j : E.I₁ x x_1
⊢ F.map (E.p₁ j) ≫ (PreZeroHypercover.map F E.toPreZeroHypercover).f x =
    F.map (E.p₂ j) ≫ (PreZeroHypercover.map F E.toPreZeroHypercover).f x_1

Tactic:
simpa using F.congr_map (E.w j)

Premises used: CategoryTheory.PreOneHypercover.w, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
⊢ E.map (𝟭 C) = E

Tactic:
rfl

Premises used: CategoryTheory.PreOneHypercover.map, CategoryTheory.PreZeroHypercover.map, rfl
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_2, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
D' : Type u_1
inst_2 : Category.{v_1, u_1} D'
G : Functor.{v₂, v_1, u₂, u_1} D D'
⊢ E.map (F ⋙ G) = (E.map F).map G

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.PreOneHypercover.map, CategoryTheory.PreZeroHypercover.map, rfl
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u
inst_3 : Category.{t, u} A
P : Functor.{v₂, t, u₂, u} Dᵒᵖ A
⊢ IsLimit ((E.map F).multifork P) ≃ IsLimit ((E.map F).multifork P)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
rw : E.sieve₁ p₁ p₂ ≤ Sieve.functorPullback F ((E.map F).sieve₁ (F.map p₁) (F.map p₂))
⊢ Sieve.functorPushforward F (E.sieve₁ p₁ p₂) ≤ (E.map F).sieve₁ (F.map p₁) (F.map p₂)

Tactic:
rw [Sieve.functorPushforward_le_iff_le_functorPullback]

Premises used: CategoryTheory.Sieve.functorPushforward_le_iff_le_functorPullback
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y : C
f : Y ⟶ W
this :
  ∀ (k : E.I₁ i₁ i₂) (u : Y ⟶ E.Y k) (hf₁ : f ≫ p₁ = u ≫ E.p₁ k) (hf₂ : f ≫ p₂ = u ≫ E.p₂ k),
    (Sieve.functorPullback F ((E.map F).sieve₁ (F.map p₁) (F.map p₂))).arrows f
⊢ (E.sieve₁ p₁ p₂).arrows f → (Sieve.functorPullback F ((E.map F).sieve₁ (F.map p₁) (F.map p₂))).arrows f

Tactic:
⟨k, u, hf₁, hf₂⟩
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y : C
f : Y ⟶ W
k : E.I₁ i₁ i₂
u : Y ⟶ E.Y k
hf₁ : f ≫ p₁ = u ≫ E.p₁ k
hf₂ : f ≫ p₂ = u ≫ E.p₂ k
⊢ F.map f ≫ F.map p₁ = F.map u ≫ (E.map F).p₁ k

Tactic:
simp [← Functor.map_comp, hf₁]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y : C
f : Y ⟶ W
k : E.I₁ i₁ i₂
u : Y ⟶ E.Y k
hf₁ : f ≫ p₁ = u ≫ E.p₁ k
hf₂ : f ≫ p₂ = u ≫ E.p₂ k
⊢ F.map f ≫ F.map p₂ = F.map u ≫ (E.map F).p₂ k

Tactic:
simp [← Functor.map_comp, hf₂]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y : C
f : Y ⟶ W
k : E.I₁ i₁ i₂
u : Y ⟶ E.Y k
hf₁ : f ≫ p₁ = u ≫ E.p₁ k
hf₂ : f ≫ p₂ = u ≫ E.p₂ k
⊢ (Sieve.functorPullback F ((E.map F).sieve₁ (F.map p₁) (F.map p₂))).arrows f

Tactic:
exact ⟨k, F.map u, by simp [← Functor.map_comp, hf₁], by simp [← Functor.map_comp, hf₂]⟩
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
⊢ HasPullback ((E.map F).f i₁) ((E.map F).f i₂)

Tactic:
have : HasPullback ((E.map F).f i₁) ((E.map F).f i₂) :=
    hasPullback_of_preservesPullback F (E.f i₁) (E.f i₂)
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ Eq (α := Sieve.{v₂, u₂} (F.obj (pullback (E.f i₁) (E.f i₂)))) (Sieve.functorPushforward F (E.sieve₁' i₁ i₂))
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
i₁ i₂ : E.I₀
inst_2 : HasPullback (E.f i₁) (E.f i₂)
inst_3 : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
refine_1 :
  LE.le (α := Sieve.{v₂, u₂} (F.obj (pullback (E.f i₁) (E.f i₂)))) (Sieve.functorPushforward F (E.sieve₁' i₁ i₂))
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))
refine_2 :
  LE.le (α := Sieve.{v₂, u₂} (F.obj (pullback (E.f i₁) (E.f i₂))))
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))
    (Sieve.functorPushforward F (E.sieve₁' i₁ i₂))
⊢ Eq (α := Sieve.{v₂, u₂} (F.obj (pullback (E.f i₁) (E.f i₂)))) (Sieve.functorPushforward F (E.sieve₁' i₁ i₂))
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm