awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
D : Type u_3
E : Type u_4
inst_3 : Category.{v_3, u_3} D
inst_4 : Category.{v_4, u_4} E
F : Functor.{v_3, v_4, u_3, u_4} D E
inst_5 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_6 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_8 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_3, u, u_3} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst_11 : (X Y : D) → FunLike.{u_5 + 1, u_6 + 1, u_6 + 1} (FD X Y) (CD X) (CD Y)
inst_12 : (X Y : E) → FunLike.{u_7 + 1, u_8 + 1, u_8 + 1} (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory.{u_6, v_3, u_3, u_5} D FD (CC := CD)
instCCE : ConcreteCategory.{u_8, v_4, u_4, u_7} E FE (CC := CE)
inst_13 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_14 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E (FC := FE) (CC := CE))
inst_15 : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_16 : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E (FC := FE) (CC := CE))
inst_17 : ReflectsIsomorphisms.{v_3, u_3, u_6, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_18 : ReflectsIsomorphisms.{v_4, u_4, u_8, u_8 + 1} (forget E (FC := FE) (CC := CE))
P : Functor.{v, v_3, u, u_3} Cᵒᵖ D
⊢ IsIso (X :=
    obj (sheafToPresheaf J E) ((obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)).obj P)) (Y :=
    obj (sheafToPresheaf J E) ((plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F).obj P))
    (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
D : Type u_3
E : Type u_4
inst_3 : Category.{v_3, u_3} D
inst_4 : Category.{v_4, u_4} E
F : Functor.{v_3, v_4, u_3, u_4} D E
inst_5 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_6 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_8 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_3, u, u_3} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst_11 : (X Y : D) → FunLike.{u_5 + 1, u_6 + 1, u_6 + 1} (FD X Y) (CD X) (CD Y)
inst_12 : (X Y : E) → FunLike.{u_7 + 1, u_8 + 1, u_8 + 1} (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory.{u_6, v_3, u_3, u_5} D FD (CC := CD)
instCCE : ConcreteCategory.{u_8, v_4, u_4, u_7} E FE (CC := CE)
inst_13 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_14 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E (FC := FE) (CC := CE))
inst_15 : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_16 : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E (FC := FE) (CC := CE))
inst_17 : ReflectsIsomorphisms.{v_3, u_3, u_6, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_18 : ReflectsIsomorphisms.{v_4, u_4, u_8, u_8 + 1} (forget E (FC := FE) (CC := CE))
⊢ IsIso (X := obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)) (Y :=
    plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F)
    (sheafComposeNatTrans J F (plusPlusAdjunction J D (FD := FD) (CD := CD))
      (plusPlusAdjunction J E (FD := FE) (CD := CE)))

Tactic:
NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
D : Type u_3
E : Type u_4
inst_3 : Category.{v_3, u_3} D
inst_4 : Category.{v_4, u_4} E
F : Functor.{v_3, v_4, u_3, u_4} D E
inst_5 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_6 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_8 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_3, u, u_3} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst_11 : (X Y : D) → FunLike.{u_5 + 1, u_6 + 1, u_6 + 1} (FD X Y) (CD X) (CD Y)
inst_12 : (X Y : E) → FunLike.{u_7 + 1, u_8 + 1, u_8 + 1} (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory.{u_6, v_3, u_3, u_5} D FD (CC := CD)
instCCE : ConcreteCategory.{u_8, v_4, u_4, u_7} E FE (CC := CE)
inst_13 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_14 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E (FC := FE) (CC := CE))
inst_15 : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_16 : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E (FC := FE) (CC := CE))
inst_17 : ReflectsIsomorphisms.{v_3, u_3, u_6, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_18 : ReflectsIsomorphisms.{v_4, u_4, u_8, u_8 + 1} (forget E (FC := FE) (CC := CE))
rw :
  IsIso (X := obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)) (Y :=
    plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F)
    (sheafComposeNatTrans J F (plusPlusAdjunction J D (FD := FD) (CD := CD))
      (plusPlusAdjunction J E (FD := FE) (CD := CE)))
⊢ J.PreservesSheafification F

Tactic:
rw [preservesSheafification_iff_of_adjunctions_of_hasSheafCompose _ _
    (plusPlusAdjunction J D) (plusPlusAdjunction J E)]

