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
X : Type (max u v)
inst_3 : Unique X
X_1 Y : Sheaf J (Type (max u v))
f : X_1 ⟶ Y
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)

Tactic:
ΓObjEquivHom_naturality J X f x

Premises used: CategoryTheory.Sheaf.ΓObjEquivHom_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 : Type (max u v)
inst_3 : Unique X
X_1 Y : Sheaf J (Type (max u v))
f : X_1 ⟶ Y
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)

Tactic:
exact ΓObjEquivHom_naturality J X f x

Premises used: CategoryTheory.Sheaf.ΓObjEquivHom_naturality
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h :
  Eq (α := (a : C) → Set (Sieve.{v, u} a)) ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X) J₁)
    ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X) J₂)
mk :
  ∀ (sieves : (X : C) → Set (Sieve.{v, u} X)) (top_mem' : ∀ (X : C), ⊤ ∈ sieves X)
    (pullback_stable' : ∀ ⦃X Y : C⦄ ⦃S : Sieve.{v, u} X⦄ (f : Y ⟶ X), S ∈ sieves X → Sieve.pullback f S ∈ sieves Y)
    (transitive' :
      ∀ ⦃X : C⦄ ⦃S : Sieve.{v, u} X⦄,
        S ∈ sieves X →
          ∀ (R : Sieve.{v, u} X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X)
    (h :
      Eq (α := (a : C) → Set (Sieve.{v, u} a))
        ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
          { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' })
        ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X) J₂)),
    { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' :
        GrothendieckTopology.{v, u} C } =
      J₂
⊢ J₁ = J₂

Tactic:
cases J₁
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J₂ : GrothendieckTopology.{v, u} C
sieves : (X : C) → Set (Sieve.{v, u} X)
top_mem' : ∀ (X : C), ⊤ ∈ sieves X
pullback_stable' : ∀ ⦃X Y : C⦄ ⦃S : Sieve.{v, u} X⦄ (f : Y ⟶ X), S ∈ sieves X → Sieve.pullback f S ∈ sieves Y
transitive' :
  ∀ ⦃X : C⦄ ⦃S : Sieve.{v, u} X⦄,
    S ∈ sieves X →
      ∀ (R : Sieve.{v, u} X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X
h :
  Eq (α := (a : C) → Set (Sieve.{v, u} a))
    ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
      { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' })
    ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X) J₂)
mk :
  ∀ (sieves_1 : (X : C) → Set (Sieve.{v, u} X)) (top_mem'_1 : ∀ (X : C), ⊤ ∈ sieves_1 X)
    (pullback_stable'_1 :
      ∀ ⦃X Y : C⦄ ⦃S : Sieve.{v, u} X⦄ (f : Y ⟶ X), S ∈ sieves_1 X → Sieve.pullback f S ∈ sieves_1 Y)
    (transitive'_1 :
      ∀ ⦃X : C⦄ ⦃S : Sieve.{v, u} X⦄,
        S ∈ sieves_1 X →
          ∀ (R : Sieve.{v, u} X),
            (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves_1 Y) → R ∈ sieves_1 X)
    (h :
      Eq (α := (a : C) → Set (Sieve.{v, u} a))
        ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
          { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' })
        ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
          { sieves := sieves_1, top_mem' := top_mem'_1, pullback_stable' := pullback_stable'_1,
            transitive' := transitive'_1 })),
    { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' :
        GrothendieckTopology.{v, u} C } =
      { sieves := sieves_1, top_mem' := top_mem'_1, pullback_stable' := pullback_stable'_1,
        transitive' := transitive'_1 }
⊢ { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' :
      GrothendieckTopology.{v, u} C } =
    J₂

Tactic:
cases J₂
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
sieves : (X : C) → Set (Sieve.{v, u} X)
top_mem' : ∀ (X : C), ⊤ ∈ sieves X
pullback_stable' : ∀ ⦃X Y : C⦄ ⦃S : Sieve.{v, u} X⦄ (f : Y ⟶ X), S ∈ sieves X → Sieve.pullback f S ∈ sieves Y
transitive' :
  ∀ ⦃X : C⦄ ⦃S : Sieve.{v, u} X⦄,
    S ∈ sieves X →
      ∀ (R : Sieve.{v, u} X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X
sieves_1 : (X : C) → Set (Sieve.{v, u} X)
top_mem'_1 : ∀ (X : C), ⊤ ∈ sieves_1 X
pullback_stable'_1 : ∀ ⦃X Y : C⦄ ⦃S : Sieve.{v, u} X⦄ (f : Y ⟶ X), S ∈ sieves_1 X → Sieve.pullback f S ∈ sieves_1 Y
transitive'_1 :
  ∀ ⦃X : C⦄ ⦃S : Sieve.{v, u} X⦄,
    S ∈ sieves_1 X →
      ∀ (R : Sieve.{v, u} X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves_1 Y) → R ∈ sieves_1 X
h :
  Eq (α := (a : C) → Set (Sieve.{v, u} a))
    ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
      { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' })
    ((fun (J : GrothendieckTopology.{v, u} C) (X : C) ↦ J.sieves X)
      { sieves := sieves_1, top_mem' := top_mem'_1, pullback_stable' := pullback_stable'_1,
        transitive' := transitive'_1 })
⊢ { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' :
      GrothendieckTopology.{v, u} C } =
    { sieves := sieves_1, top_mem' := top_mem'_1, pullback_stable' := pullback_stable'_1, transitive' := transitive'_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : (⇑J₁ : (a : C) → Set (Sieve a)) = (⇑J₂ : (a : C) → Set (Sieve a))
⊢ J₁ = J₂

Tactic:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ S ∈ J.sieves X ↔ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
⊢ ⊤ ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.top_mem' X

Premises used: Set.Mem, CategoryTheory.GrothendieckTopology.top_mem'
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
J.pullback_stable' f hS

Premises used: Set.Mem, CategoryTheory.GrothendieckTopology.pullback_stable'
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
⊢ Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X ↔ S ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
⟨fun H ↦ ?_, J.pullback_stable i⟩

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
refine : ∀ (H : Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X), S ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X ↔ S ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
refine ⟨fun H ↦ ?_, J.pullback_stable i⟩
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
H : Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.pullback (inv i) (Sieve.pullback i S) ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
J.pullback_stable (inv i) H

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
H : Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X
h : S = Sieve.pullback (inv i) (Sieve.pullback i S)
⊢ S ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
convert! J.pullback_stable (inv i) H

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
i : X ⟶ Y
inst_1 : IsIso i
S : Sieve.{v, u} Y
H : Sieve.pullback i S ∈ (J : (a : C) → Set (Sieve a)) X
h : S = Sieve.pullback (inv i ≫ i) S
h₁ : S = Sieve.pullback (𝟙 Y) S
h₂ h₃ : S = S
⊢ S = Sieve.pullback (inv i) (Sieve.pullback i S)

Tactic:
rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Sieve.pullback_comp, CategoryTheory.Sieve.pullback_id
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
R : Sieve.{v, u} X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ R ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.transitive' hS R h

Premises used: CategoryTheory.GrothendieckTopology.transitive', Set.Mem
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ S = ⊤ → S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
fun h => h.symm ▸ J.top_mem X

Premises used: CategoryTheory.GrothendieckTopology.top_mem, Eq.rec, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
s : (X : C) → Set (Sieve.{v, u} X)
h : J.sieves = s
⊢ (J.copy s h).sieves = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
s : (X : C) → Set (Sieve.{v, u} X)
h : J.sieves = s
⊢ (⇑(J.copy s h) : (a : C) → Set (Sieve a)) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
s : (X : C) → Set (Sieve.{v, u} X)
h : J.sieves = s
⊢ J.copy s h = J

Tactic:
GrothendieckTopology.ext h.symm

Premises used: CategoryTheory.GrothendieckTopology.ext, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
Hss : S ≤ R
sjx : S ∈ (J : (a : C) → Set (Sieve a)) X
apply : ∀ (Y : C) (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f R ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ R ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
apply J.transitive sjx R fun Y f hf => _

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
Hss : S ≤ R
sjx : S ∈ (J : (a : C) → Set (Sieve a)) X
Y : C
f : Y ⟶ X
hf : S.arrows f
a : Sieve.pullback f R = ⊤
⊢ Sieve.pullback f R ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
apply covering_of_eq_top

Premises used: CategoryTheory.GrothendieckTopology.covering_of_eq_top
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
Hss : S ≤ R
sjx : S ∈ (J : (a : C) → Set (Sieve a)) X
Y : C
f : Y ⟶ X
hf : S.arrows f
a : Sieve.pullback f S ≤ Sieve.pullback f R
⊢ Sieve.pullback f R = ⊤

Tactic:
rw [← top_le_iff, ← S.pullback_eq_top_of_mem hf]

Premises used: CategoryTheory.Sieve.pullback_eq_top_of_mem, top_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
Hss : S ≤ R
sjx : S ∈ (J : (a : C) → Set (Sieve a)) X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f S ≤ Sieve.pullback f R

Tactic:
apply Sieve.pullback_monotone _ Hss

Premises used: CategoryTheory.Sieve.pullback_monotone
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
rj : R ∈ (J : (a : C) → Set (Sieve a)) X
sj : S ∈ (J : (a : C) → Set (Sieve a)) X
apply : ∀ (Y : C) (f : Y ⟶ X) (Hf : R.arrows f), Sieve.pullback f (R ⊓ S) ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ R ⊓ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
apply J.transitive rj _ fun Y f Hf => _

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
rj : R ∈ (J : (a : C) → Set (Sieve a)) X
sj : S ∈ (J : (a : C) → Set (Sieve a)) X
Y : C
f : Y ⟶ X
hf : R.arrows f
rw : ⊤ ⊓ Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ Sieve.pullback f (R ⊓ S) ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
rw [Sieve.pullback_inter, R.pullback_eq_top_of_mem hf]

Premises used: CategoryTheory.Sieve.pullback_eq_top_of_mem, CategoryTheory.Sieve.pullback_inter
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
rj : R ∈ (J : (a : C) → Set (Sieve a)) X
sj : S ∈ (J : (a : C) → Set (Sieve a)) X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ ⊤ ⊓ Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
simp [sj]
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ R ⊓ S ∈ (J : (a : C) → Set (Sieve a)) X ↔ R ∈ (J : (a : C) → Set (Sieve a)) X ∧ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
⟨fun h => ⟨J.superset_covering inf_le_left h, J.superset_covering inf_le_right h⟩, fun t =>
    intersection_covering _ t.1 t.2⟩

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, inf_le_right, And.right, And.left, CategoryTheory.GrothendieckTopology.intersection_covering, And.intro, Iff.intro, inf_le_left
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
J : GrothendieckTopology.{v, u} C
S : Sieve.{v, u} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Sieve.{v, u} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (H : S.arrows f), R H ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ Sieve.bind S.arrows R ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.transitive hS _ fun _ f hf => superset_covering J (Sieve.le_pullback_bind S R f hf) (hR hf)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve.{v, u} (Z i)
h : Sieve.ofArrows Z f ∈ (J : (a : C) → Set (Sieve a)) X
hR :
  ∀ (i : ι), Membership.mem (γ := Set (Sieve.{v, u} (Z i))) ((J : (a : C) → Set (Sieve a)) (Z i)) (Sieve.generate (R i))
⊢ Sieve.generate (Presieve.bindOfArrows Z f R) ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.superset_covering (Presieve.bind_ofArrows_le_bindOfArrows _ _ _) ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve.{v, u} (Z i)
h : Sieve.ofArrows Z f ∈ (J : (a : C) → Set (Sieve a)) X
hR :
  ∀ (i : ι), Membership.mem (γ := Set (Sieve.{v, u} (Z i))) ((J : (a : C) → Set (Sieve a)) (Z i)) (Sieve.generate (R i))
refine :
  (Sieve.bind (Sieve.ofArrows Z f).arrows fun (x : C) (x_1 : x ⟶ X) (hg : (Sieve.ofArrows Z f).arrows x_1) ↦
      Sieve.pullback (Sieve.ofArrows.h hg) (Sieve.generate (R (Sieve.ofArrows.i hg)))) ∈
    (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.generate (Presieve.bindOfArrows Z f R) ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
refine J.superset_covering (Presieve.bind_ofArrows_le_bindOfArrows _ _ _) ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve.{v, u} (Z i)
h : Sieve.ofArrows Z f ∈ (J : (a : C) → Set (Sieve a)) X
hR :
  ∀ (i : ι), Membership.mem (γ := Set (Sieve.{v, u} (Z i))) ((J : (a : C) → Set (Sieve a)) (Z i)) (Sieve.generate (R i))
⊢ (Sieve.bind (Sieve.ofArrows Z f).arrows fun (x : C) (x_1 : x ⟶ X) (hg : (Sieve.ofArrows Z f).arrows x_1) ↦
      Sieve.pullback (Sieve.ofArrows.h hg) (Sieve.generate (R (Sieve.ofArrows.i hg)))) ∈
    (J : (a : C) → Set (Sieve a)) X

Tactic:
J.bind_covering h fun _ _ _ ↦ J.pullback_stable _ (hR _)

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Sieve.ofArrows.h, CategoryTheory.GrothendieckTopology.bind_covering, CategoryTheory.Sieve.ofArrows.i
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve.{v, u} (Z i)
h : Sieve.ofArrows Z f ∈ (J : (a : C) → Set (Sieve a)) X
hR :
  ∀ (i : ι), Membership.mem (γ := Set (Sieve.{v, u} (Z i))) ((J : (a : C) → Set (Sieve a)) (Z i)) (Sieve.generate (R i))
⊢ (Sieve.bind (Sieve.ofArrows Z f).arrows fun (x : C) (x_1 : x ⟶ X) (hg : (Sieve.ofArrows Z f).arrows x_1) ↦
      Sieve.pullback (Sieve.ofArrows.h hg) (Sieve.generate (R (Sieve.ofArrows.i hg)))) ∈
    (J : (a : C) → Set (Sieve a)) X

Tactic:
exact J.bind_covering h fun _ _ _ ↦ J.pullback_stable _ (hR _)

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.GrothendieckTopology.bind_covering
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
S : Sieve.{v, u} X
f : Y ⟶ X
⊢ J.Covers S f ↔ Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.GrothendieckTopology.Covers
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
J : GrothendieckTopology.{v, u} C
S : Sieve.{v, u} X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X ↔ J.Covers S (𝟙 X)

Tactic:
simp [covers_iff]

Premises used: CategoryTheory.GrothendieckTopology.covers_iff
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S : Sieve.{v, u} X
hf : S.arrows f
rw : ⊤ ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ J.Covers S f

Tactic:
rw [Covers, (Sieve.mem_iff_pullback_eq_top f).1 hf]

Premises used: CategoryTheory.Sieve.mem_iff_pullback_eq_top, CategoryTheory.GrothendieckTopology.Covers, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S : Sieve.{v, u} X
hf : S.arrows f
⊢ ⊤ ∈ (J : (a : C) → Set (Sieve a)) Y

Tactic:
apply J.top_mem

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S : Sieve.{v, u} X
h : J.Covers S f
Z : C
g : Z ⟶ Y
rw :
  ∀ (h : Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y) {Z : C} (g : Z ⟶ Y),
    Sieve.pullback (g ≫ f) S ∈ (J : (a : C) → Set (Sieve a)) Z
⊢ J.Covers S (g ≫ f)

Tactic:
rw [covers_iff] at h ⊢

Premises used: CategoryTheory.GrothendieckTopology.covers_iff
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S : Sieve.{v, u} X
h : Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y
Z : C
g : Z ⟶ Y
⊢ Sieve.pullback (g ≫ f) S ∈ (J : (a : C) → Set (Sieve a)) Z

Tactic:
simp [h, Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S R : Sieve.{v, u} X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
h₁ :
  ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ (J : (a : C) → Set (Sieve a)) Y_1
⊢ J.Covers R f

Tactic:
apply J.transitive h

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S R : Sieve.{v, u} X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
h₁ : Sieve.pullback (g ≫ f) R ∈ (J : (a : C) → Set (Sieve a)) Z
⊢ Sieve.pullback g (Sieve.pullback f R) ∈ (J : (a : C) → Set (Sieve a)) Z

Tactic:
rw [← Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S R : Sieve.{v, u} X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback (g ≫ f) R ∈ (J : (a : C) → Set (Sieve a)) Z

Tactic:
apply k (g ≫ f) hg

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
J : GrothendieckTopology.{v, u} C
f : Y ⟶ X
S R : Sieve.{v, u} X
hS : J.Covers S f
hR : J.Covers R f
⊢ J.Covers (S ⊓ R) f

Tactic:
simpa [covers_iff] using And.intro hS hR

Premises used: And.intro, CategoryTheory.GrothendieckTopology.covers_iff