awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.48971
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.48971} D
x y : Coverage.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hx : S ∈ x.coverings X
T : Presieve.{v_1, u_1} Y
hT : T ∈ x.coverings Y ∧ T.FactorsThruAlong S f
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
exact ⟨T, Or.inl hT.1, hT.2⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.48971
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.48971} D
x y : Coverage.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hy : S ∈ y.coverings X
inr :
  ∀ (T : Presieve.{v_1, u_1} Y) (hT : T ∈ y.coverings Y ∧ T.FactorsThruAlong S f),
    ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
obtain ⟨T, hT⟩ := y.pullback f S hy

Premises used: CategoryTheory.Coverage.pullback
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.48971
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.48971} D
x y : Coverage.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hy : S ∈ y.coverings X
T : Presieve.{v_1, u_1} Y
hT : T ∈ y.coverings Y ∧ T.FactorsThruAlong S f
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
⟨T, Or.inr hT.1, hT.2⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.48971
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.48971} D
x y : Coverage.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hy : S ∈ y.coverings X
T : Presieve.{v_1, u_1} Y
hT : T ∈ y.coverings Y ∧ T.FactorsThruAlong S f
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
exact ⟨T, Or.inr hT.1, hT.2⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x y : Coverage.{v_1, u_1} C
B : C
⊢ (x ⊔ y).coverings B = x.coverings B ∪ y.coverings B

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
R : Presieve.{v_1, u_1} X
h : R ≤ S.arrows
hR : R ∈ K.coverings X
⊢ S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
K.saturate_of_superset ((Sieve.generate_le_iff _ _).mpr h) (Coverage.Saturate.of X _ hR)

Premises used: Iff.mpr, Set.Mem, setOf, CategoryTheory.Coverage.saturate_of_superset, CategoryTheory.Coverage.Saturate.of, CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
X : C
S : Presieve.{v_1, u_1} X
⊢ S ∈ J.toCoverage.coverings X ↔ S ∈ J.coverings X

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
h :
  ∀ (T : C) (S : Sieve.{v_1, u_1} T),
    S ∈ (J.toCoverage.toGrothendieck : (a : C) → Set (Sieve a)) T ↔ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) T
⊢ J.toCoverage.toGrothendieck = J.toGrothendieck

Tactic:
ext T S
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
⊢ J.toCoverage.Saturate T S ↔ ∃ R ∈ J.coverings T, R ≤ S.arrows

Tactic:
⟨fun h ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩

Premises used: _private.0.CategoryTheory.Pretopology.toGrothendieck_toCoverage.match_1, Iff.intro, CategoryTheory.Pretopology.toCoverage, CategoryTheory.Coverage.Saturate
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
h : ∀ (h : J.toCoverage.Saturate T S), ∃ R ∈ J.coverings T, R ≤ S.arrows
h₁ :
  (∃ R ∈ J.coverings T, R ≤ S.arrows) →
    ∀ (R : Presieve.{v_1, u_1} T) (hR : R ∈ J.coverings T) (hle : R ≤ S.arrows), J.toCoverage.Saturate T S
⊢ J.toCoverage.Saturate T S ↔ ∃ R ∈ J.coverings T, R ≤ S.arrows

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ J.toCoverage.coverings X
w : Presieve.{v_1, u_1} X
left : S ∈ J.coverings X
right : S ≤ (Sieve.generate S).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ (Sieve.generate S).arrows

Tactic:
use S, hS, Sieve.le_generate S

Premises used: CategoryTheory.Sieve.le_generate
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
X : C
w : Presieve.{v_1, u_1} X
left : Presieve.singleton (𝟙 X) ∈ J.coverings X
right : LE.le (α := Presieve.{v_1, u_1} X) (Presieve.singleton (𝟙 X)) (Sieve.arrows ⊤)
⊢ ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤

Tactic:
use Presieve.singleton (𝟙 X), J.has_isos (𝟙 X), le_top

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Pretopology.has_isos, le_top, CategoryTheory.Presieve.singleton
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
hle : ∃ R_1 ∈ J.coverings X, R_1 ≤ R.arrows
hfS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
h : ∀ (R' : Presieve.{v_1, u_1} X) (hR' : R' ∈ J.coverings X) (hle : R' ≤ R.arrows), ∃ R ∈ J.coverings X, R ≤ S.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
obtain ⟨R', hR', hle⟩ := hle
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
hfS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
h :
  ∀ (S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y)
    (hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y)
    (hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows),
    ∃ R ∈ J.coverings X, R ≤ S.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
choose S' hS' hS'le using hfS
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ _ hf)), ?_, fun Z u hu ↦ ?_⟩

Premises used: CategoryTheory.Presieve.bind, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
h : (R'.bind fun (Y : C) (f : Y ⟶ X) (hf : R' f) ↦ S' ⋯) ∈ J.coverings X
h₁ : ∀ (Z : C) (u : Z ⟶ X) (hu : R'.bind (fun (Y : C) (f : Y ⟶ X) (hf : R' f) ↦ S' ⋯) u), S.arrows u
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
refine ⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ _ hf)), ?_, fun Z u hu ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
⊢ (R'.bind fun (Y : C) (f : Y ⟶ X) (hf : R' f) ↦ S' ⋯) ∈ J.coverings X

