awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
x : unop (op X)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x : P.obj (op Z)))
          Y₁ f₁ hf₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x : P.obj (op Z)))
          Y₂ f₂ hf₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
(ConcreteCategory.congr_hom (hz g₁ g₂ hf₁ hf₂ h)) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
x : unop (op X)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x : P.obj (op Z)))
          Y₁ f₁ hf₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x : P.obj (op Z)))
          Y₂ f₂ hf₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
exact (ConcreteCategory.congr_hom (hz g₁ g₂ hf₁ hf₂ h)) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
Z : C
f : Z ⟶ Y
hf : S.arrows f
mpr :
  ∀ (x : unop (op X)),
    Eq (α := P.obj (op Z))
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda (op X)).map f.op) :
                  (a : (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Y))) →
                    (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Z)))
                (↾fun (x : unop (op X)) ↦
                  ⋯.amalgamate (R := S.arrows)
                    (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                    ⋯)) :
            (a : unop (op X)) → P.obj (op Z))
          x :
        P.obj (op Z))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x : P.obj (op Z))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda (op X)).map f.op) :
        (a : (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Y))) →
          (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Z)))
      (↾fun (x : unop (op X)) ↦
        ⋯.amalgamate (R := S.arrows)
          (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
          ⋯) =
    z f hf

Tactic:
apply ConcreteCategory.hom_ext

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
Z : C
f : Z ⟶ Y
hf : S.arrows f
x : unop (op X)
mpr :
  Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) : (a : P.obj (op Y)) → P.obj (op Z))
        (⋯.amalgamate (R := S.arrows)
          (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : X) → P.obj (op Z)) x)
          ⋯) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : X) → P.obj (op Z)) x : P.obj (op Z))
⊢ Eq (α := P.obj (op Z))
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda (op X)).map f.op) :
                (a : (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Y))) →
                  (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Z)))
              (↾fun (x : unop (op X)) ↦
                ⋯.amalgamate (R := S.arrows)
                  (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                  ⋯)) :
          (a : unop (op X)) → P.obj (op Z))
        x :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x : P.obj (op Z))

Tactic:
simp only [Functor.comp_obj, Functor.flip_obj_obj, yoneda_obj_obj, Functor.comp_map,
        Functor.flip_obj_map, yoneda_map_app, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
        comp_apply]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.yoneda_map_app, TypeCat.Fun.coe_mk, CategoryTheory.yoneda_obj_obj, CategoryTheory.comp_apply, CategoryTheory.Functor.flip_obj_map, CategoryTheory.Functor.flip_obj_obj, CategoryTheory.ConcreteCategory.hom_ofHom, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
Z : C
f : Z ⟶ Y
hf : S.arrows f
x : unop (op X)
⊢ Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) : (a : P.obj (op Y)) → P.obj (op Z))
        (⋯.amalgamate (R := S.arrows)
          (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : X) → P.obj (op Z)) x)
          ⋯) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : X) → P.obj (op Z)) x : P.obj (op Z))

Tactic:
apply Presieve.IsSheafFor.valid_glue

Premises used: CategoryTheory.Presieve.IsSheafFor.valid_glue
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
y : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)
hy : z.IsAmalgamation (R := S.arrows) y
mpr :
  ∀ (x : unop (op X)),
    Eq (α := P.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) y : (a : unop (op X)) → P.obj (op Y)) x : P.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : unop (op X)) ↦
                ⋯.amalgamate (R := S.arrows)
                  (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                  ⋯) :
            (a : unop (op X)) → P.obj (op Y))
          x :
        P.obj (op Y))
⊢ y =
    ↾fun (x : unop (op X)) ↦
      ⋯.amalgamate (R := S.arrows)
        (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
        ⋯

Tactic:
apply ConcreteCategory.hom_ext

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
y : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)
hy : z.IsAmalgamation (R := S.arrows) y
x : unop (op X)
mpr :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    S.arrows f →
      Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) y : (a : unop (op X)) → P.obj (op Y)) x : P.obj (op Y)) :
          (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (↾fun (x : unop (op X)) ↦
                      ⋯.amalgamate (R := S.arrows)
                        (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                          (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                        ⋯) :
                  (a : unop (op X)) → P.obj (op Y))
                x :
              P.obj (op Y)) :
          (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
⊢ Eq (α := P.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) y : (a : unop (op X)) → P.obj (op Y)) x : P.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : unop (op X)) ↦
              ⋯.amalgamate (R := S.arrows)
                (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                ⋯) :
          (a : unop (op X)) → P.obj (op Y))
        x :
      P.obj (op Y))

Tactic:
apply (hP S hS).isSeparatedFor.ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
y : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)
hy : z.IsAmalgamation (R := S.arrows) y
x : unop (op X)
Y' : C
f : Y' ⟶ Y
hf : S.arrows f
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Y')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) y : (a : unop (op X)) → P.obj (op Y)) x : P.obj (op Y)) :
      (fun (X : Type w) ↦ X) (P.obj (op Y')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Y')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾fun (x : unop (op X)) ↦
                  ⋯.amalgamate (R := S.arrows)
                    (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                    ⋯) :
              (a : unop (op X)) → P.obj (op Y))
            x :
          P.obj (op Y)) :
      (fun (X : Type w) ↦ X) (P.obj (op Y')))

Tactic:
simp [Presieve.IsSheafFor.valid_glue _ _ _ hf, ← hy _ hf]

Premises used: CategoryTheory.Presieve.IsSheafFor.valid_glue
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
A_1 : Type u₂
inst_1 : Category.{v₂, u₂} A_1
A : Type u₂
inst_2 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
ℱ : Sheaf.{v₁, v₂, u₁, u₂} J A
E : A
rw : Presieve.IsSheaf.{v₂, v₁, u₁} J (ℱ.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op E))
⊢ Presheaf.IsSheaf J (ℱ.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op E))

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
A_1 : Type u₂
inst_1 : Category.{v₂, u₂} A_1
A : Type u₂
inst_2 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
ℱ : Sheaf.{v₁, v₂, u₁, u₂} J A
E : A
⊢ Presieve.IsSheaf.{v₂, v₁, u₁} J (ℱ.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op E))