Premises used: CategoryTheory.plusPlusAdjunction, CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
D : Type u_3
E : Type u_4
inst_3 : Category.{v_3, u_3} D
inst_4 : Category.{v_4, u_4} E
F : Functor.{v_3, v_4, u_3, u_4} D E
inst_5 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_6 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_8 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_3, u, u_3} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst_11 : (X Y : D) → FunLike.{u_5 + 1, u_6 + 1, u_6 + 1} (FD X Y) (CD X) (CD Y)
inst_12 : (X Y : E) → FunLike.{u_7 + 1, u_8 + 1, u_8 + 1} (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory.{u_6, v_3, u_3, u_5} D FD (CC := CD)
instCCE : ConcreteCategory.{u_8, v_4, u_4, u_7} E FE (CC := CE)
inst_13 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_14 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E (FC := FE) (CC := CE))
inst_15 : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_16 : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E (FC := FE) (CC := CE))
inst_17 : ReflectsIsomorphisms.{v_3, u_3, u_6, u_6 + 1} (forget D (FC := FD) (CC := CD))
inst_18 : ReflectsIsomorphisms.{v_4, u_4, u_8, u_8 + 1} (forget E (FC := FE) (CC := CE))
⊢ IsIso (X := obj (whiskeringRight Cᵒᵖ D E) F ⋙ plusPlusSheaf J E (FD := FE) (CD := CE)) (Y :=
    plusPlusSheaf J D (FD := FD) (CD := CD) ⋙ sheafCompose J F)
    (sheafComposeNatTrans J F (plusPlusAdjunction J D (FD := FD) (CD := CD))
      (plusPlusAdjunction J E (FD := FE) (CD := CE)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.PreservesSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u_1
B : Type u_2
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} B
F : Functor.{v_1, v_2, u_1, u_2} A B
D : Type u_3
inst_3 : Category.{max v u, u_3} D
FD : D → D → Type u_4
CD : D → Type (max v u)
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory D FD (CC := CD)
inst_6 : PreservesLimits (forget D (FC := FD) (CC := CD))
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_9 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_10 : ReflectsIsomorphisms (forget D (FC := FD) (CC := CD))
⊢ J.PreservesSheafification (forget D (FC := FD) (CC := CD))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K₁ K₂ : Pretopology.{v, u} C
⊢ K₁ ≤ K₂ ↔ K₁.coverings ≤ K₂.coverings

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
g : Y ⟶ X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ R ∈ K.coverings Y, R ≤ S.arrows}
    (Sieve.pullback g S)

Tactic:
⟨_, K.pullbacks g _ hR, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, CategoryTheory.Pretopology.pullbacks
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
g : Y ⟶ X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
refine : pullbackArrows g R ≤ (Sieve.pullback g S).arrows
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ R ∈ K.coverings Y, R ≤ S.arrows}
    (Sieve.pullback g S)

Tactic:
refine ⟨_, K.pullbacks g _ hR, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
g : Y ⟶ X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
rw : Sieve.pullback g (Sieve.generate R) ≤ Sieve.pullback g S
⊢ pullbackArrows g R ≤ (Sieve.pullback g S).arrows

Tactic:
rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]

Premises used: CategoryTheory.Sieve.pullbackArrows_comm, CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
g : Y ⟶ X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
a : Sieve.generate R ≤ S
⊢ Sieve.pullback g (Sieve.generate R) ≤ Sieve.pullback g S

Tactic:
apply Sieve.pullback_monotone

Premises used: CategoryTheory.Sieve.pullback_monotone
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
g : Y ⟶ X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
a a₁ a₂ a₃ : R ≤ S.arrows
⊢ Sieve.generate R ≤ S

Tactic:
rwa [Sieve.giGenerate.gc]

Premises used: CategoryTheory.Sieve.giGenerate, GaloisInsertion.gc
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X : C
S : Sieve.{v, u} X
R' : Presieve.{v, u} X
hR' : R' ∈ K.coverings X
RS : R' ≤ S.arrows
R : Sieve.{v, u} X
t :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ R ∈ K.coverings Y, R ≤ S.arrows}
        (Sieve.pullback f R)
choose :
  ∀ (t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve.{v, u} Y)
    (t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ K.coverings Y)
    (t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows),
    Membership.mem (γ := Set (Sieve.{v, u} X)) {S : Sieve.{v, u} X | ∃ R ∈ K.coverings X, R ≤ S.arrows} R
⊢ Membership.mem (γ := Set (Sieve.{v, u} X)) {S : Sieve.{v, u} X | ∃ R ∈ K.coverings X, R ≤ S.arrows} R

Tactic:
choose t₁ t₂ t₃ using t
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X : C
S : Sieve.{v, u} X
R' : Presieve.{v, u} X
hR' : R' ∈ K.coverings X
RS : R' ≤ S.arrows
R : Sieve.{v, u} X
t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve.{v, u} Y
t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ K.coverings Y
t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows
⊢ Membership.mem (γ := Set (Sieve.{v, u} X)) {S : Sieve.{v, u} X | ∃ R ∈ K.coverings X, R ≤ S.arrows} R

Tactic:
⟨_, K.transitive _ _ hR' fun _ f hf => t₂ (RS _ _ hf), ?_⟩

Premises used: Set.Mem, CategoryTheory.Pretopology.transitive, setOf, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X : C
S : Sieve.{v, u} X
R' : Presieve.{v, u} X
hR' : R' ∈ K.coverings X
RS : R' ≤ S.arrows
R : Sieve.{v, u} X
t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve.{v, u} Y
t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ K.coverings Y
t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows
refine : (R'.bind fun (x : C) (f : x ⟶ X) (hf : R' f) ↦ t₁ ⋯) ≤ R.arrows
⊢ Membership.mem (γ := Set (Sieve.{v, u} X)) {S : Sieve.{v, u} X | ∃ R ∈ K.coverings X, R ≤ S.arrows} R