Tactic:
J.transitive R' (fun Y f hf ↦ S' (hle Y _ hf)) hR' fun Y f H ↦ hS' (hle Y _ H)

Premises used: CategoryTheory.Pretopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
⊢ (R'.bind fun (Y : C) (f : Y ⟶ X) (hf : R' f) ↦ S' ⋯) ∈ J.coverings X

Tactic:
exact J.transitive R' (fun Y f hf ↦ S' (hle Y _ hf)) hR' fun Y f H ↦ hS' (hle Y _ H)

Premises used: CategoryTheory.Pretopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
Z : C
u : Z ⟶ X
hu : R'.bind (fun (Y : C) (f : Y ⟶ X) (hf : R' f) ↦ S' ⋯) u
h : ∀ (W : C) (g : Z ⟶ W) (w : W ⟶ X) (hw : R' w) (hg : S' ⋯ g), S.arrows (g ≫ w)
⊢ S.arrows u

Tactic:
obtain ⟨W, g, w, hw, hg, rfl⟩ := hu

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
Z W : C
g : Z ⟶ W
w : W ⟶ X
hw : R' w
hg : S' ⋯ g
⊢ S.arrows (g ≫ w)

Tactic:
hS'le _ _ _ hg
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
Z W : C
g : Z ⟶ W
w : W ⟶ X
hw : R' w
hg : S' ⋯ g
⊢ S.arrows (g ≫ w)

Tactic:
exact hS'le _ _ _ hg
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
h : J.toCoverage.Saturate T S
h₁ :
  ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ J.toCoverage.coverings X),
    ∃ R ∈ J.coverings X, R ≤ (Sieve.generate S).arrows
h₂ : ∀ (X : C), ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤
h₃ :
  ∀ (X : C) (R S : Sieve.{v_1, u_1} X) (hR : J.toCoverage.Saturate X R)
    (hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S))
    (hle : ∃ R_1 ∈ J.coverings X, R_1 ≤ R.arrows)
    (hfS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows),
    ∃ R ∈ J.coverings X, R ≤ S.arrows
⊢ ∃ R ∈ J.coverings T, R ≤ S.arrows

Tactic:
induction h with
    | of X S hS => use S, hS, Sieve.le_generate S
    | top X => use Presieve.singleton (𝟙 X), J.has_isos (𝟙 X), le_top
    | transitive X R S hR hRS hle hfS =>
        obtain ⟨R', hR', hle⟩ := hle
        choose S' hS' hS'le using hfS
        refine ⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ _ hf)), ?_, fun Z u hu ↦ ?_⟩
        · exact J.transitive R' (fun Y f hf ↦ S' (hle Y _ hf)) hR' fun Y f H ↦ hS' (hle Y _ H)
        · obtain ⟨W, g, w, hw, hg, rfl⟩ := hu
          exact hS'le _ _ _ hg

Premises used: CategoryTheory.Pretopology.transitive, CategoryTheory.Sieve.le_generate, le_top, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
h : ∃ R ∈ J.coverings T, R ≤ S.arrows
R : Presieve.{v_1, u_1} T
hR : R ∈ J.coverings T
hle : R ≤ S.arrows
⊢ J.toCoverage.Saturate T S

Tactic:
Coverage.saturate_of_superset _ ?_ (.of _ _ hR)

Premises used: CategoryTheory.Coverage.saturate_of_superset, CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
h_1 : ∃ R ∈ J.coverings T, R ≤ S.arrows
R : Presieve.{v_1, u_1} T
hR : R ∈ J.coverings T
hle : R ≤ S.arrows
h : Sieve.generate R ≤ S
⊢ J.toCoverage.Saturate T S

Tactic:
refine Coverage.saturate_of_superset _ ?_ (.of _ _ hR)

Premises used: CategoryTheory.Coverage.saturate_of_superset, CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
h_1 : ∃ R ∈ J.coverings T, R ≤ S.arrows
R : Presieve.{v_1, u_1} T
hR : R ∈ J.coverings T
hle : R ≤ S.arrows
h h₁ h₂ h₃ : R ≤ S.arrows
⊢ Sieve.generate R ≤ S

Tactic:
rwa [Sieve.generate_le_iff]

Premises used: CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.54698
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.54698} D
J : Precoverage.{v_1, u_1} C
inst_2 : J.HasPullbacks
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ J.coverings X
⊢ S.HasPullbacks f

Tactic:
have : S.HasPullbacks f := J.hasPullbacks_of_mem _ hS
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.54698
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.54698} D
J : Precoverage.{v_1, u_1} C
inst_2 : J.HasPullbacks
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ J.coverings X
this : S.HasPullbacks f
⊢ ∃ T ∈ J.coverings Y, T.FactorsThruAlong S f

