awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
hf : Membership.mem (γ := Set (Sieve.{v, u} X)) {⊤} S
⊢ S = ⊤

Tactic:
rw [Set.mem_singleton_iff] at hf ⊢

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
hf : S = ⊤
⊢ Sieve.pullback f S = ⊤

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : Membership.mem (γ := Set (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)) {⊤} (Sieve.pullback f R)
rw :
  ∀ (hS : S.arrows (𝟙 X)) (R : Sieve.{v, u} X)
    (hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Membership.mem (γ := Set (Sieve.{v, u} Y)) {⊤} (Sieve.pullback f R)),
    Membership.mem (γ := Set (Sieve.{v, u} X)) {⊤} R
⊢ Membership.mem (γ := Set (Sieve.{v, u} X)) {⊤} R

Tactic:
rw [Set.mem_singleton_iff, ← Sieve.id_mem_iff_eq_top] at hS

Premises used: Set.mem_singleton_iff, CategoryTheory.Sieve.id_mem_iff_eq_top
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S.arrows (𝟙 X)
R : Sieve.{v, u} X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Membership.mem (γ := Set (Sieve.{v, u} Y)) {⊤} (Sieve.pullback f R)
⊢ Membership.mem (γ := Set (Sieve.{v, u} X)) {⊤} R

Tactic:
simpa using hR hS
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ ∀ (X : C), Membership.mem (γ := Set (Sieve.{v, u} X)) Set.univ ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X Y : C
f : Sieve.{v, u} X
⊢ ∀ (f_1 : Y ⟶ X),
    Membership.mem (γ := Set (Sieve.{v, u} X)) Set.univ f →
      Membership.mem (γ := Set (Sieve.{v, u} Y)) Set.univ (Sieve.pullback f_1 f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve.{v, u} X⦄,
    Membership.mem (γ := Set (Sieve.{v, u} X)) Set.univ S →
      ∀ (R : Sieve.{v, u} X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Membership.mem (γ := Set (Sieve.{v, u} Y)) Set.univ (Sieve.pullback f R)) →
          Membership.mem (γ := Set (Sieve.{v, u} X)) Set.univ R

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
⊢ S ∈ (trivial C : (a : C) → Set (Sieve a)) X ↔ S = ⊤

Tactic:
Set.mem_singleton_iff

Premises used: Set.Mem, setOf, Set.mem_singleton_iff, Set.singleton
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
⊢ J₁ ≤ J₂ ↔ (⇑J₁ : (a : C) → Set (Sieve a)) ≤ (⇑J₂ : (a : C) → Set (Sieve a))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S R : Sieve.{v, u} X_1
J_1 : GrothendieckTopology.{v, u} C
T : Set (GrothendieckTopology.{v, u} C)
X : C
J : GrothendieckTopology.{v, u} C
hJ : J ∈ T
⊢ Membership.mem (γ := Set (Sieve.{v, u} X))
    ((fun (f : (↑(sieves '' T) : Type (max u v))) ↦ (↑f : (i : C) → (fun (X : C) ↦ Set (Sieve X)) i) X)
      (Subtype.mk (p := fun (x : (i : C) → (fun (X : C) ↦ Set (Sieve.{v, u} X)) i) ↦ x ∈ sieves '' T) J.sieves ⋯))
    ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J_1 : GrothendieckTopology.{v, u} C
T : Set (GrothendieckTopology.{v, u} C)
X Y : C
S : Sieve.{v, u} X
hS : Y ⟶ X
f : S ∈ sInf (sieves '' T) X
J : GrothendieckTopology.{v, u} C
hJ : J ∈ T
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y))
    ((fun (f : (↑(sieves '' T) : Type (max u v))) ↦ (↑f : (i : C) → (fun (X : C) ↦ Set (Sieve X)) i) Y)
      (Subtype.mk (p := fun (x : (i : C) → (fun (X : C) ↦ Set (Sieve.{v, u} X)) i) ↦ x ∈ sieves '' T) J.sieves ⋯))
    (Sieve.pullback hS S)

