awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
refine_1 :
  ∀ (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X) (hle : R ≤ S.arrows),
    ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
⊢ ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows

Tactic:
obtain ⟨R, hR, hle⟩ := h
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ R.HasPullbacks f

Tactic:
have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
⊢ ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows

Tactic:
⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩

Premises used: CategoryTheory.Presieve.pullbackArrows, CategoryTheory.Precoverage.pullbackArrows_mem, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
refine_1 : Presieve.pullbackArrows f R ≤ (Sieve.pullback f S).arrows
⊢ ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows

Tactic:
refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
refine_1 : Sieve.pullback f (Sieve.generate R) ≤ Sieve.pullback f S
⊢ Presieve.pullbackArrows f R ≤ (Sieve.pullback f S).arrows

Tactic:
rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]

Premises used: CategoryTheory.Sieve.pullbackArrows_comm, CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
refine_1 : Sieve.generate R ≤ S
⊢ Sieve.pullback f (Sieve.generate R) ≤ Sieve.pullback f S

Tactic:
apply Sieve.pullback_monotone

Premises used: CategoryTheory.Sieve.pullback_monotone
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
refine_1 refine_1₁ refine_1₂ refine_1₃ : R ≤ S.arrows
⊢ Sieve.generate R ≤ S

Tactic:
rwa [Sieve.generate_le_iff]

Premises used: CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleS : ∃ R ∈ J.coverings X, R ≤ S.arrows
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
refine_1 :
  ∀ (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X) (hle : R ≤ S.arrows), ∃ R ∈ J.coverings X, R ≤ T.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows

Tactic:
obtain ⟨R, hR, hle⟩ := hleS
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
rw [mem_iff_exists_zeroHypercover] at hR

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
hR₁ : ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ R ≤ S.arrows

Tactic:
rw [mem_iff_exists_zeroHypercover] at hR

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
R : Presieve.{u_1, u_2} X
hR : ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
hle : R ≤ S.arrows
refine_1 : ∀ (E : J.ZeroHypercover X) (hle : Presieve.ofArrows E.X E.f ≤ S.arrows), ∃ R ∈ J.coverings X, R ≤ T.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows

