awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
V U : Cᵒᵖ
f : U ⟶ V
⊢ Eq (α := Functor.obj (Γ J A) F ⟶ F.obj (P := Presheaf.IsSheaf J).obj V)
    (F.ΓRes U ≫ F.obj (P := Presheaf.IsSheaf J).map f) (F.ΓRes V)

Tactic:
F.coneΓ.w f

Premises used: CategoryTheory.Sheaf.coneΓ, CategoryTheory.Sheaf.ΓRes, CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F : Sheaf.{v, v₂, u, u₂} J A
U : Cᵒᵖ
⊢ F.coneΓ.π.app U = F.ΓRes U

Tactic:
rfl

Premises used: CategoryTheory.Sheaf.ΓRes, rfl
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F G : Sheaf.{v, v₂, u, u₂} J A
f : F ⟶ G
U : Cᵒᵖ
⊢ Eq (α := Functor.obj (Γ J A) F ⟶ G.obj (P := Presheaf.IsSheaf J).obj U) (Functor.map (Γ J A) f ≫ G.ΓRes U)
    (F.ΓRes U ≫ f.hom.app U)

Tactic:
.trans ?_ <| congr_app (ΓHomEquiv_naturality_right_symm _ _) U

Premises used: CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm, CategoryTheory.congr_app, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F G : Sheaf.{v, v₂, u, u₂} J A
f : F ⟶ G
U : Cᵒᵖ
refine :
  Eq (α := Functor.obj (Γ J A) F ⟶ G.obj (P := Presheaf.IsSheaf J).obj U) (Functor.map (Γ J A) f ≫ G.ΓRes U)
    (NatTrans.app
      ((Equiv.symm ΓHomEquiv : (a : (Γ J A).1 F ⟶ (Γ J A).obj G) → (Functor.const Cᵒᵖ).obj ((Γ J A).1 F) ⟶ G.obj)
        (𝟙 (Functor.obj (Γ J A) F) ≫ Functor.map (Γ J A) f))
      U)
⊢ Eq (α := Functor.obj (Γ J A) F ⟶ G.obj (P := Presheaf.IsSheaf J).obj U) (Functor.map (Γ J A) f ≫ G.ΓRes U)
    (F.ΓRes U ≫ f.hom.app U)

Tactic:
refine .trans ?_ <| congr_app (ΓHomEquiv_naturality_right_symm _ _) U

Premises used: CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F G : Sheaf.{v, v₂, u, u₂} J A
f : F ⟶ G
U : Cᵒᵖ
⊢ Eq.{v₂ + 1} (α :=
    Functor.obj.{v, v₂, u, u₂} (Functor.obj (Functor.const Cᵒᵖ) (Functor.obj (Γ J A) F)) U ⟶
      G.obj (P := Presheaf.IsSheaf J).obj U)
    (NatTrans.app
      ((Equiv.symm ΓHomEquiv : (a : (Γ J A).obj F ⟶ (Γ J A).obj G) → (Functor.const Cᵒᵖ).obj ((Γ J A).obj F) ⟶ G.obj)
        (Functor.map (Γ J A) f ≫ 𝟙 (Functor.obj (Γ J A) G)))
      U)
    (NatTrans.app
      ((Equiv.symm ΓHomEquiv : (a : (Γ J A).1 F ⟶ (Γ J A).obj G) → (Functor.const Cᵒᵖ).obj ((Γ J A).1 F) ⟶ G.obj)
        (𝟙 (Functor.obj (Γ J A) F) ≫ Functor.map (Γ J A) f))
      U)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasGlobalSectionsFunctor.{u, v, u₂, v₂} J A