Tactic:
apply J.pullback_stable _ (f _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩)

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S_1 R_1 : Sieve.{v, u} X_1
J_1 : GrothendieckTopology.{v, u} C
T : Set (GrothendieckTopology.{v, u} C)
X : C
S : Sieve.{v, u} X
hS : S ∈ sInf (sieves '' T) X
R : Sieve.{v, u} X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sInf (sieves '' T) Y
J : GrothendieckTopology.{v, u} C
hJ : J ∈ T
⊢ Membership.mem (γ := Set (Sieve.{v, u} X))
    ((fun (f : (↑(sieves '' T) : Type (max u v))) ↦ (↑f : (i : C) → (fun (X : C) ↦ Set (Sieve X)) i) X)
      (Subtype.mk (p := fun (x : (i : C) → (fun (X : C) ↦ Set (Sieve.{v, u} X)) i) ↦ x ∈ sieves '' T) J.sieves ⋯))
    R

Tactic:
apply
          J.transitive (hS _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩) _ fun Y f hf => h hf _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩

Premises used: CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.GrothendieckTopology.sieves, Subtype.mk, And.intro, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
s : Set (GrothendieckTopology.{v, u} C)
X : C
S : Sieve.{v, u} X
⊢ S ∈ sInf (sieves '' s) X ↔ ∀ t ∈ s, S ∈ (t : (a : C) → Set (Sieve a)) X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
s : Set (GrothendieckTopology.{v, u} C)
⊢ IsGLB s (sInf s)

Tactic:
@IsGLB.of_image _ _ _ _ sieves ?_ _ _ ?_

Premises used: IsGLB.of_image
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
s : Set (GrothendieckTopology.{v, u} C)
refine_1 : ∀ {x y : GrothendieckTopology.{v, u} C}, x.sieves ≤ y.sieves ↔ x ≤ y
refine_2 : IsGLB (sieves '' s) (sInf s).sieves
⊢ IsGLB s (sInf s)

Tactic:
refine @IsGLB.of_image _ _ _ _ sieves ?_ _ _ ?_

Premises used: IsGLB.of_image
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
s : Set (GrothendieckTopology.{v, u} C)
⊢ ∀ {x y : GrothendieckTopology.{v, u} C}, x.sieves ≤ y.sieves ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
s : Set (GrothendieckTopology.{v, u} C)
⊢ IsGLB (sieves '' s) (sInf s).sieves

Tactic:
_root_.isGLB_sInf _

Premises used: isGLB_sInf
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
s : Set (GrothendieckTopology.{v, u} C)
⊢ IsGLB (sieves '' s) (sInf s).sieves

Tactic:
exact _root_.isGLB_sInf _

Premises used: isGLB_sInf
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
a : LE.le (α := GrothendieckTopology.{v, u} C) (discrete C) ⊤
a₁ : LE.le (α := GrothendieckTopology.{v, u} C) ⊤ (discrete C)
⊢ Eq (α := GrothendieckTopology.{v, u} C) (discrete C) ⊤

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ LE.le (α := GrothendieckTopology.{v, u} C) (discrete C) ⊤

Tactic:
(completeLatticeOfInf _ isGLB_sInf).le_top (discrete C)

Premises used: OrderTop.le_top, CategoryTheory.GrothendieckTopology.discrete
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ LE.le (α := GrothendieckTopology.{v, u} C) (discrete C) ⊤

Tactic:
exact (completeLatticeOfInf _ isGLB_sInf).le_top (discrete C)

