awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve.{v, u} X :=
  Sieve.bind S.arrows fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦ (↑(x f hf) : (Functor.sieves C).obj (Opposite.op Y))
this :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = (↑(x f hf) : (Functor.sieves C).obj (Opposite.op Y))
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ J₁.close (↑(x f hf) : (Functor.sieves C).obj (Opposite.op Y)) = (↑(x f hf) : Sieve Y)

Tactic:
apply le_antisymm (J₁.le_close_of_isClosed le_rfl (x f hf).2) (J₁.le_close _)

Premises used: le_rfl, le_antisymm, CategoryTheory.GrothendieckTopology.le_close_of_isClosed, CategoryTheory.GrothendieckTopology.le_close, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X ↔ Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows

Tactic:
⟨fun hS ↦ classifier_isSheaf _ _ hS, fun H ↦ ?_⟩

Premises used: Iff.intro, CategoryTheory.classifier_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
refine : ∀ (H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows), S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X ↔ Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows

Tactic:
refine ⟨fun hS ↦ classifier_isSheaf _ _ hS, fun H ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
rw : J.close S = ⊤
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
rw [← J.close_eq_top_iff_mem]

Premises used: CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
Y : C
f : Y ⟶ X
_ : J.Covers ⊤ f → Sieve.arrows ⊤ f
⊢ J.Covers ⊤ f → Sieve.arrows ⊤ f

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
Y : C
f : Y ⟶ X
h : J.Covers ⊤ f
⊢ Sieve.arrows ⊤ f

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
⊢ J.IsClosed (X := X) ⊤

Tactic:
have : J.IsClosed (⊤ : Sieve X) := by
    intro Y f _
    trivial
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this_1 : J.IsClosed (X := X) ⊤
this : Subtype.mk (p := J.IsClosed) (J.close S) ⋯ = Subtype.mk (p := J.IsClosed) ⊤ this_1
⊢ (↑(Subtype.mk (p := J.IsClosed) (J.close S) ⋯) : Sieve X) = (↑(Subtype.mk (p := J.IsClosed) ⊤ this_1) : Sieve X)

Tactic:
rw [Subtype.ext_iff] at this

Premises used: Subtype.ext_iff
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this_1 : J.IsClosed (X := X) ⊤
this : (↑(Subtype.mk (p := J.IsClosed) (J.close S) ⋯) : Sieve X) = (↑(Subtype.mk (p := J.IsClosed) ⊤ this_1) : Sieve X)
⊢ J.close S = ⊤

Tactic:
this

Premises used: CategoryTheory.GrothendieckTopology.close
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this_1 : J.IsClosed (X := X) ⊤
this : (↑(Subtype.mk (p := J.IsClosed) (J.close S) ⋯) : Sieve X) = (↑(Subtype.mk (p := J.IsClosed) ⊤ this_1) : Sieve X)
⊢ J.close S = ⊤

Tactic:
exact this
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed (X := X) ⊤
suffices : Subtype.mk (p := J.IsClosed) (J.close S) ⋯ = Subtype.mk (p := J.IsClosed) ⊤ this
⊢ J.close S = ⊤

Tactic:
suffices (⟨J.close S, J.close_isClosed S⟩ : Subtype _) = ⟨⊤, this⟩ by
    rw [Subtype.ext_iff] at this
    exact this
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed (X := X) ⊤
⊢ Subtype.mk (p := J.IsClosed) (J.close S) ⋯ = Subtype.mk (p := J.IsClosed) ⊤ this

Tactic:
H.isSeparatedFor.ext fun Y f hf ↦ ?_

Premises used: Set.Mem, setOf, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.GrothendieckTopology.IsClosed
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed (X := X) ⊤
refine :
  ∀ (Y : C) (f : Y ⟶ X) (hf : S.arrows f),
    Eq (α := (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
            (a : (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op X))) →
              (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))
          (Subtype.mk (p := J.IsClosed) (J.close S) ⋯) :
        (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
            (a : (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op X))) →
              (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))
          (Subtype.mk (p := J.IsClosed) ⊤ this) :
        (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))
⊢ Subtype.mk (p := J.IsClosed) (J.close S) ⋯ = Subtype.mk (p := J.IsClosed) ⊤ this