F G : Sheaf.{v, v₂, u, u₂} J A
f : F ⟶ G
U : Cᵒᵖ
⊢ Eq (α := Functor.obj (Γ J A) F ⟶ G.obj (P := Presheaf.IsSheaf J).obj U) (Functor.map (Γ J A) f ≫ G.ΓRes U)
    (NatTrans.app
      ((Equiv.symm ΓHomEquiv : (a : (Γ J A).1 F ⟶ (Γ J A).obj G) → (Functor.const Cᵒᵖ).obj ((Γ J A).1 F) ⟶ G.obj)
        (𝟙 (Functor.obj (Γ J A) F) ≫ Functor.map (Γ J A) f))
      U)

Tactic:
exact (congr_app (ΓHomEquiv_naturality_left_symm ((Γ J A).map f) (𝟙 _)) U).symm.trans (by simp)

Premises used: CategoryTheory.Sheaf.ΓHomEquiv_naturality_left_symm, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, CategoryTheory.Sheaf.Γ, Eq.symm, CategoryTheory.congr_app, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
inst_3 : HasWeakSheafify J (Type w)
inst_4 : HasGlobalSectionsFunctor J (Type w)
F : Sheaf J (Type w)
⊢ Functor.obj (Γ J (Type w)) F ≃ (PUnit.{w + 1} ⟶ Functor.obj (Γ J (Type w)) F)

Tactic:
exact (Equiv.funUnique (PUnit) _).symm.trans TypeCat.homEquiv.symm