Premises used: OrderTop.le_top, CategoryTheory.GrothendieckTopology.discrete
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
a : S ∈ (⊤ : (a : C) → Set (Sieve a)) X → S ∈ (discrete C : (a : C) → Set (Sieve a)) X
⊢ S ∈ (⊤ : (a : C) → Set (Sieve a)) X → S ∈ (discrete C : (a : C) → Set (Sieve a)) X

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
h : S ∈ (⊤ : (a : C) → Set (Sieve a)) X
⊢ S ∈ (discrete C : (a : C) → Set (Sieve a)) X

Tactic:
apply Set.mem_univ

Premises used: Set.mem_univ
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
a : LE.le (α := GrothendieckTopology.{v, u} C) (trivial C) ⊥
a₁ : LE.le (α := GrothendieckTopology.{v, u} C) ⊥ (trivial C)
⊢ Eq (α := GrothendieckTopology.{v, u} C) (trivial C) ⊥

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S ∈ (trivial C : (a : C) → Set (Sieve a)) X
⊢ S = ⊤

Tactic:
rw [trivial_covering] at hS

Premises used: CategoryTheory.GrothendieckTopology.trivial_covering
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
hS : S = ⊤
⊢ S ∈ (⊥ : (a : C) → Set (Sieve a)) X

Tactic:
apply covering_of_eq_top _ hS

Premises used: CategoryTheory.GrothendieckTopology.covering_of_eq_top
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ LE.le (α := GrothendieckTopology.{v, u} C) ⊥ (trivial C)

Tactic:
(completeLatticeOfInf _ isGLB_sInf).bot_le (trivial C)

Premises used: OrderBot.bot_le, CategoryTheory.GrothendieckTopology.trivial
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S R : Sieve.{v, u} X
J : GrothendieckTopology.{v, u} C
⊢ LE.le (α := GrothendieckTopology.{v, u} C) ⊥ (trivial C)

Tactic:
exact (completeLatticeOfInf _ isGLB_sInf).bot_le (trivial C)

Premises used: OrderBot.bot_le, CategoryTheory.GrothendieckTopology.trivial
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := GrothendieckTopology.{v, u} C) (trivial C) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := GrothendieckTopology.{v, u} C) (discrete C) ⊤

Tactic:
rfl

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

Tactic:
trivial_covering

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

Tactic:
⟨⟩

Premises used: Set.Mem, Set.univ, setOf, True.intro
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
rw : Sieve.pullback f S ∈ (⊥ : (a : C) → Set (Sieve a)) Y ↔ S.arrows f
rw₁ : Sieve.pullback f S = ⊤ ↔ S.arrows f
rw₂ rw₃ : S.arrows f ↔ S.arrows f
⊢ Covers ⊥ S f ↔ S.arrows f

Tactic:
rw [covers_iff, bot_covering, ← Sieve.mem_iff_pullback_eq_top]

Premises used: CategoryTheory.Sieve.mem_iff_pullback_eq_top, CategoryTheory.GrothendieckTopology.bot_covering, CategoryTheory.GrothendieckTopology.covers_iff
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
S : Sieve.{v, u} X
f : Y ⟶ X
⊢ Covers ⊤ S f

Tactic:
simp [covers_iff]

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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
refine : ∀ (h : ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X), J = ⊤
⊢ J = ⊤ ↔ ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
refine ⟨fun h ↦ h ▸ by simp, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
h : ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
rw : ⊤ ≤ J
⊢ J = ⊤

