awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve.{v_1, u_1} Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
WW : C
ii : W ⟶ WW
ee : WW ⟶ X
hh1 : S ee
hh2 : ii ≫ ee = e ≫ f
⊢ (i ≫ ii) ≫ ee = g ≫ f

Tactic:
simp [hh2, reassoc_of% h2]
-- 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_1 Y : C
S : Sieve.{v_1, u_1} X_1
X : C
f : Y ⟶ X
⊢ K.Saturate Y (Sieve.pullback f ⊤)

Tactic:
.top _

Premises used: CategoryTheory.Coverage.Saturate.top, CategoryTheory.Sieve.pullback
-- 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_1 Y : C
S : Sieve.{v_1, u_1} X_1
X : C
f : Y ⟶ X
⊢ K.Saturate Y (Sieve.pullback f ⊤)

Tactic:
exact .top _
-- 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_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : K.Saturate X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)
a_ih : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄, R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))
f : Y ⟶ X
⊢ K.Saturate Y (Sieve.pullback f S)

Tactic:
(H1 f).transitive _ _ _ fun Z g hg ↦ ?_

Premises used: CategoryTheory.Coverage.Saturate.transitive
-- 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_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : K.Saturate X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)
a_ih : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄, R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))
f : Y ⟶ X
transitive :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f R).arrows g), K.Saturate Z (Sieve.pullback g (Sieve.pullback f S))
⊢ K.Saturate Y (Sieve.pullback f S)

Tactic:
refine (H1 f).transitive _ _ _ fun Z g hg ↦ ?_

Premises used: CategoryTheory.Coverage.Saturate.transitive
-- 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_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : K.Saturate X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)
a_ih : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄, R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))
f : Y ⟶ X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
transitive : K.Saturate Z (Sieve.pullback (g ≫ f) S)
⊢ K.Saturate Z (Sieve.pullback g (Sieve.pullback f S))

Tactic:
rw [← Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- 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_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : K.Saturate X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)
a_ih : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄, R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))
f : Y ⟶ X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ K.Saturate Z (Sieve.pullback (g ≫ f) S)

Tactic:
hS hg
-- 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_1 Y : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : K.Saturate X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)
a_ih : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄, R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))
f : Y ⟶ X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ K.Saturate Z (Sieve.pullback (g ≫ f) S)

Tactic:
exact hS hg
-- 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 Y : C
f : Y ⟶ X
S : Sieve.{v_1, u_1} X
h : K.Saturate X S
of :
  ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X) (f : Y ⟶ X),
    K.Saturate Y (Sieve.pullback f (Sieve.generate S))
top : ∀ (X : C) (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f ⊤)
transitive :
  ∀ (X : C) (R S : Sieve.{v_1, u_1} X),
    K.Saturate X R →
      ∀ (hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S))
        (H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)),
        (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
            R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))) →
          ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f S)
⊢ K.Saturate Y (Sieve.pullback f S)

Tactic:
induction h with
  | of X S hS =>
    obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
    suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from
      saturate_of_superset _ this (Saturate.of _ _ hR1)
    intro Z g ⟨W, i, e, h1, h2⟩
    obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
    refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
    simp [hh2, reassoc_of% h2]
  | top X => exact .top _
  | transitive X R S _ hS H1 _ =>
    refine (H1 f).transitive _ _ _ fun Z g hg ↦ ?_
    rw [← Sieve.pullback_comp]
    exact hS hg

Premises used: CategoryTheory.Coverage.Saturate.top, CategoryTheory.Coverage.Saturate.of, CategoryTheory.Sieve.pullback_comp, CategoryTheory.Coverage.Saturate.transitive
-- 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
mp : K.Saturate X S → K.Saturate X S
mpr : K.Saturate X S → K.Saturate X S
⊢ K.Saturate X S ↔ K.Saturate X S

Tactic:
constructor
-- 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
hS : K.Saturate X S
mp : ∀ (X : C), ∀ S ∈ K.coverings X, K.Saturate X (Sieve.generate S)
mp₁ : ∀ (X : C), K.Saturate X ⊤
mp₂ :
  ∀ (X : C) (R S : Sieve.{v_1, u_1} X),
    K.Saturate X R →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)) →
        K.Saturate X R → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)) → K.Saturate X S
⊢ K.Saturate X S

Tactic:
induction hS
-- 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
X_1 : C
S_1 : Presieve.{v_1, u_1} X_1
hS : S_1 ∈ K.coverings X_1
⊢ K.Saturate X_1 (Sieve.generate S_1)