Premises used: Equiv.trans, TypeCat.homEquiv, PUnit, Equiv.funUnique, Equiv.symm
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type w)
inst_2 : HasGlobalSectionsFunctor J (Type w)
F G : Sheaf J (Type w)
f : F ⟶ G
x : Functor.obj (Γ J (Type w)) F
dsimp :
  Eq (α := (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    (((G.obj (P := Presheaf.IsSheaf J).sectionsEquivHom PUnit.{w + 1}).symm :
          (a : (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ G.obj) → (↑G.obj.sections : Type (max u w)))
        ((Equiv.symm ΓHomEquiv :
            (a : PUnit.{w + 1} ⟶ (Γ J (Type w)).obj G) → (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ G.obj)
          (↾uniqueElim (α := fun (a : PUnit.{w + 1}) ↦ Functor.obj (Γ J (Type w)) G)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Γ J (Type w)) f) :
                  (a : (Γ J (Type w)).obj F) → (Γ J (Type w)).obj G)
                x))) :
      (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    (({
            toFun := fun (x : (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u w))) ↦
              Subtype.mk (p := fun (x : (j : Cᵒᵖ) → G.obj (P := Presheaf.IsSheaf J).obj j) ↦
                x ∈ G.obj (P := Presheaf.IsSheaf J).sections)
                (fun (j : Cᵒᵖ) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app j) : (a : F.obj.obj j) → G.obj.obj j)
                    ((↑x : (j : Cᵒᵖ) → F.obj.obj j) j))
                ⋯ } :
          (a : (↑F.obj.sections : Type (max u w))) → (↑G.obj.sections : Type (max u w)))
        (((F.obj (P := Presheaf.IsSheaf J).sectionsEquivHom PUnit.{w + 1}).symm :
            (a : (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ F.obj) → (↑F.obj.sections : Type (max u w)))
          ((Equiv.symm ΓHomEquiv :
              (a : PUnit.{w + 1} ⟶ (Γ J (Type w)).obj F) → (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ F.obj)
            (↾uniqueElim (α := fun (a : PUnit.{w + 1}) ↦ Functor.obj (Γ J (Type w)) F) x))) :
      (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
⊢ Eq (α := (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    ((ΓObjEquivSections J G : (a : (Γ J (Type w)).obj G) → (↑G.obj.sections : Type (max u w)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Γ J (Type w)) f) :
            (a : (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj F)) → (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj G))
          x) :
      (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.sectionsFunctor Cᵒᵖ) f.hom) :
          (a : (fun (X : Type (max u w)) ↦ X) ((Functor.sectionsFunctor Cᵒᵖ).obj F.obj)) →
            (fun (X : Type (max u w)) ↦ X) ((Functor.sectionsFunctor Cᵒᵖ).obj G.obj))
        ((ΓObjEquivSections J F : (a : (Γ J (Type w)).obj F) → (↑F.obj.sections : Type (max u w))) x) :
      (fun (X : Type (max u w)) ↦ X) (Functor.obj (Functor.sectionsFunctor Cᵒᵖ) (G.obj (P := Presheaf.IsSheaf J))))

Tactic:
dsimp [ΓObjEquivSections]

Premises used: CategoryTheory.Sheaf.ΓObjEquivSections
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type w)
inst_2 : HasGlobalSectionsFunctor J (Type w)
F G : Sheaf J (Type w)
f : F ⟶ G
x : Functor.obj (Γ J (Type w)) F
⊢ Eq (α := (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    (((G.obj (P := Presheaf.IsSheaf J).sectionsEquivHom PUnit.{w + 1}).symm :
          (a : (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ G.obj) → (↑G.obj.sections : Type (max u w)))
        ((Equiv.symm ΓHomEquiv :
            (a : PUnit.{w + 1} ⟶ (Γ J (Type w)).obj G) → (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ G.obj)
          (↾uniqueElim (α := fun (a : PUnit.{w + 1}) ↦ Functor.obj (Γ J (Type w)) G)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Γ J (Type w)) f) :
                  (a : (Γ J (Type w)).obj F) → (Γ J (Type w)).obj G)
                x))) :
      (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    (({
            toFun := fun (x : (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u w))) ↦
              Subtype.mk (p := fun (x : (j : Cᵒᵖ) → G.obj (P := Presheaf.IsSheaf J).obj j) ↦
                x ∈ G.obj (P := Presheaf.IsSheaf J).sections)
                (fun (j : Cᵒᵖ) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app j) : (a : F.obj.obj j) → G.obj.obj j)
                    ((↑x : (j : Cᵒᵖ) → F.obj.obj j) j))
                ⋯ } :
          (a : (↑F.obj.sections : Type (max u w))) → (↑G.obj.sections : Type (max u w)))
        (((F.obj (P := Presheaf.IsSheaf J).sectionsEquivHom PUnit.{w + 1}).symm :
            (a : (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ F.obj) → (↑F.obj.sections : Type (max u w)))
          ((Equiv.symm ΓHomEquiv :
              (a : PUnit.{w + 1} ⟶ (Γ J (Type w)).obj F) → (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ F.obj)
            (↾uniqueElim (α := fun (a : PUnit.{w + 1}) ↦ Functor.obj (Γ J (Type w)) F) x))) :
      (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))

Tactic:
(congr_arg _ (ΓHomEquiv_naturality_right_symm (↾(uniqueElim x)) f)).trans
    (Functor.sectionsEquivHom_naturality_symm _ _ _)

Premises used: Eq.mpr, TypeCat.ofHom, TypeCat.Fun.comp, congr_arg, CategoryTheory.Functor.sectionsEquivHom_naturality_symm, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm, uniqueElim, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type w)
inst_2 : HasGlobalSectionsFunctor J (Type w)
F G : Sheaf J (Type w)
f : F ⟶ G
x : Functor.obj (Γ J (Type w)) F
⊢ Eq (α := (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    (((G.obj (P := Presheaf.IsSheaf J).sectionsEquivHom PUnit.{w + 1}).symm :
          (a : (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ G.obj) → (↑G.obj.sections : Type (max u w)))
        ((Equiv.symm ΓHomEquiv :
            (a : PUnit.{w + 1} ⟶ (Γ J (Type w)).obj G) → (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ G.obj)
          (↾uniqueElim (α := fun (a : PUnit.{w + 1}) ↦ Functor.obj (Γ J (Type w)) G)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Γ J (Type w)) f) :
                  (a : (Γ J (Type w)).obj F) → (Γ J (Type w)).obj G)
                x))) :
      (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))
    (({
            toFun := fun (x : (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u w))) ↦
              Subtype.mk (p := fun (x : (j : Cᵒᵖ) → G.obj (P := Presheaf.IsSheaf J).obj j) ↦
                x ∈ G.obj (P := Presheaf.IsSheaf J).sections)
                (fun (j : Cᵒᵖ) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app j) : (a : F.obj.obj j) → G.obj.obj j)
                    ((↑x : (j : Cᵒᵖ) → F.obj.obj j) j))
                ⋯ } :
          (a : (↑F.obj.sections : Type (max u w))) → (↑G.obj.sections : Type (max u w)))
        (((F.obj (P := Presheaf.IsSheaf J).sectionsEquivHom PUnit.{w + 1}).symm :
            (a : (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ F.obj) → (↑F.obj.sections : Type (max u w)))
          ((Equiv.symm ΓHomEquiv :
              (a : PUnit.{w + 1} ⟶ (Γ J (Type w)).obj F) → (Functor.const Cᵒᵖ).obj PUnit.{w + 1} ⟶ F.obj)
            (↾uniqueElim (α := fun (a : PUnit.{w + 1}) ↦ Functor.obj (Γ J (Type w)) F) x))) :
      (↑G.obj (P := Presheaf.IsSheaf J).sections : Type (max u w)))