Tactic:
refine ⟨_, K.transitive _ _ hR' fun _ f hf => t₂ (RS _ _ hf), ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X : C
S : Sieve.{v, u} X
R' : Presieve.{v, u} X
hR' : R' ∈ K.coverings X
RS : R' ≤ S.arrows
R : Sieve.{v, u} X
t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve.{v, u} Y
t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ K.coverings Y
t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hg : R' f
hf : t₁ ⋯ g
⊢ R.arrows (g ≫ f)

Tactic:
apply t₃ (RS _ _ hg) _ _ hf
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
X : C
S : Sieve.{v, u} X
⊢ S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X ↔ ∃ R ∈ K.coverings X, R ≤ S.arrows

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : Y ⟶ X
i : IsIso f
⊢ Sieve.generate (Presieve.singleton f) = ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : Y ⟶ X
R : Presieve.{v, u} X
hR :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} R
⊢ Membership.mem (γ := Set (Presieve.{v, u} Y))
    {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (pullbackArrows f R)

Tactic:
simpa [Sieve.pullbackArrows_comm] using J.pullback_stable f hR

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Sieve.pullbackArrows_comm
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
h :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    (Sieve.generate S).arrows f → Sieve.pullback f (Sieve.generate (S.bind Ti)) ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} (S.bind Ti)

Tactic:
apply J.transitive hS

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
h : Sieve.pullback g (Sieve.pullback f (Sieve.generate (S.bind Ti))) ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ Sieve.pullback (g ≫ f) (Sieve.generate (S.bind Ti)) ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
rw [Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
h : Sieve.pullback f (Sieve.generate (S.bind Ti)) ∈ (J : (a : C) → Set (Sieve a)) Z
⊢ Sieve.pullback g (Sieve.pullback f (Sieve.generate (S.bind Ti))) ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
apply J.pullback_stable g

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
apply : Sieve.generate (Ti f hf) ≤ Sieve.pullback f (Sieve.generate (S.bind Ti))
⊢ Sieve.pullback f (Sieve.generate (S.bind Ti)) ∈ (J : (a : C) → Set (Sieve a)) Z

Tactic:
apply J.superset_covering _ (hTi _ hf)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
Y_1 Z : C
g_1 : Y_1 ⟶ Z
f : Z ⟶ X
hf : S f
Y W : C
h : Y ⟶ W
g : W ⟶ Z
hg : Ti f hf g
⊢ h ≫ g ≫ f = (h ≫ g) ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
Y_1 Z : C
g_1 : Y_1 ⟶ Z
f : Z ⟶ X
hf : S f
Y W : C
h : Y ⟶ W
g : W ⟶ Z
hg : Ti f hf g
⊢ (Sieve.pullback f (Sieve.generate (S.bind Ti))).arrows (h ≫ g)

Tactic:
exact ⟨_, h, _, ⟨_, _, _, hf, hg, rfl⟩, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
J : GrothendieckTopology.{v, u} C
mp : K.toGrothendieck ≤ J → K ≤ J.toPretopology
mpr : K ≤ J.toPretopology → K.toGrothendieck ≤ J
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toPretopology

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
J : GrothendieckTopology.{v, u} C
h : K.toGrothendieck ≤ J
X : C
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
⊢ R ∈ (toPrecoverage J.toPretopology).coverings X

Tactic:
h _ ⟨_, hR, Sieve.le_generate R⟩

Premises used: Set.Mem, setOf, CategoryTheory.Sieve.le_generate, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
J : GrothendieckTopology.{v, u} C
h : K.toGrothendieck ≤ J
X : C
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
⊢ R ∈ (toPrecoverage J.toPretopology).coverings X

Tactic:
exact h _ ⟨_, hR, Sieve.le_generate R⟩

Premises used: CategoryTheory.Sieve.le_generate, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
J : GrothendieckTopology.{v, u} C
h : K ≤ J.toPretopology
X : C
S : Sieve.{v, u} X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
apply : Sieve.generate R ≤ S
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
apply J.superset_covering _ (h _ hR)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
J : GrothendieckTopology.{v, u} C
h : K ≤ J.toPretopology
X : C
S : Sieve.{v, u} X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
rwa rwa₁ rwa₂ rwa₃ : R ≤ S.arrows
⊢ Sieve.generate R ≤ S

Tactic:
rwa [Sieve.giGenerate.gc]

Premises used: CategoryTheory.Sieve.giGenerate, GaloisInsertion.gc
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
t : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
⊢ S ∈ (Pretopology.toPrecoverage t.toPretopology).coverings X ↔ Sieve.generate S ∈ (t : (a : C) → Set (Sieve a)) X

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf