awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
⊢ S.arrows u
have h : ∀ (W : C) (g : Z ⟶ W) (w : W ⟶ X) (hw : R' w) (hg : S' sorry g), S.arrows (g ≫ w)
Tactic: obtain ⟨W, g, w, hw, hg, rfl⟩ := hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
⊢ ∃ R ∈ J.coverings T, R ≤ S.arrows
have 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
⊢ ∃ R ∈ J.coverings T, R ≤ S.arrows
have h₂ : ∀ (X : C), ∃ R ∈ J.coverings X, R ≤ Sieve.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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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 ⊤
⊢ ∃ R ∈ J.coverings T, R ≤ S.arrows
have 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
have h : Sieve.generate R ≤ S
Tactic: refine Coverage.saturate_of_superset _ ?_ (.of _ _ hR)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (hypothesis)
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
⊢ ∃ T ∈ J.coverings Y, T.FactorsThruAlong S f
have this : S.HasPullbacks f
Tactic: have : S.HasPullbacks f := J.hasPullbacks_of_mem _ hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Coverage.{v_1, u_1} C
⊢ J.toGrothendieck = J.toGrothendieck
have rw : J.toGrothendieck = J.toGrothendieck.copy (fun (X : C) ↦ setOf (J.Saturate X)) sorry
Tactic: rw [Coverage.toGrothendieck, GrothendieckTopology.copy_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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)) ⋯
⊢ J.toGrothendieck = J.toGrothendieck
have rw₁ : J.toGrothendieck = J.toGrothendieck
Tactic: rw [Coverage.toGrothendieck, GrothendieckTopology.copy_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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)
⊢ IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
have 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
Tactic: rw [← toGrothendieck_toPrecoverage, Precoverage.isSheaf_toGrothendieck_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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)
⊢ (∀ {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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
⊢ (∀ {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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
have 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
Tactic: obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
have mpr : T.FactorsThru (Sieve.pullback f (Sieve.generate S)).arrows
Tactic: apply Presieve.isSheafFor_of_factorsThru (S := T)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
have mpr₁ : IsSheafFor P T
Tactic: apply Presieve.isSheafFor_of_factorsThru (S := T)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
have 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
Tactic: apply Presieve.isSheafFor_of_factorsThru (S := T)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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 ⟶ Y), (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g
have 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
Tactic: obtain ⟨W, i, e, h1, h2⟩ := hT2 hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
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
h : (Sieve.pullback f (Sieve.generate S)).arrows g
⊢ ∃ (R : Presieve.{v_1, u_2} Z), IsSeparatedFor P R ∧ R.FactorsThruAlong T g
have mpr : ∀ (R : Presieve.{v_1, u_2} Z) (hR1 : R ∈ K.coverings Z) (hR2 : R.FactorsThruAlong T g),
  ∃ (R : Presieve.{v_1, u_2} Z), IsSeparatedFor P R ∧ R.FactorsThruAlong T g
Tactic: obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
⊢ IsSheaf (K ⊔ L).toGrothendieck P ↔ IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P
have refine : ∀ (h : IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P), IsSheaf (K ⊔ L).toGrothendieck P
Tactic: refine ⟨fun h ↦ ⟨Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_left) h,
      Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_right) h⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (hypothesis)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : Coverage.{v_1, u_2} C
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h : IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P
⊢ IsSheaf (K ⊔ L).toGrothendieck P
have h₁ : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
Tactic: rw [isSheaf_coverage, isSheaf_coverage] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : 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 : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
⊢ IsSheaf (K ⊔ L).toGrothendieck P
have rw : ∀ {X : C}, ∀ R ∈ (K ⊔ L).coverings X, IsSheafFor P R
Tactic: rw [isSheaf_coverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : 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 : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve.{v_1, u_2} X
hR : R ∈ (K ⊔ L).coverings X
⊢ IsSheafFor P R
have inl : ∀ (hR : R ∈ K.coverings X), IsSheafFor P R
Tactic: rcases hR with hR | hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
K L : 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 : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve.{v_1, u_2} X
hR : R ∈ (K ⊔ L).coverings X
inl : ∀ (hR : R ∈ K.coverings X), IsSheafFor P R
⊢ IsSheafFor P R
have inr : ∀ (hR : R ∈ L.coverings X), IsSheafFor P R
Tactic: rcases hR with hR | hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.HasPullbacks
inst_2 : J.IsStableUnderBaseChange
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
⊢ Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R
have rw : Presieve.IsSheaf J.toCoverage.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
Tactic: rw [← J.toCoverage_toPrecoverage, Coverage.toGrothendieck_toPrecoverage,
    Presieve.isSheaf_coverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.HasPullbacks
inst_2 : J.IsStableUnderBaseChange
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
rw : Presieve.IsSheaf J.toCoverage.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
⊢ Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R
have rw₁ : Presieve.IsSheaf J.toCoverage.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
Tactic: rw [← J.toCoverage_toPrecoverage, Coverage.toGrothendieck_toPrecoverage,
    Presieve.isSheaf_coverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.HasPullbacks
inst_2 : J.IsStableUnderBaseChange
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
rw : Presieve.IsSheaf J.toCoverage.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
rw₁ :
  Presieve.IsSheaf J.toCoverage.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
⊢ Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R
have rw₂ : (∀ {X : C}, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R) ↔
  ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
Tactic: rw [← J.toCoverage_toPrecoverage, Coverage.toGrothendieck_toPrecoverage,
    Presieve.isSheaf_coverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
⊢ Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
      Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
have rw : (∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R) ↔
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
Tactic: rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
⊢ (∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R) ↔
    ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
      Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
have refine : ∀
  (h :
    ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
      Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover))
  (X : C) (R : Presieve.{v_1, u_2} X) (hR : R ∈ J.coverings X), Presieve.IsSheafFor P R
Tactic: refine ⟨fun h X E ↦ h _ E.mem₀, fun h X R hR ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
R : Presieve.{v_1, u_2} X
hR : R ∈ J.coverings X
⊢ Presieve.IsSheafFor P R
have obtain : ∀ (E₀ : PreZeroHypercover X) (hR : E₀.presieve₀ ∈ J.coverings X), Presieve.IsSheafFor P E₀.presieve₀
Tactic: obtain ⟨E₀, rfl⟩ := R.exists_eq_preZeroHypercover
Cleared hypotheses: R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
⊢ Presieve.IsSheafFor P E₀.presieve₀
have rw : Presieve.IsSheafFor P (Sieve.generate E₀.presieve₀).arrows
Tactic: rw [Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
⊢ Presieve.IsSheafFor P (Sieve.generate E₀.presieve₀).arrows
have h₁ : (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.restrictIndexOfSmall.toPreZeroHypercover)).arrows ≤
  (Sieve.generate E₀.presieve₀).arrows
Tactic: apply Presieve.isSheafFor_subsieve
      (S := .generate <| (ZeroHypercover.restrictIndexOfSmall.{w} E).presieve₀)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
h₁ :
  (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.restrictIndexOfSmall.toPreZeroHypercover)).arrows ≤
    (Sieve.generate E₀.presieve₀).arrows
⊢ Presieve.IsSheafFor P (Sieve.generate E₀.presieve₀).arrows
have trans : ∀ ⦃Y : C⦄ (f : Y ⟶ X),
  Presieve.IsSheafFor P
    (Sieve.pullback f
        (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.restrictIndexOfSmall.toPreZeroHypercover))).arrows
Tactic: apply Presieve.isSheafFor_subsieve
      (S := .generate <| (ZeroHypercover.restrictIndexOfSmall.{w} E).presieve₀)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
J : Precoverage.{v_1, u_2} C
inst_1 : J.IsStableUnderBaseChange
inst_2 : J.HasPullbacks
inst_3 : J.Small
P : Functor.{v_1, u_1, u_2, u_1 + 1} Cᵒᵖ (Type u_1)
h :
  ∀ ⦃X : C⦄ (E : ZeroHypercover.{w, v_1, u_2} J X),
    Presieve.IsSheafFor P (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.toPreZeroHypercover)
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P
    (Sieve.pullback f
        (Sieve.generate (PreZeroHypercover.presieve₀.{w, v_1, u_2} E.restrictIndexOfSmall.toPreZeroHypercover))).arrows
have trans : Presieve.IsSheafFor P
  (PreZeroHypercover.presieve₀.{w, v_1, u_2} (ZeroHypercover.pullback₂ f E.restrictIndexOfSmall).toPreZeroHypercover)
Tactic: rw [← Sieve.pullbackArrows_comm, ← Presieve.isSheafFor_iff_generate,
      ← PreZeroHypercover.presieve₀_pullback₁, ← ZeroHypercover.pullback₂_toPreZeroHypercover]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
K : Coverage.{v_1, u_1} C
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
⊢ IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op))
have simp : (∀ (E : D) {X : C}, ∀ R ∈ K.coverings X, Presieve.IsSheafFor (P ⋙ Functor.obj coyoneda (Opposite.op E)) R) ↔
  ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, ∀ (E : Dᵒᵖ), Presieve.IsSheafFor (P ⋙ Functor.obj coyoneda E) R
Tactic: simp only [Presheaf.IsSheaf, Presieve.isSheaf_coverage, isLimit_iff_isSheafFor,
    ← Presieve.isSheafFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
hX : IsTerminal.{v, u} X
I : Type u_1
Y : I → C
⊢ J.CoversTop Y ↔ Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
have mp : J.CoversTop Y → Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
hX : IsTerminal.{v, u} X
I : Type u_1
Y : I → C
mp : J.CoversTop Y → Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
⊢ J.CoversTop Y ↔ Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
have mpr : Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X → J.CoversTop Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoversTop.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
hX : IsTerminal.{v, u} X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ (J : (a : C) → Set (Sieve a)) X
W : C
⊢ Sieve.ofObjects Y W ∈ (J : (a : C) → Set (Sieve a)) W
have apply : Sieve.pullback (hX.from W) (Sieve.ofObjects Y X) ≤ Sieve.ofObjects Y W
Tactic: apply J.superset_covering _ (J.pullback_stable (hX.from W) h)