Tactic:
grind [Precoverage.Saturate]

Premises used: CategoryTheory.Precoverage.Saturate
-- 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
X_1 : C
⊢ K.Saturate X_1 ⊤

Tactic:
grind [Precoverage.Saturate]

Premises used: CategoryTheory.Precoverage.Saturate
-- 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
X_1 : C
R S_1 : Sieve.{v_1, u_1} X_1
h : K.Saturate X_1 R
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X_1⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S_1)
a_ih : K.Saturate X_1 R
a_ih_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X_1⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S_1)
⊢ K.Saturate X_1 S_1

Tactic:
grind [Precoverage.Saturate]

Premises used: CategoryTheory.Precoverage.Saturate
-- 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
hS : K.Saturate X S
mpr : ∀ (X : C), ∀ S ∈ K.coverings X, K.Saturate X (Sieve.generate S)
mpr₁ : ∀ (X : C), K.Saturate X ⊤
mpr₂ :
  ∀ (X : C) (S : Sieve.{v_1, u_1} X),
    K.Saturate X S → ∀ (Y : C) (f : Y ⟶ X), K.Saturate X S → K.Saturate Y (Sieve.pullback f S)
mpr₃ :
  ∀ (X : C) (S R : Sieve.{v_1, u_1} X),
    K.Saturate X S →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f R)) →
        K.Saturate X S → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f R)) → K.Saturate X R
⊢ K.Saturate X S

Tactic:
induction hS
-- 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
X_1 : C
S_1 : Presieve.{v_1, u_1} X_1
hS : S_1 ∈ K.coverings X_1
⊢ K.Saturate X_1 (Sieve.generate S_1)

Tactic:
grind [Saturate]

Premises used: CategoryTheory.Coverage.Saturate
-- 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
X_1 : C
⊢ K.Saturate X_1 ⊤

Tactic:
grind [Saturate]

Premises used: CategoryTheory.Coverage.Saturate
-- 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
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
h : K.Saturate X_1 S_1
Y : C
f : Y ⟶ X_1
a_ih : K.Saturate X_1 S_1
⊢ K.Saturate Y (Sieve.pullback f S_1)

Tactic:
grind [Saturate]

Premises used: CategoryTheory.Coverage.Saturate
-- 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
X_1 : C
S_1 R : Sieve.{v_1, u_1} X_1
h : K.Saturate X_1 S_1
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X_1⦄, S_1.arrows f → K.Saturate Y (Sieve.pullback f R)
a_ih : K.Saturate X_1 S_1
a_ih_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X_1⦄, S_1.arrows f → K.Saturate Y (Sieve.pullback f R)
⊢ K.Saturate X_1 R

Tactic:
grind [Saturate]

Premises used: CategoryTheory.Coverage.Saturate
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.45260
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.45260} D
K : Coverage.{v_1, u_1} C
h : ∀ (x : C) (x_1 : Sieve.{v_1, u_1} x), x_1 ∈ K.toGrothendieck.sieves x ↔ x_1 ∈ setOf (K.Saturate x)
⊢ K.toGrothendieck.sieves = fun (X : C) ↦ setOf (K.Saturate X)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.45260
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.45260} D
K : Coverage.{v_1, u_1} C
x : C
x_1 : Sieve.{v_1, u_1} x
⊢ x_1 ∈ K.toGrothendieck.sieves x ↔ x_1 ∈ setOf (K.Saturate x)

Tactic:
K.saturate_iff_saturate_toPrecoverage.symm

Premises used: CategoryTheory.Coverage.saturate_iff_saturate_toPrecoverage, Set.Mem, setOf, Iff.symm
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.45260
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.45260} D
K : Coverage.{v_1, u_1} C
x : C
x_1 : Sieve.{v_1, u_1} x
⊢ x_1 ∈ K.toGrothendieck.sieves x ↔ x_1 ∈ setOf (K.Saturate x)

Tactic:
exact K.saturate_iff_saturate_toPrecoverage.symm

Premises used: CategoryTheory.Coverage.saturate_iff_saturate_toPrecoverage, Iff.symm
-- 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
⊢ S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X ↔ K.Saturate X S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
mp : K.toGrothendieck ≤ J → K ≤ J.toCoverage
mpr : K ≤ J.toCoverage → K.toGrothendieck ≤ J
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toCoverage

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K.toGrothendieck ≤ J
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
⊢ S ∈ J.toCoverage.coverings X

Tactic:
H _ <| Saturate.of _ _ hS

