awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
refine_1 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ Z⦄,
    (Sieve.pullback g R).arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows
refine_2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ Z⦄,
    (Sieve.pullback g S).arrows f → Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback g R).arrows

Tactic:
refine Presieve.isSheafFor_trans P (pullback g S) _ (hS Z g) ?_ ?_

Premises used: CategoryTheory.Presieve.isSheafFor_trans, CategoryTheory.Sieve.pullback
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
refine_1 : (Sieve.pullback g R).arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows
⊢ (Sieve.pullback g R).arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
h : (Sieve.pullback g R).arrows f
refine_1 : Presieve.IsSeparatedFor P (Sieve.pullback (f ≫ g) S).arrows
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows

Tactic:
rw [← pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
h : (Sieve.pullback g R).arrows f
⊢ Presieve.IsSeparatedFor P (Sieve.pullback (f ≫ g) S).arrows

Tactic:
apply (hS _ _).isSeparatedFor

Premises used: CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
⊢ Presieve.IsSheafFor P (Sieve.pullback (𝟙 Y) (Sieve.pullback (f ≫ g) R)).arrows

Tactic:
have := hR hf _ (𝟙 _)
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
this : Presieve.IsSheafFor P (Sieve.pullback (𝟙 Y) (Sieve.pullback (f ≫ g) R)).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows

Tactic:
rw [pullback_id, pullback_comp] at this

Premises used: CategoryTheory.Sieve.pullback_comp, CategoryTheory.Sieve.pullback_id
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P_1 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J : GrothendieckTopology.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows} S
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
        (Sieve.pullback f R)
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
this : Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows

Tactic:
apply this
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
Ps : Set (Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
h : P ∈ Ps
X : C
S : Sieve.{v, u} X
hS : S ∈ (finestTopology Ps : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
simpa using hS _ ⟨⟨_, _, ⟨_, h, rfl⟩, rfl⟩, rfl⟩ _ (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
Ps : Set (Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
X : C
S : Sieve.{v, u} X
H : ∀ P ∈ Ps, ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hP : P ∈ Ps
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f S).arrows

Tactic:
H P hP _
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
Ps : Set (Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
X : C
S : Sieve.{v, u} X
H : ∀ P ∈ Ps, ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hP : P ∈ Ps
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f S).arrows

Tactic:
exact H P hP _
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
Ps : Set (Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
J : GrothendieckTopology.{v, u} C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (finestTopology Ps : (a : C) → Set (Sieve a)) X

Tactic:
mem_finestTopology_of_forall_isSheafFor
    fun P hP Y f ↦ hJ P hP _ (J.pullback_stable _ hS)

Premises used: CategoryTheory.Sheaf.mem_finestTopology_of_forall_isSheafFor, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Sieve.pullback
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
Ps : Set (Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
J : GrothendieckTopology.{v, u} C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (finestTopology Ps : (a : C) → Set (Sieve a)) X

Tactic:
exact mem_finestTopology_of_forall_isSheafFor
    fun P hP Y f ↦ hJ P hP _ (J.pullback_stable _ hS)

Premises used: CategoryTheory.Sheaf.mem_finestTopology_of_forall_isSheafFor, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Sieve.pullback
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ Presieve.IsSheaf.{v, v, u} (canonicalTopology C) (Functor.obj yoneda X)

Tactic:
fun _ _ hS => sheaf_for_finestTopology _ (Set.mem_range_self _) _ hS

Premises used: CategoryTheory.Presieve.IsSheaf, Set.mem_range_self, CategoryTheory.yoneda, CategoryTheory.Sheaf.sheaf_for_finestTopology, Set.range, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
rw : Presieve.IsSheaf (canonicalTopology C) (P ⋙ uliftFunctor.{v, w})
⊢ Presieve.IsSheaf (canonicalTopology C) P

Tactic:
rw [← Presieve.isSheaf_comp_uliftFunctor_iff]

Premises used: CategoryTheory.Presieve.isSheaf_comp_uliftFunctor_iff
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
⊢ Presieve.IsSheaf (canonicalTopology C) (P ⋙ uliftFunctor.{v, w})

Tactic:
Presieve.isSheaf_iso (canonicalTopology C) (P ⋙ uliftFunctor.{v}).uliftYonedaReprXIso ?_

Premises used: CategoryTheory.Functor.uliftYonedaReprXIso, CategoryTheory.Functor.comp, CategoryTheory.uliftFunctor, CategoryTheory.Presieve.isSheaf_iso, CategoryTheory.Sheaf.canonicalTopology
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
refine : Presieve.IsSheaf (canonicalTopology C) (Functor.obj uliftYoneda.{w, v, u} (P ⋙ uliftFunctor.{v, w}).reprX)
⊢ Presieve.IsSheaf (canonicalTopology C) (P ⋙ uliftFunctor.{v, w})

Tactic:
refine Presieve.isSheaf_iso (canonicalTopology C) (P ⋙ uliftFunctor.{v}).uliftYonedaReprXIso ?_
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
rw : Presheaf.IsSheaf (canonicalTopology C) (Functor.obj uliftYoneda.{w, v, u} (P ⋙ uliftFunctor.{v, w}).reprX)
⊢ Presieve.IsSheaf (canonicalTopology C) (Functor.obj uliftYoneda.{w, v, u} (P ⋙ uliftFunctor.{v, w}).reprX)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
⊢ Presheaf.IsSheaf (canonicalTopology C) (Functor.obj uliftYoneda.{w, v, u} (P ⋙ uliftFunctor.{v, w}).reprX)

Tactic:
GrothendieckTopology.HasSheafCompose.isSheaf _ ?_

Premises used: CategoryTheory.Functor.comp, CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
refine : Presheaf.IsSheaf.{v, v, u, v + 1} (canonicalTopology C) (Functor.obj yoneda (P ⋙ uliftFunctor.{v, w}).reprX)
⊢ Presheaf.IsSheaf (canonicalTopology C) (Functor.obj uliftYoneda.{w, v, u} (P ⋙ uliftFunctor.{v, w}).reprX)

Tactic:
refine GrothendieckTopology.HasSheafCompose.isSheaf _ ?_

Premises used: CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
rw : Presieve.IsSheaf.{v, v, u} (canonicalTopology C) (Functor.obj yoneda (P ⋙ uliftFunctor.{v, w}).reprX)
⊢ Presheaf.IsSheaf.{v, v, u, v + 1} (canonicalTopology C) (Functor.obj yoneda (P ⋙ uliftFunctor.{v, w}).reprX)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
⊢ Presieve.IsSheaf.{v, v, u} (canonicalTopology C) (Functor.obj yoneda (P ⋙ uliftFunctor.{v, w}).reprX)

Tactic:
isSheaf_yoneda_obj _

Premises used: CategoryTheory.Sheaf.isSheaf_yoneda_obj
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : P.IsRepresentable
⊢ Presieve.IsSheaf.{v, v, u} (canonicalTopology C) (Functor.obj yoneda (P ⋙ uliftFunctor.{v, w}).reprX)

Tactic:
exact isSheaf_yoneda_obj _

Premises used: CategoryTheory.Sheaf.isSheaf_yoneda_obj
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
⊢ J ≤ canonicalTopology C

Tactic:
Subcanonical.le_canonical

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.le_canonical
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
h : ∀ (X : C), Presieve.IsSheaf J (Functor.obj yoneda X)
X : C
⊢ Presieve.IsSheaf J (Functor.obj yoneda X)

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_2 : P.IsRepresentable
⊢ Presieve.IsSheaf J P

Tactic:
Presieve.isSheaf_of_le _ J.le_canonical (Sheaf.isSheaf_of_isRepresentable P)

Premises used: CategoryTheory.Presieve.isSheaf_of_le, CategoryTheory.Sheaf.isSheaf_of_isRepresentable, CategoryTheory.GrothendieckTopology.le_canonical
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
J K : GrothendieckTopology.{v, u} C
h : J ≤ K
inst_1 : K.Subcanonical
x x_1 : C
x_2 : Sieve.{v, u} x_1
h_1 : x_2 ∈ (J : (a : C) → Set (Sieve a)) x_1
⊢ generate x_2.arrows ∈ (J : (a : C) → Set (Sieve a)) x_1

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J_1 J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X : C
rw : Presieve.IsSheaf J (Functor.obj CategoryTheory.yoneda X)
⊢ Presheaf.IsSheaf J (Functor.obj CategoryTheory.yoneda X)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X_1 : C
J_1 J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X : C
⊢ Presieve.IsSheaf J (Functor.obj CategoryTheory.yoneda X)

Tactic:
apply Subcanonical.isSheaf_of_isRepresentable

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
J_1 J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
⊢ J.yoneda.Full

Tactic:
(J.yonedaFullyFaithful).full

Premises used: CategoryTheory.GrothendieckTopology.yonedaFullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
J_1 J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
⊢ J.yoneda.Faithful

Tactic:
(J.yonedaFullyFaithful).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.GrothendieckTopology.yonedaFullyFaithful
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
J_1 J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
⊢ (uliftYoneda.{w, v, u} J).Full

Tactic:
(J.fullyFaithfulUliftYoneda).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.GrothendieckTopology.fullyFaithfulUliftYoneda
-- Module: Mathlib.CategoryTheory.Sites.Canonical
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
J_1 J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
⊢ (uliftYoneda.{w, v, u} J).Faithful

Tactic:
(J.fullyFaithfulUliftYoneda).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.GrothendieckTopology.fullyFaithfulUliftYoneda
-- Module: Mathlib.CategoryTheory.Sites.CartesianMonoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
X Y : Sheaf.{v₁, v₂, u₁, u₂} J A
apply :
  IsLimit
    ((Cone.postcompose (pairComp X Y (sheafToPresheaf J A)).inv).obj
      (BinaryFan.mk (P :=
        tensorObj (𝒞 := Functor.category) (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))
        (fst (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))
        (snd (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))))
⊢ Presheaf.IsSheaf J
    (tensorObj (𝒞 := Functor.category) (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))

Tactic:
apply isSheaf_of_isLimit (E := (Cone.postcompose (pairComp X Y (sheafToPresheaf J A)).inv).obj
    (BinaryFan.mk (fst X.obj Y.obj) (snd _ _)))

Premises used: CategoryTheory.Limits.pairComp, CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Sheaf.isSheaf_of_isLimit, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.SemiCartesianMonoidalCategory.fst, CategoryTheory.sheafToPresheaf, CategoryTheory.Limits.Cone.postcompose
-- Module: Mathlib.CategoryTheory.Sites.CartesianMonoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
X Y : Sheaf.{v₁, v₂, u₁, u₂} J A
⊢ IsLimit
    ((Cone.postcompose (pairComp X Y (sheafToPresheaf J A)).inv).obj
      (BinaryFan.mk (P :=
        tensorObj (𝒞 := Functor.category) (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))
        (fst (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))
        (snd (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))))

Tactic:
exact (IsLimit.postcomposeInvEquiv _ _).invFun
    (tensorProductIsBinaryProduct X.obj Y.obj)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Sites.CartesianMonoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
apply :
  IsLimit (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (F := Functor.empty (Sheaf.{v₁, v₂, u₁, u₂} J A) ⋙ sheafToPresheaf J A)
    (Functor.obj
      (Cone.postcompose
        (Iso.inv (Functor.uniqueFromEmpty (Functor.empty (Sheaf.{v₁, v₂, u₁, u₂} J A) ⋙ sheafToPresheaf J A))))
      (asEmptyCone ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A)) (𝒞 := Functor.category))))
apply₁ : Discrete PEmpty.{1} ⥤ Sheaf.{v₁, v₂, u₁, u₂} J A
⊢ Presheaf.IsSheaf.{v₁, v₂, u₁, u₂} (A := A) J ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A)) (𝒞 := Functor.category))