Tactic:
exact (congr_arg _ (ΓHomEquiv_naturality_right_symm (↾(uniqueElim x)) f)).trans
    (Functor.sectionsEquivHom_naturality_symm _ _ _)

Premises used: TypeCat.ofHom, congr_arg, CategoryTheory.Functor.sectionsEquivHom_naturality_symm, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm, uniqueElim, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type w)
inst_2 : HasGlobalSectionsFunctor J (Type w)
F G : Sheaf J (Type w)
f : F ⟶ G
x : (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u w))
⊢ Eq (α := Functor.obj (Γ J (Type w)) G)
    ((Equiv.symm (ΓObjEquivSections J G) : (a : (↑G.obj.sections : Type (max u w))) → (Γ J (Type w)).obj G)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.sectionsFunctor Cᵒᵖ) f.hom) :
            (a : (fun (X : Type (max u w)) ↦ X) ((Functor.sectionsFunctor Cᵒᵖ).obj F.obj)) →
              (fun (X : Type (max u w)) ↦ X) ((Functor.sectionsFunctor Cᵒᵖ).obj G.obj))
          x) :
      Functor.obj (Γ J (Type w)) G)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Γ J (Type w)) f) :
          (a : (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj F)) → (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj G))
        ((Equiv.symm (ΓObjEquivSections J F) : (a : (↑F.obj.sections : Type (max u w))) → (Γ J (Type w)).obj F) x :
          Functor.obj (Γ J (Type w)) F) :
      (fun (X : Type w) ↦ X) (Functor.obj (Γ J (Type w)) G))

Tactic:
ConcreteCategory.congr_hom (ΓHomEquiv_naturality_right (F.obj.sectionsEquivHom _ x) f) _

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.ObjectProperty.FullSubcategory.obj, TypeCat.Fun.comp, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right, CategoryTheory.ConcreteCategory.congr_hom, DFunLike.coe, CategoryTheory.Functor.sectionsEquivHom
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
X Y : Sheaf J (Type (max u v))
f : X ⟶ Y
h :
  ∀ (x : Functor.obj (Γ J (Type (max u v))) X),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Γ J (Type (max u v))) f ≫
            Iso.hom
              ((fun (F : Sheaf J (Type (max u v))) ↦
                  (Equiv.toIso (ΓObjEquivSections J F) :
                    Functor.obj (Γ J (Type (max u v))) F ≅
                      (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
                Y)))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (F : Sheaf J (Type (max u v))) ↦
                  (Equiv.toIso (ΓObjEquivSections J F) :
                    Functor.obj (Γ J (Type (max u v))) F ≅
                      (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
                X) ≫
            (sheafToPresheaf J (Type (max u v)) ⋙ Functor.sectionsFunctor Cᵒᵖ).map f))
        x