Premises used: Set.Mem, setOf, CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K.toGrothendieck ≤ J
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
⊢ S ∈ J.toCoverage.coverings X

Tactic:
exact H _ <| Saturate.of _ _ hS

Premises used: CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K ≤ J.toCoverage
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
⊢ Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
H _ hS

Premises used: Set.Mem, setOf
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K ≤ J.toCoverage
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
⊢ Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
exact H _ hS
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K ≤ J.toCoverage
X : C
S : Sieve.{v_1, u_1} X
X_1 : C
⊢ ⊤ ∈ (J : (a : C) → Set (Sieve a)) X_1

Tactic:
apply J.top_mem

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K ≤ J.toCoverage
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : K.Saturate X R
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : R ∈ (J : (a : C) → Set (Sieve a)) X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.transitive H1 _ H2

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K ≤ J.toCoverage
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : K.Saturate X R
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : R ∈ (J : (a : C) → Set (Sieve a)) X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
exact J.transitive H1 _ H2

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K ≤ J.toCoverage
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
mpr : ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
mpr₁ : ∀ (X : C), ⊤ ∈ (J : (a : C) → Set (Sieve a)) X
mpr₂ :
  ∀ (X : C) (R S : Sieve.{v_1, u_1} X),
    K.Saturate X R →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)) →
        ∀ (H1 : R ∈ (J : (a : C) → Set (Sieve a)) X)
          (H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y),
          S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
induction hS with
      | of X S hS => exact H _ hS
      | top => apply J.top_mem
      | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
J : GrothendieckTopology.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
rw : Sieve.generate S.arrows ∈ (J.toCoverage.toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J.toCoverage.toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
rw [← Sieve.generate_sieve S]

Premises used: CategoryTheory.Sieve.generate_sieve
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
J : GrothendieckTopology.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
hS₁ : S.arrows ∈ J.toCoverage.coverings X
⊢ Sieve.generate S.arrows ∈ (J.toCoverage.toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
apply Saturate.of

Premises used: CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
J : GrothendieckTopology.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
hS₁ hS₂ hS₃ hS₄ : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.generate S.arrows ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
rwa [Sieve.generate_sieve S]

Premises used: CategoryTheory.Sieve.generate_sieve
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
a : K.toGrothendieck ≤ sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage}
a₁ : sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} ≤ K.toGrothendieck
⊢ K.toGrothendieck = sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
a :
  ∀ (b : GrothendieckTopology.{v_1, u_1} C),
    Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
        {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} b →
      K.toGrothendieck ≤ b
⊢ K.toGrothendieck ≤ sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage}

Tactic:
apply le_sInf

Premises used: le_sInf
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
hJ :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} J
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
a : S ∈ K.coverings X
⊢ Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
apply hJ
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
hJ :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} J
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
⊢ S ∈ K.coverings X

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
hJ :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} J
X : C
S : Sieve.{v_1, u_1} X
X_1 : C
⊢ ⊤ ∈ (J : (a : C) → Set (Sieve a)) X_1

Tactic:
apply J.top_mem

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
hJ :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} J
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : K.Saturate X R
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : R ∈ (J : (a : C) → Set (Sieve a)) X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.transitive H1 _ H2

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
hJ :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} J
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : K.Saturate X R
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : R ∈ (J : (a : C) → Set (Sieve a)) X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
exact J.transitive H1 _ H2

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
hJ :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} J
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
a : ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
a₁ : ∀ (X : C), ⊤ ∈ (J : (a : C) → Set (Sieve a)) X
a₂ :
  ∀ (X : C) (R S : Sieve.{v_1, u_1} X),
    K.Saturate X R →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)) →
        ∀ (H1 : R ∈ (J : (a : C) → Set (Sieve a)) X)
          (H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y),
          S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
induction hS with
    | of X S hS => apply hJ; assumption
    | top => apply J.top_mem
    | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.Coverage
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
a :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} K.toGrothendieck
⊢ sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} ≤ K.toGrothendieck

Tactic:
apply sInf_le

Premises used: sInf_le
-- 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 : Presieve.{v_1, u_1} X
hS : S ∈ K.coverings X
⊢ S ∈ K.toGrothendieck.toCoverage.coverings X

Tactic:
apply Saturate.of _ _ hS

Premises used: CategoryTheory.Coverage.Saturate.of
-- 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
inl :
  ∀ (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
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
obtain ⟨T, hT⟩ := x.pullback f S hx

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
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:
⟨T, Or.inl hT.1, hT.2⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Or.inl