Tactic:
apply isSheaf_of_isLimit (E := (Cone.postcompose (Functor.uniqueFromEmpty _).inv).obj
    (asEmptyCone (𝟙_ _)))

Premises used: CategoryTheory.Sheaf.isSheaf_of_isLimit, CategoryTheory.Functor.uniqueFromEmpty, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.Limits.asEmptyCone, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cone.postcompose
-- Module: Mathlib.CategoryTheory.Sites.CartesianMonoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
⊢ IsLimit (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (F := Functor.empty (Sheaf.{v₁, v₂, u₁, u₂} J A) ⋙ sheafToPresheaf J A)
    (Functor.obj
      (Cone.postcompose
        (Iso.inv (Functor.uniqueFromEmpty (Functor.empty (Sheaf.{v₁, v₂, u₁, u₂} J A) ⋙ sheafToPresheaf J A))))
      (asEmptyCone ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A)) (𝒞 := Functor.category))))

Tactic:
exact (IsLimit.postcomposeInvEquiv _ _).invFun isTerminalTensorUnit

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Sites.CartesianMonoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
⊢ Discrete PEmpty.{1} ⥤ Sheaf.{v₁, v₂, u₁, u₂} J A

Tactic:
exact .empty _
-- Module: Mathlib.CategoryTheory.Sites.CartesianMonoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
X Y : Sheaf.{v₁, v₂, u₁, u₂} J A
⊢ Eq (α :=
    (tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf J)) X Y).obj (P := Presheaf.IsSheaf J) ⟶
      X.obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (fst X Y)) (fst (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.CartesianMonoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
X Y : Sheaf.{v₁, v₂, u₁, u₂} J A
⊢ Eq (α :=
    (tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf J)) X Y).obj (P := Presheaf.IsSheaf J) ⟶
      Y.obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (snd X Y)) (snd (X.obj (P := Presheaf.IsSheaf J)) (Y.obj (P := Presheaf.IsSheaf J)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.CartesianMonoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
X Y W : Sheaf.{v₁, v₂, u₁, u₂} J A
f : W ⟶ X
g : W ⟶ Y
⊢ Eq (α :=
    W.obj (P := Presheaf.IsSheaf J) ⟶
      (tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf J)) X Y).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (lift f g)) (lift f.hom g.hom)

Tactic:
rfl

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, rfl
-- Module: Mathlib.CategoryTheory.Sites.CartesianMonoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
inst_2 : CartesianMonoidalCategory.{v₂, u₂} A
X W : Sheaf.{v₁, v₂, u₁, u₂} J A
f : W ⟶ X
⊢ Eq (α :=
    (tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf J)) X W).obj (P := Presheaf.IsSheaf J) ⟶
      (tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf J)) X X).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (X ◁ f)) (X.obj (P := Presheaf.IsSheaf J) ◁ f.hom)

Tactic:
rfl

Premises used: rfl