Tactic:
ℱ.property E

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
A_1 : Type u₂
inst_1 : Category.{v₂, u₂} A_1
A : Type u₂
inst_2 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
ℱ : Sheaf.{v₁, v₂, u₁, u₂} J A
E : A
⊢ Presieve.IsSheaf.{v₂, v₁, u₁} J (ℱ.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op E))

Tactic:
exact ℱ.property E

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : IsSheaf J P
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
rw :
  ∀ (hP : Presieve.IsSheaf J P) {X : C} (S : Sieve.{v₁, u₁} X) (hS : S ∈ (J : (a : C) → Set (Sieve a)) X),
    Presieve.IsSheafFor P S.arrows
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
rw [isSheaf_iff_isSheaf_of_type] at hP

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
hP S hS
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
exact hP S hS
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
⊢ IsSheaf ⊥ P

Tactic:
fun _ ↦ Presieve.isSheaf_bot

Premises used: CategoryTheory.Presieve.isSheaf_bot, CategoryTheory.Presheaf.IsSheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
K : GrothendieckTopology.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hle : J ≤ K
h : IsSheaf K F
⊢ IsSheaf J F

Tactic:
fun _ _ _ hS ↦ h _ _ (hle _ hS)

Premises used: CategoryTheory.Presieve.IsSheaf, CategoryTheory.Presheaf.IsSheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Sheaf.{v₁, v₂, u₁, u₂} J A
X : C
H : ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
refine : (X_1 : A) → Unique (X_1 ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X))
⊢ IsTerminal.{v₂, u₂} (F.obj (P := Presheaf.IsSheaf J).obj (op X))

Tactic:
refine @IsTerminal.ofUnique _ _ _ ?_

Premises used: CategoryTheory.Limits.IsTerminal.ofUnique
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Sheaf.{v₁, v₂, u₁, u₂} J A
X : C
H : ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
Y : A
tauto tauto₁ tauto₂ tauto₃ :
  ⦃Y_1 : C⦄ → (f : Y_1 ⟶ X) → arrows ⊥ f → (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)
⊢ Presieve.FamilyOfElements (X := X) (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)) (arrows ⊥)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Sheaf.{v₁, v₂, u₁, u₂} J A
X : C
H : ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
Y : A
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ tauto₁₁ tauto₁₂ :
  ∀ ⦃Y₁ Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : arrows ⊥ f₁) (h₂ : arrows ⊥ f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      Eq (α := (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).map g₁.op) :
              (a : (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Y₁))) →
                (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Z)))
            ((fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦
                (False.elim ⋯ : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)))
              f₁ h₁) :
          (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).map g₂.op) :
              (a : (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Y₂))) →
                (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Z)))
            ((fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦
                (False.elim ⋯ : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)))
              f₂ h₂) :
          (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Z)))
⊢ Presieve.FamilyOfElements.Compatible.{v₂, v₁, u₁} (P := F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y))
    (R := arrows ⊥) fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Sheaf.{v₁, v₂, u₁, u₂} J A
X : C
H : ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
Y : A
choose :
  (t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)) →
    (h :
        (fun (t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)) ↦
              Presieve.FamilyOfElements.IsAmalgamation (R := arrows ⊥)
                (fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯) t)
            t ∧
          ∀ (y : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)),
            (fun (t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)) ↦
                  Presieve.FamilyOfElements.IsAmalgamation (R := arrows ⊥)
                    (fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯) t)
                y →
              y = t) →
      Unique (Y ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X))
⊢ Unique (Y ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X))

Tactic:
choose t h using F.2 Y _ H (by tauto) (by tauto)

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Sheaf.{v₁, v₂, u₁, u₂} J A
X : C
H : ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
Y : A
t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)
h :
  (fun (t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)) ↦
        Presieve.FamilyOfElements.IsAmalgamation (R := arrows ⊥)
          (fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯) t)
      t ∧
    ∀ (y : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)),
      (fun (t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)) ↦
            Presieve.FamilyOfElements.IsAmalgamation (R := arrows ⊥)
              (fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯) t)
          y →
        y = t
a : Y ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X)
tauto tauto₁ tauto₂ tauto₃ :
  ∀ ⦃Y_1 : C⦄,
    Presieve.FamilyOfElements.IsAmalgamation (R := arrows ⊥)
        (fun ⦃Y_2 : C⦄ (f : Y_2 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯) t →
      (∀ (y : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)),
          (fun (t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)) ↦
                Presieve.FamilyOfElements.IsAmalgamation (R := arrows ⊥)
                  (fun ⦃Y_2 : C⦄ (f : Y_2 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯) t)
              y →
            y = t) →
        ∀ (f : Y_1 ⟶ X) (h : arrows ⊥ f),
          Eq (α :=
            (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).map f.op) :
                  (a : (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op X))) →
                    (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Y_1)))
                a :
              (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)))
            ((fun ⦃Y_2 : C⦄ (f : Y_2 ⟶ X) (a : arrows ⊥ f) ↦
                  (False.elim ⋯ : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_2)))
                f h :
              (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1))
⊢ Presieve.FamilyOfElements.IsAmalgamation.{v₂, v₁, u₁} (P :=
    F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)) (R := arrows ⊥)
    (fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯) a

Tactic:
tauto