Tactic:
refine H.isSeparatedFor.ext fun Y f hf ↦ ?_

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed (X := X) ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
simp :
  Eq (α := { x : Sieve.{v, u} Y // J.IsClosed x })
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
          (a : { x : Sieve X // J.IsClosed x }) → { x : Sieve Y // J.IsClosed x })
        (Subtype.mk (p := J.IsClosed) (J.close S) ⋯) :
      { x : Sieve.{v, u} Y // J.IsClosed x })
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
          (a : { x : Sieve X // J.IsClosed x }) → { x : Sieve Y // J.IsClosed x })
        (Subtype.mk (p := J.IsClosed) ⊤ this) :
      { x : Sieve.{v, u} Y // J.IsClosed x })
⊢ Eq (α := (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
          (a : (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op X))) →
            (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))
        (Subtype.mk (p := J.IsClosed) (J.close S) ⋯) :
      (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
          (a : (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op X))) →
            (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))
        (Subtype.mk (p := J.IsClosed) ⊤ this) :
      (fun (X : Type (max u v)) ↦ X) ((Functor.closedSieves J).toFunctor.obj (Opposite.op Y)))

Tactic:
simp only [Subfunctor.toFunctor_obj, Functor.sieves_obj, Functor.closedSieves_obj, Set.coe_setOf]

Premises used: CategoryTheory.Subfunctor.toFunctor_obj, CategoryTheory.Functor.closedSieves_obj, CategoryTheory.Functor.sieves_obj, Set.coe_setOf
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed (X := X) ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
a :
  Eq (α := Sieve.{v, u} Y)
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
            (a : { x : Sieve X // J.IsClosed x }) → { x : Sieve Y // J.IsClosed x })
          (Subtype.mk (p := J.IsClosed) (J.close S) ⋯)) :
      Sieve Y)
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
            (a : { x : Sieve X // J.IsClosed x }) → { x : Sieve Y // J.IsClosed x })
          (Subtype.mk (p := J.IsClosed) ⊤ this)) :
      Sieve Y)
⊢ Eq (α := { x : Sieve.{v, u} Y // J.IsClosed x })
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
          (a : { x : Sieve X // J.IsClosed x }) → { x : Sieve Y // J.IsClosed x })
        (Subtype.mk (p := J.IsClosed) (J.close S) ⋯) :
      { x : Sieve.{v, u} Y // J.IsClosed x })
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
          (a : { x : Sieve X // J.IsClosed x }) → { x : Sieve Y // J.IsClosed x })
        (Subtype.mk (p := J.IsClosed) ⊤ this) :
      { x : Sieve.{v, u} Y // J.IsClosed x })

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed (X := X) ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
a : Sieve.pullback f (J.close S) = Sieve.pullback f ⊤
⊢ Eq (α := Sieve.{v, u} Y)
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
            (a : { x : Sieve X // J.IsClosed x }) → { x : Sieve Y // J.IsClosed x })
          (Subtype.mk (p := J.IsClosed) (J.close S) ⋯)) :
      Sieve Y)
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.closedSieves J).toFunctor.map f.op) :
            (a : { x : Sieve X // J.IsClosed x }) → { x : Sieve Y // J.IsClosed x })
          (Subtype.mk (p := J.IsClosed) ⊤ this)) :
      Sieve Y)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed (X := X) ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
a : ⊤ ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ Sieve.pullback f (J.close S) = Sieve.pullback f ⊤

Tactic:
rw [Sieve.pullback_top, ← J.pullback_close, S.pullback_eq_top_of_mem hf,
    J.close_eq_top_iff_mem]

Premises used: CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem, CategoryTheory.Sieve.pullback_eq_top_of_mem, CategoryTheory.Sieve.pullback_top, CategoryTheory.GrothendieckTopology.pullback_close
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed (X := X) ⊤
Y : C
f : Y ⟶ 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.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
rw : Presieve.IsSheafFor (Functor.closedSieves J₂).toFunctor S.arrows
⊢ S ∈ (J₂ : (a : C) → Set (Sieve a)) X

Tactic:
rw [GrothendieckTopology.mem_iff_isSheafFor_closedSieves]

Premises used: CategoryTheory.GrothendieckTopology.mem_iff_isSheafFor_closedSieves
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSheafFor (Functor.closedSieves J₂).toFunctor S.arrows

Tactic:
h _ hS
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor
X : C
S : Sieve.{v, u} X
hS : S ∈ (J₁ : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSheafFor (Functor.closedSieves J₂).toFunctor S.arrows

Tactic:
exact h _ hS
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
mp : J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
mpr : (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂
⊢ J₁ = J₂ ↔ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
⊢ Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
mpr : J₁ ≤ J₂
mpr₁ : J₂ ≤ J₁
⊢ J₁ = J₂

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
mpr : Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor
⊢ J₁ ≤ J₂

Tactic:
apply le_topology_of_closedSieves_isSheaf

Premises used: CategoryTheory.le_topology_of_closedSieves_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
mpr : Presieve.IsSheaf J₂ (Functor.closedSieves J₂).toFunctor
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₂).toFunctor

Tactic:
apply classifier_isSheaf

Premises used: CategoryTheory.classifier_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
mpr : Presieve.IsSheaf J₂ (Functor.closedSieves J₁).toFunctor
⊢ J₂ ≤ J₁

Tactic:
apply le_topology_of_closedSieves_isSheaf

Premises used: CategoryTheory.le_topology_of_closedSieves_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
mpr : Presieve.IsSheaf J₁ (Functor.closedSieves J₁).toFunctor
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₁).toFunctor

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁).toFunctor

Tactic:
apply classifier_isSheaf

Premises used: CategoryTheory.classifier_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
c : (X : C) → ClosureOperator (Sieve.{v, u} X)
hc :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve.{v, u} X),
    (c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) = Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S)
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X |
      Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)}
    S
⊢ Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)

Tactic:
rw [Set.mem_setOf_eq] at hS

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
c : (X : C) → ClosureOperator (Sieve.{v, u} X)
hc :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve.{v, u} X),
    (c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) = Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S)
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
hS : Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)
rw :
  Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)
rw₁ : Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S) = ⊤
rw₂ : Sieve.pullback f ⊤ = ⊤
rw₃ rw₄ : Eq (α := Sieve.{v, u} Y) ⊤ ⊤
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y))
    {S : Sieve.{v, u} Y |
      Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) S : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)}
    (Sieve.pullback f S)

