awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
    (∀ (x : ↥S), ∃ (i : ι), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(X i)) ⇑(f i)) x) ∧ ∀ (i : ι), P (f i)
have simp_rw : Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
  Presieve.ofArrows X f ∈ (Precoverage.comap forget Types.jointlySurjectivePrecoverage).coverings S ∧ ∀ (i : ι), P (f i)
Tactic: simp_rw [← Scheme.forget_map', ← Scheme.forget_obj,
    ← Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ Presieve.singleton f ∈ (precoverage P).coverings S ↔ Function.Surjective (α := ↥X) (β := ↥S) ⇑f ∧ P f
have rw : ((∀ (x : ↥S), ∃ (i : PUnit.{1}), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) x) ∧ ∀ (i : PUnit.{1}), P f) ↔
  Function.Surjective (α := ↥X) (β := ↥S) ⇑f ∧ P f
Tactic: rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ofArrows_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ precoverage P ≤ precoverage Q
have grw : jointlySurjectivePrecoverage ⊓ P.precoverage ≤ precoverage Q
Tactic: grw [precoverage, precoverage, MorphismProperty.precoverage_monotone h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P Q : MorphismProperty Scheme
h : P ≤ Q
grw : jointlySurjectivePrecoverage ⊓ P.precoverage ≤ precoverage Q
⊢ precoverage P ≤ precoverage Q
have grw₁ : jointlySurjectivePrecoverage ⊓ P.precoverage ≤ jointlySurjectivePrecoverage ⊓ Q.precoverage
Tactic: grw [precoverage, precoverage, MorphismProperty.precoverage_monotone h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P Q : MorphismProperty Scheme
h : P ≤ Q
grw : jointlySurjectivePrecoverage ⊓ P.precoverage ≤ precoverage Q
grw₁ : jointlySurjectivePrecoverage ⊓ P.precoverage ≤ jointlySurjectivePrecoverage ⊓ Q.precoverage
⊢ precoverage P ≤ precoverage Q
have grw₂ : jointlySurjectivePrecoverage ⊓ Q.precoverage ≤ jointlySurjectivePrecoverage ⊓ Q.precoverage
Tactic: grw [precoverage, precoverage, MorphismProperty.precoverage_monotone h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P_1 P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
inst_1 : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ (precoverage P).coverings S
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows T p₁ ∈ (precoverage P).coverings Y
have rw : ∀ (hf : (∀ (x : ↥S), ∃ (i : ι), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(X i)) ⇑(f i)) x) ∧ ∀ (i : ι), P (f i))
  (Y : Scheme.{u}) (g : Y ⟶ S) (T : ι → Scheme.{u}) (p₁ : (i : ι) → T i ⟶ Y) (p₂ : (i : ι) → T i ⟶ X i)
  (H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)),
  (∀ (x : ↥Y), ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x) ∧ ∀ (i : ι), P (p₁ i)
Tactic: rw [ofArrows_mem_precoverage_iff] at hf ⊢
Cleared hypotheses: hf, Y, g, T, p₁, p₂, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P_1 P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
inst_1 : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ (i : ι), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(X i)) ⇑(f i)) x) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ (∀ (x : ↥Y), ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x) ∧ ∀ (i : ι), P (p₁ i)
have refine : ∀ (x : ↥Y), ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x
Tactic: refine ⟨fun x ↦ ?_, fun i ↦ P.of_isPullback (H i).flip (hf.2 i)⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P_1 P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
inst_1 : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ (i : ι), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(X i)) ⇑(f i)) x) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : ↥Y
⊢ ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x
have obtain : ∀ (i : ι) (y : ↥(X i)) (hy : Eq (α := ↥S) ((f i) y : ↥S) (g x : ↥S)),
  ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x
Tactic: obtain ⟨i, y, hy⟩ := hf.1 (g x)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (hypothesis)
Goal:
P_1 P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
inst_1 : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ (i : ι), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(X i)) ⇑(f i)) x) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : ↥Y
i : ι
y : ↥(X i)
hy : Eq (α := ↥S) ((f i) y : ↥S) (g x : ↥S)
⊢ ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x
have this : HasPullback g (f i)
Tactic: have := (H i).hasPullback
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P_1 P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
inst_1 : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ (i : ι), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(X i)) ⇑(f i)) x) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : ↥Y
i : ι
y : ↥(X i)
hy : Eq (α := ↥S) ((f i) y : ↥S) (g x : ↥S)
this : HasPullback g (f i)
⊢ ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x
have obtain : ∀ (w : ↥(pullback g (f i))) (hw : (pullback.fst g (f i)) w = x),
  ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x
Tactic: obtain ⟨w, hw⟩ := IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop (hf.2 i)
      (f := g) x y hy.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P_1 P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