Tactic:
rw [_root_.eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
h : ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
X : C
S : Sieve.{v, u} X
_ : S ∈ (⊤ : (a : C) → Set (Sieve a)) X → S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (⊤ : (a : C) → Set (Sieve a)) X → S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
h : ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
X : C
S : Sieve.{v, u} X
h_1 : S ∈ (⊤ : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.superset_covering bot_le (h X)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, bot_le
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
h : ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
X : C
S : Sieve.{v, u} X
h_1 : S ∈ (⊤ : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
exact J.superset_covering bot_le (h X)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, bot_le
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsEmpty C
J : GrothendieckTopology.{v, u} C
rw : ∀ (X : C), ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
⊢ J = ⊤

Tactic:
rw [eq_top_iff]

Premises used: CategoryTheory.GrothendieckTopology.eq_top_iff
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsEmpty C
J : GrothendieckTopology.{v, u} C
X : C
⊢ ⊥ ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
IsEmpty.elim ‹IsEmpty C› X

Premises used: IsEmpty.elim
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsEmpty C
J : GrothendieckTopology.{v, u} C
X : C
⊢ ⊥ ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
exact IsEmpty.elim ‹IsEmpty C› X
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := GrothendieckTopology.{v, u} C) ⊥ ⊤ ↔ IsEmpty C

Tactic:
⟨fun h ↦ ⟨fun X ↦ ?_⟩, fun h ↦ eq_top_of_isEmpty _⟩

Premises used: Bot.bot, IsEmpty.mk, CategoryTheory.GrothendieckTopology.eq_top_of_isEmpty, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
refine : ∀ (h : Eq (α := GrothendieckTopology.{v, u} C) ⊥ ⊤) (X : C), False
⊢ Eq (α := GrothendieckTopology.{v, u} C) ⊥ ⊤ ↔ IsEmpty C

Tactic:
refine ⟨fun h ↦ ⟨fun X ↦ ?_⟩, fun h ↦ eq_top_of_isEmpty _⟩
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
h : Eq (α := GrothendieckTopology.{v, u} C) ⊥ ⊤
X : C
apply : Eq (α := Sieve.{v, u} X) ⊥ ⊤
⊢ False

Tactic:
apply bot_ne_top (α := Sieve X)

Premises used: bot_ne_top
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
h : Eq (α := GrothendieckTopology.{v, u} C) ⊥ ⊤
X : C
⊢ Eq (α := Sieve.{v, u} X) ⊥ ⊤

Tactic:
simp only [← GrothendieckTopology.bot_covering, h, top_covering]

Premises used: CategoryTheory.GrothendieckTopology.bot_covering, CategoryTheory.GrothendieckTopology.top_covering
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
contrapose! : ¬LT.lt (α := GrothendieckTopology.{v, u} C) ⊥ ⊤ ↔ IsEmpty C
⊢ LT.lt (α := GrothendieckTopology.{v, u} C) ⊥ ⊤ ↔ Nonempty C

Tactic:
contrapose!
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
⊢ ¬LT.lt (α := GrothendieckTopology.{v, u} C) ⊥ ⊤ ↔ IsEmpty C

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
h : Y ⟶ X
H :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
Z : C
f : Z ⟶ Y
rcases :
  ∀ (W : C) (g : W ⟶ Z) (H' : S.arrows (g ≫ f ≫ h)), ∃ (Z_1 : C) (g : Z_1 ⟶ Z), (Sieve.pullback h S).arrows (g ≫ f)
⊢ ∃ (Z_1 : C) (g : Z_1 ⟶ Z), (Sieve.pullback h S).arrows (g ≫ f)

Tactic:
rcases H (f ≫ h) with ⟨W, g, H'⟩

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
h : Y ⟶ X
H :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
Z : C
f : Z ⟶ Y
W : C
g : W ⟶ Z
H' : S.arrows (g ≫ f ≫ h)
⊢ (Sieve.pullback h S).arrows (g ≫ f)

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X Y : C
S : Sieve.{v, u} X
h : Y ⟶ X
H :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
Z : C
f : Z ⟶ Y
W : C
g : W ⟶ Z
H' : S.arrows (g ≫ f ≫ h)
⊢ ∃ (Z_1 : C) (g : Z_1 ⟶ Z), (Sieve.pullback h S).arrows (g ≫ f)

Tactic:
exact ⟨W, g, by simpa⟩
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H₁ :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
R : Sieve.{v, u} X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ {Y_2 : C} (f : Y_2 ⟶ Y), ∃ (Z : C) (g : Z ⟶ Y_2), S.arrows (g ≫ f)} (Sieve.pullback f R)
Y : C
f : Y ⟶ X
rcases : ∀ (Z : C) (g : Z ⟶ Y) (H₃ : S.arrows (g ≫ f)), ∃ (Z : C) (g : Z ⟶ Y), R.arrows (g ≫ f)
⊢ ∃ (Z : C) (g : Z ⟶ Y), R.arrows (g ≫ f)

Tactic:
rcases H₁ f with ⟨Z, g, H₃⟩
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H₁ :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
R : Sieve.{v, u} X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ {Y_2 : C} (f : Y_2 ⟶ Y), ∃ (Z : C) (g : Z ⟶ Y_2), S.arrows (g ≫ f)} (Sieve.pullback f R)
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
rcases :
  ∀ (W : C) (h : W ⟶ Z) (H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)), ∃ (Z : C) (g : Z ⟶ Y), R.arrows (g ≫ f)