⊢ Eq (α :=
    Functor.obj (Γ J (Type (max u v))) X ⟶ (sheafToPresheaf J (Type (max u v)) ⋙ Functor.sectionsFunctor Cᵒᵖ).obj Y)
    (Functor.map (Γ J (Type (max u v))) f ≫
      Iso.hom
        ((fun (F : Sheaf J (Type (max u v))) ↦
            (Equiv.toIso (ΓObjEquivSections J F) :
              Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
          Y))
    (Iso.hom
        ((fun (F : Sheaf J (Type (max u v))) ↦
            (Equiv.toIso (ΓObjEquivSections J F) :
              Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
          X) ≫
      (sheafToPresheaf J (Type (max u v)) ⋙ Functor.sectionsFunctor Cᵒᵖ).map f)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
X Y : Sheaf J (Type (max u v))
f : X ⟶ Y
x : Functor.obj (Γ J (Type (max u v))) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Γ J (Type (max u v))) f ≫
          Iso.hom
            ((fun (F : Sheaf J (Type (max u v))) ↦
                (Equiv.toIso (ΓObjEquivSections J F) :
                  Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
              Y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (F : Sheaf J (Type (max u v))) ↦
                (Equiv.toIso (ΓObjEquivSections J F) :
                  Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
              X) ≫
          (sheafToPresheaf J (Type (max u v)) ⋙ Functor.sectionsFunctor Cᵒᵖ).map f))
      x

Tactic:
ΓObjEquivSections_naturality J f x

Premises used: Set.Mem, CategoryTheory.Sheaf.ΓObjEquivSections_naturality
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
X Y : Sheaf J (Type (max u v))
f : X ⟶ Y
x : Functor.obj (Γ J (Type (max u v))) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Γ J (Type (max u v))) f ≫
          Iso.hom
            ((fun (F : Sheaf J (Type (max u v))) ↦
                (Equiv.toIso (ΓObjEquivSections J F) :
                  Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
              Y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (F : Sheaf J (Type (max u v))) ↦
                (Equiv.toIso (ΓObjEquivSections J F) :
                  Functor.obj (Γ J (Type (max u v))) F ≅ (↑F.obj (P := Presheaf.IsSheaf J).sections : Type (max u v))))
              X) ≫
          (sheafToPresheaf J (Type (max u v)) ⋙ Functor.sectionsFunctor Cᵒᵖ).map f))
      x

Tactic:
exact ΓObjEquivSections_naturality J f x

Premises used: CategoryTheory.Sheaf.ΓObjEquivSections_naturality
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type w)
inst_2 : HasGlobalSectionsFunctor J (Type w)
X : Type w
inst_3 : Unique X
F G : Sheaf J (Type w)
f : F ⟶ G
x : Functor.obj (Γ J (Type w)) F
⊢ Eq (α := Functor.obj (constantSheaf J (Type w)) X ⟶ G)
    ((ΓObjEquivHom J G X : (a : (Γ J (Type w)).obj G) → (constantSheaf J (Type w)).obj X ⟶ G)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Γ J (Type w)) f) :
            (a : (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj F)) → (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj G))
          x) :
      Functor.obj (constantSheaf J (Type w)) X ⟶ G)
    ((ΓObjEquivHom J F X : (a : (Γ J (Type w)).obj F) → (constantSheaf J (Type w)).obj X ⟶ F) x ≫ f :
      Functor.obj (constantSheaf J (Type w)) X ⟶ G)

Tactic:
(constantSheafΓAdj J (Type w)).homEquiv_naturality_right_symm
    (↾(uniqueElim x)) f