inst_1 : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ (i : ι), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(X i)) ⇑(f i)) x) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : ↥Y
i : ι
y : ↥(X i)
hy : Eq (α := ↥S) ((f i) y : ↥S) (g x : ↥S)
this : HasPullback g (f i)
w : ↥(pullback g (f i))
hw : (pullback.fst g (f i)) w = x
⊢ ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x
have h : (p₁ i) ((Iso.inv sorry.isoPullback) w : ↥(T i)) = x
Tactic: use i, (H i).isoPullback.inv w
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Pretopology (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ ⊥ ∈ (grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X
have rw : Sieve.generate ⊥ ∈ (grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X
Tactic: rw [← Sieve.generate_bot]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Pretopology (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
S : Sieve X
⊢ S ∈ (grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X ↔
    ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
have simp_rw : (∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows) ↔
  ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
Tactic: simp_rw [grothendieckTopology, Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Pretopology (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
S : Sieve X
⊢ (∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows) ↔
    ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
have refine : (∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows) →
  ∀ (R : Presieve X) (hR : R ∈ (precoverage P).coverings X) (hle : R ≤ S.arrows),
    ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
Tactic: refine ⟨fun ⟨R, hR, hle⟩ ↦ ?_, fun ⟨𝒰, hle⟩ ↦ ⟨.ofArrows 𝒰.X 𝒰.f, 𝒰.mem_pretopology, hle⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Pretopology (hypothesis)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
S : Sieve X
h : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
R : Presieve X
hR : R ∈ (precoverage P).coverings X
hle : R ≤ S.arrows
⊢ ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
have hR₁ : ∃ (𝒰 : (precoverage P).ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: rw [Precoverage.mem_iff_exists_zeroHypercover] at hR
Cleared hypotheses: hR, hle
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Pretopology (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
S : Sieve X
h : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
R : Presieve X
hR : ∃ (𝒰 : (precoverage P).ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
hle : R ≤ S.arrows
⊢ ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
have obtain : ∀ (𝒰 : Cover (precoverage P) X) (hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows),
  ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
Tactic: obtain ⟨(𝒰 : Scheme.Cover _ _), rfl⟩ := hR
Cleared hypotheses: R, hR, hle
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Pretopology (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
S : Sieve X
h : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
𝒰 : Cover (precoverage P) X
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
⊢ ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
have w : Cover (precoverage P) X
Tactic: use 𝒰.ulift, le_trans (fun Y g ⟨i⟩ ↦ .mk _) hle
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Pretopology (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
S : Sieve X
h : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
𝒰 : Cover (precoverage P) X
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
w : Cover (precoverage P) X
⊢ ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
have h : Presieve.ofArrows 𝒰.ulift (P := P).X 𝒰.ulift (P := P).f ≤ S.arrows
Tactic: use 𝒰.ulift, le_trans (fun Y g ⟨i⟩ ↦ .mk _) hle
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Pretopology (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
⊢ grothendieckTopology P = (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck
have rw : Pretopology.toGrothendieck (Precoverage.toPretopology Scheme (precoverage P)) =
  (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck
Tactic: rw [grothendieckTopology, ← Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Proetale (goal)
Goal:
⊢ etalePrecoverage ≤ proetalePrecoverage
have rw : precoverage @Etale ≤ qcPrecoverage ∧ precoverage @Etale ≤ precoverage @WeaklyEtale
Tactic: rw [proetalePrecoverage, propQCPrecoverage, etalePrecoverage, le_inf_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Proetale (goal)
Goal:
⊢ precoverage @Etale ≤ qcPrecoverage ∧ precoverage @Etale ≤ precoverage @WeaklyEtale
have refine : precoverage @Etale ≤ precoverage @WeaklyEtale
Tactic: refine ⟨precoverage_le_qcPrecoverage_of_isOpenMap fun X Y f hf ↦ f.isOpenMap, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Proetale (goal)
Goal:
⊢ precoverage @Etale ≤ precoverage @WeaklyEtale
have h : @Etale ≤ @WeaklyEtale
Tactic: apply precoverage_mono
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Proetale (goal)
Goal:
S : Scheme
⊢ (ProEt.forget S).LocallyCoverDense (proetaleTopology.over S)
have H : proetalePrecoverage ≤ MorphismProperty.precoverage @WeaklyEtale
Tactic: apply MorphismProperty.locallyCoverDense_forget_of_le
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Proetale (goal)
Goal:
S : Scheme
⊢ topology S = (ProEt.forget S).inducedTopology (proetaleTopology.over S)
have H : proetalePrecoverage ≤ MorphismProperty.precoverage @WeaklyEtale
Tactic: apply MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Proetale (goal)
Goal:
S : Scheme
⊢ (ProEt.forget S).IsContinuous (topology S) (proetaleTopology.over S)
have rw : (ProEt.forget S).IsContinuous ((ProEt.forget S).inducedTopology (proetaleTopology.over S)) (proetaleTopology.over S)
Tactic: rw [topology_eq_inducedTopology]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Proetale (goal)
Goal:
S : Scheme
⊢ (ProEt.forget S).IsContinuous ((ProEt.forget S).inducedTopology (proetaleTopology.over S)) (proetaleTopology.over S)
have refine : CoverPreserving ((ProEt.forget S).inducedTopology (proetaleTopology.over S)) (proetaleTopology.over S) (ProEt.forget S)
Tactic: refine Functor.isContinuous_of_coverPreserving (compatiblePreservingOfFlat _ _) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Proetale (goal)
Goal:
S : Scheme
inst : IsEmpty.{u + 1} ↥S
⊢ topology S = ⊤
have rw : ∀ (X : S.ProEt), ⊥ ∈ (topology S : (a : S.ProEt) → Set (Sieve a)) X
Tactic: rw [GrothendieckTopology.eq_top_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Proetale (hypothesis)
Goal:
S : Scheme
inst : IsEmpty.{u + 1} ↥S
X : S.ProEt
⊢ ⊥ ∈ (topology S : (a : S.ProEt) → Set (Sieve a)) X
have this : IsEmpty.{u + 1} ↥X.toComma (P := @WeaklyEtale) (Q := ⊤) (W := ⊤).left
Tactic: have : IsEmpty X.left := X.hom.base.1.1.isEmpty (β := S)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S : Scheme
E : PreZeroHypercover.{w, u, u + 1} S
⊢ E.presieve₀ ∈ qcPrecoverage.coverings S ↔ QuasiCompactCover E
have rw : qcCoverFamily.property E.shrink ↔ QuasiCompactCover E
Tactic: rw [← PreZeroHypercover.presieve₀_shrink, Scheme.qcPrecoverage,
    E.shrink.presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S : Scheme
⊢ qcPrecoverage.IsStableUnderBaseChange
have refine_1 : ∀ {X : Scheme.{u_1}}, ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) qcCoverFamily.property
Tactic: refine .of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S : Scheme
refine_1 :
  ∀ {X : Scheme.{u_1}}, ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) qcCoverFamily.property
⊢ qcPrecoverage.IsStableUnderBaseChange
have refine_2 : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
  qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)
Tactic: refine .of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (hypothesis)
Goal:
S : Scheme
X Y : Scheme
f : X ⟶ Y
E : PreZeroHypercover Y
h : ∀ (i : E.I₀), HasPullback f (E.f i)
hE : qcCoverFamily.property E
⊢ qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)
have hE₁ : QuasiCompactCover E
Tactic: simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE ⊢
Cleared hypotheses: hE
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S : Scheme
⊢ qcPrecoverage.IsStableUnderComposition
have refine : ∀ {X : Scheme.{u_1}} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i))
  (hE : qcCoverFamily.property E) (hF : ∀ (i : E.I₀), qcCoverFamily.property (F i)), qcCoverFamily.property (E.bind F)
Tactic: refine .of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (hypothesis)
Goal:
S : Scheme
X : Scheme
E : PreZeroHypercover X
F : (i : E.I₀) → PreZeroHypercover (E.X i)
hE : qcCoverFamily.property E
hF : ∀ (i : E.I₀), qcCoverFamily.property (F i)
⊢ qcCoverFamily.property (E.bind F)
have hE₁ : QuasiCompactCover E
Tactic: simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢
Cleared hypotheses: hE, hF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (hypothesis)
Goal:
S : Scheme
X : Scheme
E : PreZeroHypercover X
F : (i : E.I₀) → PreZeroHypercover (E.X i)
hE : qcCoverFamily.property E
hF : ∀ (i : E.I₀), qcCoverFamily.property (F i)
hE₁ : QuasiCompactCover E
⊢ qcCoverFamily.property (E.bind F)
have hF₁ : ∀ (i : E.I₀), QuasiCompactCover (F i)
Tactic: simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢
Cleared hypotheses: hE, hF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S : Scheme
⊢ qcPrecoverage.IsStableUnderSup
have refine : ∀ {X : Scheme.{u_1}} (E F : PreZeroHypercover X) (hE : qcCoverFamily.property E) (hF : qcCoverFamily.property F),
  qcCoverFamily.property (E.sum F)
Tactic: refine .of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (hypothesis)
Goal:
S : Scheme
X : Scheme
E F : PreZeroHypercover X
hE : qcCoverFamily.property E
hF : qcCoverFamily.property F
⊢ qcCoverFamily.property (E.sum F)
have hE₁ : QuasiCompactCover E
Tactic: simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢
Cleared hypotheses: hE, hF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (hypothesis)
Goal:
S : Scheme
X : Scheme
E F : PreZeroHypercover X
hE : qcCoverFamily.property E
hF : qcCoverFamily.property F
hE₁ : QuasiCompactCover E
⊢ qcCoverFamily.property (E.sum F)
have hF₁ : QuasiCompactCover F
Tactic: simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢
Cleared hypotheses: hE, hF
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ ⊥ ∈ qcPrecoverage.coverings X
have rw : QuasiCompactCover (PreZeroHypercover.empty X)
Tactic: rw [← PreZeroHypercover.presieve₀_empty.{0}, presieve₀_mem_qcPrecoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
hP : P ≤ fun (x x_1 : Scheme.{u}) (f : x ⟶ x_1) ↦ IsOpenMap (X := ↥x) (Y := ↥x_1) ⇑f
⊢ precoverage P ≤ qcPrecoverage
have refine : ∀ (X : Scheme.{u}) (E : (precoverage P).ZeroHypercover X), E.presieve₀ ∈ qcPrecoverage.coverings X
Tactic: refine Precoverage.le_of_zeroHypercover fun X E ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
hP : P ≤ fun (x x_1 : Scheme.{u}) (f : x ⟶ x_1) ↦ IsOpenMap (X := ↥x) (Y := ↥x_1) ⇑f
X : Scheme
E : (precoverage P).ZeroHypercover X
⊢ E.presieve₀ ∈ qcPrecoverage.coverings X
have rw : QuasiCompactCover E.toPreZeroHypercover
Tactic: rw [presieve₀_mem_qcPrecoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Surjective f
inst_1 : QuasiCompact f
E : Cover (precoverage ⊤) Y := cover (P := ⊤) f trivial
⊢ Presieve.singleton f ∈ qcPrecoverage.coverings Y
have rw : ∃ (E : PreZeroHypercover Y), qcCoverFamily.property E ∧ Presieve.singleton f = E.presieve₀
Tactic: rw [qcPrecoverage, PreZeroHypercoverFamily.mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Surjective f
inst_1 : QuasiCompact f
E : Cover (precoverage ⊤) Y := cover (P := ⊤) f trivial
⊢ ∃ (E : PreZeroHypercover Y), qcCoverFamily.property E ∧ Presieve.singleton f = E.presieve₀
have refine : qcCoverFamily.property (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage ⊤) (cover (P := ⊤) f trivial))
Tactic: refine ⟨(f.cover (P := ⊤) trivial).toPreZeroHypercover, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ qcPrecoverage ⊓ precoverage P ≤ qcPrecoverage ⊓ precoverage Q
have h₂ : precoverage P ≤ precoverage Q
Tactic: gcongr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
⊢ zariskiPrecoverage ≤ propQCPrecoverage P
have rw : zariskiPrecoverage ≤ qcPrecoverage ∧ zariskiPrecoverage ≤ precoverage P
Tactic: rw [propQCPrecoverage, le_inf_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
⊢ zariskiPrecoverage ≤ qcPrecoverage ∧ zariskiPrecoverage ≤ precoverage P
have refine : ∀ (X Y : Scheme.{u}) (f : X ⟶ Y) (hf : IsOpenImmersion f), P f
Tactic: refine ⟨zariskiPrecoverage_le_qcPrecoverage, precoverage_mono fun X Y f hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{u_1, u} (propQCPrecoverage P) S
⊢ QuasiCompactCover 𝒰.toPreZeroHypercover
have rw : PreZeroHypercover.presieve₀.{u_1, u, u + 1} 𝒰.toPreZeroHypercover ∈ qcPrecoverage.coverings S
Tactic: rw [← Scheme.presieve₀_mem_qcPrecoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{u_1, u} (propQCPrecoverage P) S
⊢ QuasiCompactCover 𝒰.forgetQc (P := P).toPreZeroHypercover
have dsimp : QuasiCompactCover 𝒰.toPreZeroHypercover
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).presieve₀ ∈ (precoverage P).coverings S
have rw : (∀ (x : ↥S),
    ∃ (i : (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).I₀),
      Membership.mem (γ := Set ↥S)
        (Set.range (ι := ↥((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X i))
          ⇑((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f i))
        x) ∧
  ∀ (i : (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).I₀),
    P ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.QuasiCompact (goal)
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ (∀ (x : ↥S),
      ∃ (i : (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).I₀),
        Membership.mem (γ := Set ↥S)
          (Set.range (ι := ↥((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X i))
            ⇑((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f i))
          x) ∧
    ∀ (i : (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).I₀),
      P ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f i)
have refine : ∀ (i : (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).I₀),
  P ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f i)
Tactic: refine ⟨fun x ↦ ⟨.inl x, 𝒰.covers _⟩, fun i ↦ ?_⟩