⊢ ∃ (Z : C) (g : Z ⟶ Y), R.arrows (g ≫ f)

Tactic:
rcases H₂ H₃ (𝟙 Z) with ⟨W, h, H₄⟩

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H₁ :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
R : Sieve.{v, u} X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ {Y_2 : C} (f : Y_2 ⟶ Y), ∃ (Z : C) (g : Z ⟶ Y_2), S.arrows (g ≫ f)} (Sieve.pullback f R)
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
W : C
h : W ⟶ Z
H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)
⊢ R.arrows ((h ≫ g) ≫ f)

Tactic:
simpa using H₄
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R_1 : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
H₁ :
  Membership.mem (γ := Set (Sieve.{v, u} X))
    {S : Sieve.{v, u} X | ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)} S
R : Sieve.{v, u} X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y | ∀ {Y_2 : C} (f : Y_2 ⟶ Y), ∃ (Z : C) (g : Z ⟶ Y_2), S.arrows (g ≫ f)} (Sieve.pullback f R)
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
W : C
h : W ⟶ Z
H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)
⊢ ∃ (Z : C) (g : Z ⟶ Y), R.arrows (g ≫ f)

Tactic:
exact ⟨W, h ≫ g, by simpa using H₄⟩
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
⊢ S ∈ (dense : (a : C) → Set (Sieve a)) X ↔ ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (g ≫ f)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasPullbacks.{v, u} C
X Y Z : C
⊢ ∀ (yx : Y ⟶ X) (zx : Z ⟶ X), ∃ (W : C) (wy : W ⟶ Y) (wz : W ⟶ Z), wy ≫ yx = wz ≫ zx

Tactic:
fun _ _ =>
  ⟨_, _, _, Limits.pullback.condition⟩

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.pullback.fst, Exists.intro, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
hro : RightOreCondition.{v, u} C
X Y : C
S : Sieve.{v, u} X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
rcases :
  ∀ (W : C) (g : W ⟶ Y) (k : W ⟶ Z) (comm : g ≫ h = k ≫ f),
    Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y), S.arrows f}
      (Sieve.pullback h S)
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y), S.arrows f}
    (Sieve.pullback h S)

Tactic:
rcases hro h f with ⟨W, g, k, comm⟩

Premises used: comm
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
hro : RightOreCondition.{v, u} C
X Y : C
S : Sieve.{v, u} X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y), S.arrows f}
    (Sieve.pullback h S)

Tactic:
⟨_, g, ?_⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
S_1 R : Sieve.{v, u} X_1
J : GrothendieckTopology.{v, u} C
hro : RightOreCondition.{v, u} C
X Y : C
S : Sieve.{v, u} X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
refine : (Sieve.pullback h S).arrows g
⊢ Membership.mem (γ := Set (Sieve.{v, u} Y)) {S : Sieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y), S.arrows f}
    (Sieve.pullback h S)

Tactic:
refine ⟨_, g, ?_⟩