Premises used: Eq.mpr, TypeCat.ofHom, TypeCat.Fun.comp, uniqueElim, CategoryTheory.constantSheafΓAdj, CategoryTheory.Adjunction.homEquiv_naturality_right_symm
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type w)
inst_2 : HasGlobalSectionsFunctor J (Type w)
X : Type w
inst_3 : Unique X
F G : Sheaf J (Type w)
f : F ⟶ G
x : Functor.obj (constantSheaf J (Type w)) X ⟶ F
⊢ Eq.{w + 1} (α := Functor.obj (Γ J (Type w)) G)
    ((Equiv.symm (ΓObjEquivHom J G X) : (a : (constantSheaf J (Type w)).obj X ⟶ G) → (Γ J (Type w)).obj G) (x ≫ f) :
      Functor.obj (Γ J (Type w)) G)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Γ J (Type w)) f) :
          (a : (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj F)) → (fun (X : Type w) ↦ X) ((Γ J (Type w)).obj G))
        ((Equiv.symm (ΓObjEquivHom J F X) : (a : (constantSheaf J (Type w)).obj X ⟶ F) → (Γ J (Type w)).obj F) x :
          Functor.obj (Γ J (Type w)) F) :
      (fun (X : Type w) ↦ X) (Functor.obj (Γ J (Type w)) G))

Tactic:
ConcreteCategory.congr_hom ((constantSheafΓAdj J _).homEquiv_naturality_right x f) default

Premises used: Inhabited.default, CategoryTheory.constantSheafΓAdj, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Adjunction.homEquiv_naturality_right
-- Module: Mathlib.CategoryTheory.Sites.GlobalSections
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v, v₂, u, u₂} J A
X : Type (max u v)
inst_3 : Unique X
X_1 Y : Sheaf J (Type (max u v))
f : X_1 ⟶ Y
h :
  ∀ (x : Functor.obj (Γ J (Type (max u v))) X_1),
    Eq (α := Functor.obj (Functor.obj coyoneda (op (Functor.obj (constantSheaf J (Type (max u v))) X))) Y)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Γ J (Type (max u v))) f ≫
            Iso.hom
              ((fun (F : Sheaf J (Type (max u v))) ↦
                  (Equiv.toIso (ΓObjEquivHom J F X) :
                    Functor.obj (Γ J (Type (max u v))) F ≅ Functor.obj (constantSheaf J (Type (max u v))) X ⟶ F))
                Y)))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (F : Sheaf J (Type (max u v))) ↦
                  (Equiv.toIso (ΓObjEquivHom J F X) :
                    Functor.obj (Γ J (Type (max u v))) F ≅ Functor.obj (constantSheaf J (Type (max u v))) X ⟶ F))
                X_1) ≫
            Functor.map (Functor.obj coyoneda (op (Functor.obj (constantSheaf J (Type (max u v))) X))) f))
        x)
⊢ Eq (α :=
    Functor.obj (Γ J (Type (max u v))) X_1 ⟶
      Functor.obj (Functor.obj coyoneda (op (Functor.obj (constantSheaf J (Type (max u v))) X))) Y)
    (Functor.map (Γ J (Type (max u v))) f ≫
      Iso.hom
        ((fun (F : Sheaf J (Type (max u v))) ↦
            (Equiv.toIso (ΓObjEquivHom J F X) :
              Functor.obj (Γ J (Type (max u v))) F ≅ Functor.obj (constantSheaf J (Type (max u v))) X ⟶ F))
          Y))
    (Iso.hom
        ((fun (F : Sheaf J (Type (max u v))) ↦
            (Equiv.toIso (ΓObjEquivHom J F X) :
              Functor.obj (Γ J (Type (max u v))) F ≅ Functor.obj (constantSheaf J (Type (max u v))) X ⟶ F))
          X_1) ≫
      Functor.map (Functor.obj coyoneda (op (Functor.obj (constantSheaf J (Type (max u v))) X))) f)

Tactic:
ext x