Tactic:
rw [Set.mem_setOf_eq, hc, hS, Sieve.pullback_top]

Premises used: Set.mem_setOf_eq, CategoryTheory.Sieve.pullback_top
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
c : (X : C) → ClosureOperator (Sieve.{v, u} X)
hc :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve.{v, u} X),
    (c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) = Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S)
X : C
S : Sieve.{v, u} X
hS :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X |
      Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)}
    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 |
          Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) S : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)}
        (Sieve.pullback f R)
rw :
  ∀ (hS : Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X))
    (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 |
              Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) S : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)}
            (Sieve.pullback f R)),
    Membership.mem (γ := Set (Sieve.{v, u} X))
      {S : Sieve.{v, u} X |
        Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)}
      R
⊢ Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X |
      Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)}
    R

Tactic:
rw [Set.mem_setOf_eq] at hS

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
c : (X : C) → ClosureOperator (Sieve.{v, u} X)
hc :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve.{v, u} X),
    (c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) = Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S)
X : C
S : Sieve.{v, u} X
hS : Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)
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 |
          Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) S : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)}
        (Sieve.pullback f R)
rw :
  LE.le (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X)
    ((c X : (a : Sieve X) → Sieve X) ((c X : (a : Sieve X) → Sieve X) R) : Sieve.{v, u} X)
⊢ Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X |
      Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)}
    R

Tactic:
rw [Set.mem_setOf_eq, ← (c X).idempotent, eq_top_iff, ← hS]

Premises used: eq_top_iff, Set.mem_setOf_eq, ClosureOperator.idempotent
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
c : (X : C) → ClosureOperator (Sieve.{v, u} X)
hc :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve.{v, u} X),
    (c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) = Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S)
X : C
S : Sieve.{v, u} X
hS : Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)
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 |
          Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) S : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)}
        (Sieve.pullback f R)
apply : ∀ (Y : C) (f : Y ⟶ X) (hf : S.arrows f), Sieve.arrows ((c X : (a : Sieve X) → Sieve X) R) f
⊢ LE.le (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X)
    ((c X : (a : Sieve X) → Sieve X) ((c X : (a : Sieve X) → Sieve X) R) : Sieve.{v, u} X)

Tactic:
apply (c X).monotone fun Y f hf => _

Premises used: ClosureOperator.monotone
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
c : (X : C) → ClosureOperator (Sieve.{v, u} X)
hc :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve.{v, u} X),
    (c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) = Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S)
X : C
S : Sieve.{v, u} X
hS : Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)
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 |
          Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) S : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)}
        (Sieve.pullback f R)
Y : C
f : Y ⟶ X
hf : S.arrows f
rw :
  Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f R) : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)
⊢ Sieve.arrows ((c X : (a : Sieve X) → Sieve X) R) f

Tactic:
rw [Sieve.mem_iff_pullback_eq_top, ← hc]

Premises used: CategoryTheory.Sieve.mem_iff_pullback_eq_top