Tactic:
⟨S.pullbackArrows f, J.pullbackArrows_mem _ hS,
      Presieve.FactorsThruAlong.pullbackArrows f S⟩

Premises used: CategoryTheory.Presieve.pullbackArrows, CategoryTheory.Precoverage.pullbackArrows_mem, And.intro, Exists.intro, CategoryTheory.Presieve.FactorsThruAlong.pullbackArrows
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.54698
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.54698} D
J : Precoverage.{v_1, u_1} C
inst_2 : J.HasPullbacks
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ J.coverings X
this : S.HasPullbacks f
⊢ ∃ T ∈ J.coverings Y, T.FactorsThruAlong S f

Tactic:
exact ⟨S.pullbackArrows f, J.pullbackArrows_mem _ hS,
      Presieve.FactorsThruAlong.pullbackArrows f S⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Precoverage.{v_1, u_1} C
inst_1 : J.HasPullbacks
inst_2 : J.IsStableUnderBaseChange
K : GrothendieckTopology.{v_1, u_1} C
⊢ (J.toCoverage ≤ K.toCoverage) = ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Subset, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Precoverage.{v_1, u_1} C
inst_1 : J.HasPullbacks
inst_2 : J.IsStableUnderBaseChange
⊢ J.toCoverage.toGrothendieck = J.toGrothendieck

Tactic:
grind [toGrothendieck_eq_sInf, Coverage.toGrothendieck_eq_sInf,
    Precoverage.toCoverage_le_toCoverage]

Premises used: CategoryTheory.Coverage.toGrothendieck_eq_sInf, CategoryTheory.Precoverage.toCoverage_le_toCoverage, CategoryTheory.Precoverage.toGrothendieck_eq_sInf
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Coverage.{v_1, u_1} C
rw : J.toGrothendieck = J.toGrothendieck.copy (fun (X : C) ↦ setOf (J.Saturate X)) ⋯
rw₁ rw₂ : J.toGrothendieck = J.toGrothendieck
⊢ J.toGrothendieck = J.toGrothendieck

Tactic:
rw [Coverage.toGrothendieck, GrothendieckTopology.copy_eq]

Premises used: CategoryTheory.Coverage.toGrothendieck, CategoryTheory.GrothendieckTopology.copy_eq
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
rw :
  (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) ↔
    ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
⊢ IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
rw [← toGrothendieck_toPrecoverage, Precoverage.isSheaf_toGrothendieck_iff]

Premises used: CategoryTheory.Coverage.toGrothendieck_toPrecoverage, CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
mp :
  (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) →
    ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
mpr :
  (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
⊢ (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) ↔
    ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
⊢ IsSheafFor P S

Tactic:
simpa [← Presieve.isSheafFor_iff_generate] using H (f := 𝟙 X) S hS

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
mpr :
  ∀ (T : Presieve.{v_1, u_2} Y) (hT1 : T ∈ K.coverings Y) (hT2 : T.FactorsThruAlong S f),
    IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows

Tactic:
obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS

Premises used: CategoryTheory.Coverage.pullback
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
mpr : T.FactorsThru (Sieve.pullback f (Sieve.generate S)).arrows
mpr₁ : IsSheafFor P T
mpr₂ :
  ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f (Sieve.generate S)).arrows f_1 →
      ∃ (R : Presieve.{v_1, u_2} Y_1), IsSeparatedFor P R ∧ R.FactorsThruAlong T f_1
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows

Tactic:
apply Presieve.isSheafFor_of_factorsThru (S := T)

Premises used: CategoryTheory.Presieve.isSheafFor_of_factorsThru
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
hg : T g
mpr :
  ∀ (W : C) (i : Z ⟶ W) (e : W ⟶ X) (h1 : S e) (h2 : i ≫ e = g ≫ f),
    ∃ (W : C) (i : Z ⟶ W) (e : W ⟶ Y), (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g
⊢ ∃ (W : C) (i : Z ⟶ W) (e : W ⟶ Y), (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g

Tactic:
obtain ⟨W, i, e, h1, h2⟩ := hT2 hg
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
hg : T g
W : C
i : Z ⟶ W
e : W ⟶ X
h1 : S e
h2 : i ≫ e = g ≫ f
⊢ 𝟙 Z ≫ g = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
hg : T g
W : C
i : Z ⟶ W
e : W ⟶ X
h1 : S e
h2 : i ≫ e = g ≫ f
⊢ ∃ (W : C) (i : Z ⟶ W) (e : W ⟶ Y), (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g

Tactic:
exact ⟨Z, 𝟙 _, g, ⟨W, i, e, h1, h2⟩, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
mpr : T ∈ K.coverings Y
⊢ IsSheafFor P T

Tactic:
apply H
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_2} X
hS : S ∈ K.coverings X
T : Presieve.{v_1, u_2} Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ T ∈ K.coverings Y

Tactic:
assumption