Tactic:
obtain ⟨E, rfl⟩ := hR

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
obtain :
  ∀ (R' : Presieve.{u_1, u_2} (E.X i))
    (hR' : Membership.mem (γ := Set (Presieve.{u_1, u_2} (E.X i))) (J.coverings (E.X i)) R')
    (hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows),
    ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows

Tactic:
obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
R' : Presieve.{u_1, u_2} (E.X i)
hR' : Membership.mem (γ := Set (Presieve.{u_1, u_2} (E.X i))) (J.coverings (E.X i)) R'
hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ (𝒰 : J.ZeroHypercover (E.X i)), R' = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
rw [mem_iff_exists_zeroHypercover] at hR'

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
R' : Presieve.{u_1, u_2} (E.X i)
hR' : Membership.mem (γ := Set (Presieve.{u_1, u_2} (E.X i))) (J.coverings (E.X i)) R'
hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows
hR'₁ : ∃ (𝒰 : J.ZeroHypercover (E.X i)), R' = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ R' ≤ (Sieve.pullback (E.f i) T).arrows

Tactic:
rw [mem_iff_exists_zeroHypercover] at hR'

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
R' : Presieve.{u_1, u_2} (E.X i)
hR' : ∃ (𝒰 : J.ZeroHypercover (E.X i)), R' = Presieve.ofArrows 𝒰.X 𝒰.f
hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows
obtain :
  ∀ (F : J.ZeroHypercover (E.X i)) (hle' : Presieve.ofArrows F.X F.f ≤ (Sieve.pullback (E.f i) T).arrows),
    ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows

Tactic:
obtain ⟨F, rfl⟩ := hR'

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
F : J.ZeroHypercover (E.X i)
hle' : Presieve.ofArrows F.X F.f ≤ (Sieve.pullback (E.f i) T).arrows
w : J.ZeroHypercover (E.X i)
h : F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows

Tactic:
use F
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
⊢ ∀ (i : E.I₀), ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows

Tactic:
replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
hleT : ∀ (i : E.I₀), ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
refine_1 :
  ∀ (F : (i : E.I₀) → J.ZeroHypercover (E.X i))
    (hle' : ∀ (i : E.I₀), (F i).presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows), ∃ R ∈ J.coverings X, R ≤ T.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows

Tactic:
choose F hle' using hleT
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
F : (i : E.I₀) → J.ZeroHypercover (E.X i)
hle' : ∀ (i : E.I₀), (F i).presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows

Tactic:
⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, And.intro, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Precoverage.ZeroHypercover.bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
F : (i : E.I₀) → J.ZeroHypercover (E.X i)
hle' : ∀ (i : E.I₀), (F i).presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
refine_1 : (E.bind F).presieve₀ ≤ T.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows

Tactic:
refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
F : (i : E.I₀) → J.ZeroHypercover (E.X i)
hle' : ∀ (i : E.I₀), (F i).presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
refine_1 : ∀ (i : (E.bind F).I₀), T.arrows ((E.bind F).f i)
⊢ (E.bind F).presieve₀ ≤ T.arrows

Tactic:
rw [Presieve.ofArrows_le_iff]

Premises used: CategoryTheory.Presieve.ofArrows_le_iff
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
F : (i : E.I₀) → J.ZeroHypercover (E.X i)
hle' : ∀ (i : E.I₀), (F i).presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
i : (E.bind F).I₀
⊢ T.arrows ((E.bind F).f i)

Tactic:
hle' _ _ _ ⟨i.snd⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sigma.snd
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
F : (i : E.I₀) → J.ZeroHypercover (E.X i)
hle' : ∀ (i : E.I₀), (F i).presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
i : (E.bind F).I₀
⊢ T.arrows ((E.bind F).f i)

Tactic:
exact hle' _ _ _ ⟨i.snd⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sigma.snd
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
refine_1 :
  ∀ (X : C) (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X), ∃ R_1 ∈ J.coverings X, R_1 ≤ (Sieve.generate R).arrows
refine_1₁ : ∀ (X : C), ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤
refine_1₂ :
  ∀ (X : C) (S : Sieve.{u_1, u_2} X) (hS : J.Saturate X S) (Y : C) (f : Y ⟶ X) (h : ∃ R ∈ J.coverings X, R ≤ S.arrows),
    ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
refine_1₃ :
  ∀ (X : C) (S T : Sieve.{u_1, u_2} X) (hS : J.Saturate X S)
    (hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T))
    (hleS : ∃ R ∈ J.coverings X, R ≤ S.arrows)
    (hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows),
    ∃ R ∈ J.coverings X, R ≤ T.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
induction hS with
    | of X R hR =>
      use R, hR
      exact Sieve.le_generate R
    | top X =>
      exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩
    | pullback X S hS Y f h =>
      obtain ⟨R, hR, hle⟩ := h
      have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
      refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
      rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]
      apply Sieve.pullback_monotone
      rwa [Sieve.generate_le_iff]
    | transitive X S T hS hT hleS hleT =>
      obtain ⟨R, hR, hle⟩ := hleS
      rw [mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
      choose F hle' using hleT
      refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
      rw [Presieve.ofArrows_le_iff]
      intro i
      exact hle' _ _ _ ⟨i.snd⟩

Premises used: CategoryTheory.Sieve.pullback_monotone, CategoryTheory.Presieve.ofArrows_le_iff, CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover, CategoryTheory.Sieve.pullbackArrows_comm, CategoryTheory.Sieve.generate_le_iff, rfl
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ Sieve.generate R ≤ S

Tactic:
rw [← Sieve.generate_le_iff] at hle

Premises used: CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : Sieve.generate R ≤ S
refine_2 : Sieve.generate R ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
apply GrothendieckTopology.superset_covering _ hle

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : Sieve.generate R ≤ S
⊢ Sieve.generate R ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
generate_mem_toGrothendieck hR

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : Sieve.generate R ≤ S
⊢ Sieve.generate R ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
exact generate_mem_toGrothendieck hR

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : Limits.HasPullbacks.{u_1, u_2} C
inst_4 : J.HasIsos
h :
  ∀ (x : C) (x_1 : Sieve.{u_1, u_2} x),
    x_1 ∈ (Pretopology.toGrothendieck (toPretopology C J) : (a : C) → Set (Sieve a)) x ↔
      x_1 ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) x
⊢ Pretopology.toGrothendieck (toPretopology C J) = J.toGrothendieck

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : Limits.HasPullbacks.{u_1, u_2} C
inst_4 : J.HasIsos
x : C
x_1 : Sieve.{u_1, u_2} x
⊢ x_1 ∈ (Pretopology.toGrothendieck (toPretopology C J) : (a : C) → Set (Sieve a)) x ↔
    x_1 ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) x

Tactic:
J.mem_toGrothendieck_iff_of_isStableUnderComposition.symm

Premises used: Set.Mem, setOf, CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, Iff.symm