awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ CoverPreserving ((ProEt.forget S).inducedTopology (proetaleTopology.over S)) (proetaleTopology.over S)
    (ProEt.forget S)

Tactic:
Functor.inducedTopology_coverPreserving _ _

Premises used: CategoryTheory.Functor.inducedTopology_coverPreserving
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ CoverPreserving ((ProEt.forget S).inducedTopology (proetaleTopology.over S)) (proetaleTopology.over S)
    (ProEt.forget S)

Tactic:
exact Functor.inducedTopology_coverPreserving _ _

Premises used: CategoryTheory.Functor.inducedTopology_coverPreserving
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ (ProEt.forget S ⋙ CategoryTheory.Over.forget S).IsContinuous (topology S) proetaleTopology

Tactic:
Functor.isContinuous_comp _ _ _ (proetaleTopology.over S) _

Premises used: CategoryTheory.Functor.isContinuous_comp, CategoryTheory.GrothendieckTopology.over, AlgebraicGeometry.Scheme.proetaleTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ (topology S).Subcanonical

Tactic:
GrothendieckTopology.subcanonical_of_full_of_faithful (ProEt.forget S) _ (proetaleTopology.over S)

Premises used: CategoryTheory.GrothendieckTopology.subcanonical_of_full_of_faithful, AlgebraicGeometry.Scheme.ProEt.forget, CategoryTheory.GrothendieckTopology.over, AlgebraicGeometry.Scheme.proetaleTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
X : S.ProEt
inst : IsEmpty.{u + 1} ↥X.toComma (P := @WeaklyEtale) (Q := ⊤) (W := ⊤).left
⊢ ⊥ ∈ (topology S : (a : S.ProEt) → Set (Sieve a)) X

Tactic:
simp [topology_eq_inducedTopology, GrothendieckTopology.mem_over_iff,
    proetaleTopology_eq_propQCTopology, bot_mem_propQCTopology]

Premises used: CategoryTheory.GrothendieckTopology.mem_over_iff, AlgebraicGeometry.Scheme.ProEt.topology_eq_inducedTopology, AlgebraicGeometry.Scheme.proetaleTopology_eq_propQCTopology, AlgebraicGeometry.Scheme.bot_mem_propQCTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
inst : IsEmpty.{u + 1} ↥S
rw : ∀ (X : S.ProEt), ⊥ ∈ (topology S : (a : S.ProEt) → Set (Sieve a)) X
⊢ topology S = ⊤

Tactic:
rw [GrothendieckTopology.eq_top_iff]

Premises used: CategoryTheory.GrothendieckTopology.eq_top_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
inst : IsEmpty.{u + 1} ↥S
X : S.ProEt
⊢ IsEmpty.{u + 1} ↥X.toComma (P := @WeaklyEtale) (Q := ⊤) (W := ⊤).left

Tactic:
have : IsEmpty X.left := X.hom.base.1.1.isEmpty (β := S)
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
inst : IsEmpty.{u + 1} ↥S
X : S.ProEt
this : IsEmpty.{u + 1} ↥X.toComma (P := @WeaklyEtale) (Q := ⊤) (W := ⊤).left
⊢ ⊥ ∈ (topology S : (a : S.ProEt) → Set (Sieve a)) X

Tactic:
bot_mem_topology _

Premises used: AlgebraicGeometry.Scheme.ProEt.bot_mem_topology
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
inst : IsEmpty.{u + 1} ↥S
X : S.ProEt
this : IsEmpty.{u + 1} ↥X.toComma (P := @WeaklyEtale) (Q := ⊤) (W := ⊤).left
⊢ ⊥ ∈ (topology S : (a : S.ProEt) → Set (Sieve a)) X

Tactic:
exact bot_mem_topology _

Premises used: AlgebraicGeometry.Scheme.ProEt.bot_mem_topology
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
E : PreZeroHypercover.{w, u, u + 1} S
⊢ QuasiCompactCover E.shrink ↔ QuasiCompactCover E

Tactic:
⟨fun _ ↦ .of_hom E.fromShrink, fun _ ↦ .of_hom E.toShrink⟩

Premises used: CategoryTheory.PreZeroHypercover.toShrink, AlgebraicGeometry.QuasiCompactCover.of_hom, Iff.intro, CategoryTheory.PreZeroHypercover.fromShrink
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
E : PreZeroHypercover.{w, u, u + 1} S
rw : qcCoverFamily.property E.shrink ↔ QuasiCompactCover E
⊢ E.presieve₀ ∈ qcPrecoverage.coverings S ↔ QuasiCompactCover E

Tactic:
rw [← PreZeroHypercover.presieve₀_shrink, Scheme.qcPrecoverage,
    E.shrink.presieve₀_mem_precoverage_iff]

Premises used: CategoryTheory.PreZeroHypercover.presieve₀_shrink, AlgebraicGeometry.Scheme.qcPrecoverage, CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
E : PreZeroHypercover.{w, u, u + 1} S
⊢ qcCoverFamily.property E.shrink ↔ QuasiCompactCover E

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
X Y : Scheme
f : X ⟶ Y
hf : IsIso f
⊢ QuasiCompactCover (PreZeroHypercover.singleton f)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
⊢ qcPrecoverage.IsStableUnderBaseChange

Tactic:
.of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms ?_ ?_

Premises used: CategoryTheory.Precoverage.IsStableUnderBaseChange.of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms, AlgebraicGeometry.Scheme.qcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
refine_1 :
  ∀ {X : Scheme.{u_1}}, ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) qcCoverFamily.property
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)
⊢ qcPrecoverage.IsStableUnderBaseChange

Tactic:
refine .of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms ?_ ?_
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
X : Scheme
⊢ ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) qcCoverFamily.property

Tactic:
X.isClosedUnderIsomorphisms_quasiCompactCover

Premises used: AlgebraicGeometry.Scheme.isClosedUnderIsomorphisms_quasiCompactCover, AlgebraicGeometry.Scheme.quasiCompactCover
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
X : Scheme
⊢ ObjectProperty.IsClosedUnderIsomorphisms (C := PreZeroHypercover X) qcCoverFamily.property

Tactic:
exact X.isClosedUnderIsomorphisms_quasiCompactCover

Premises used: AlgebraicGeometry.Scheme.isClosedUnderIsomorphisms_quasiCompactCover
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
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
⊢ QuasiCompactCover E

Tactic:
simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE ⊢

Premises used: AlgebraicGeometry.Scheme.quasiCompactCover_iff, AlgebraicGeometry.Scheme.qcCoverFamily_property
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
X Y : Scheme
f : X ⟶ Y
E : PreZeroHypercover Y
h : ∀ (i : E.I₀), HasPullback f (E.f i)
hE : QuasiCompactCover E
⊢ QuasiCompactCover (PreZeroHypercover.pullback₁ f E)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
⊢ qcPrecoverage.IsStableUnderComposition

Tactic:
.of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_

Premises used: CategoryTheory.Precoverage.IsStableUnderComposition.of_preZeroHypercoverFamily, AlgebraicGeometry.Scheme.qcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
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)
⊢ qcPrecoverage.IsStableUnderComposition

Tactic:
refine .of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
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)
⊢ QuasiCompactCover E

Tactic:
simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢

Premises used: AlgebraicGeometry.Scheme.quasiCompactCover_iff, AlgebraicGeometry.Scheme.qcCoverFamily_property
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
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
⊢ ∀ (i : E.I₀), QuasiCompactCover (F i)

Tactic:
simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢

Premises used: AlgebraicGeometry.Scheme.quasiCompactCover_iff, AlgebraicGeometry.Scheme.qcCoverFamily_property
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
X : Scheme
E : PreZeroHypercover X
F : (i : E.I₀) → PreZeroHypercover (E.X i)
hE : QuasiCompactCover E
hF : ∀ (i : E.I₀), QuasiCompactCover (F i)
⊢ QuasiCompactCover (E.bind F)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
⊢ qcPrecoverage.IsStableUnderSup

Tactic:
.of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_

Premises used: CategoryTheory.Precoverage.IsStableUnderSup.of_preZeroHypercoverFamily, AlgebraicGeometry.Scheme.qcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
refine :
  ∀ {X : Scheme.{u_1}} (E F : PreZeroHypercover X) (hE : qcCoverFamily.property E) (hF : qcCoverFamily.property F),
    qcCoverFamily.property (E.sum F)
⊢ qcPrecoverage.IsStableUnderSup

Tactic:
refine .of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
X : Scheme
E F : PreZeroHypercover X
hE : qcCoverFamily.property E
hF : qcCoverFamily.property F
⊢ QuasiCompactCover E

Tactic:
simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢

Premises used: AlgebraicGeometry.Scheme.quasiCompactCover_iff, AlgebraicGeometry.Scheme.qcCoverFamily_property
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
X : Scheme
E F : PreZeroHypercover X
hE : qcCoverFamily.property E
hF : qcCoverFamily.property F
hE₁ : QuasiCompactCover E
⊢ QuasiCompactCover F

Tactic:
simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE hF ⊢

Premises used: AlgebraicGeometry.Scheme.quasiCompactCover_iff, AlgebraicGeometry.Scheme.qcCoverFamily_property
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S : Scheme
X : Scheme
E F : PreZeroHypercover X
hE : QuasiCompactCover E
hF : QuasiCompactCover F
⊢ QuasiCompactCover (E.sum F)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
X : Scheme
inst : IsEmpty.{u + 1} ↥X
rw : QuasiCompactCover (PreZeroHypercover.empty X)
⊢ ⊥ ∈ qcPrecoverage.coverings X

Tactic:
rw [← PreZeroHypercover.presieve₀_empty.{0}, presieve₀_mem_qcPrecoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff, CategoryTheory.PreZeroHypercover.presieve₀_empty
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ QuasiCompactCover (PreZeroHypercover.empty X)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
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

Tactic:
Precoverage.le_of_zeroHypercover fun X E ↦ ?_

Premises used: CategoryTheory.Precoverage.le_of_zeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
hP : P ≤ fun (x x_1 : Scheme.{u}) (f : x ⟶ x_1) ↦ IsOpenMap (X := ↥x) (Y := ↥x_1) ⇑f
refine : ∀ (X : Scheme.{u}) (E : (precoverage P).ZeroHypercover X), E.presieve₀ ∈ qcPrecoverage.coverings X
⊢ precoverage P ≤ qcPrecoverage

Tactic:
refine Precoverage.le_of_zeroHypercover fun X E ↦ ?_

Premises used: CategoryTheory.Precoverage.le_of_zeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
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
rw : QuasiCompactCover E.toPreZeroHypercover
⊢ E.presieve₀ ∈ qcPrecoverage.coverings X

Tactic:
rw [presieve₀_mem_qcPrecoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
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
⊢ QuasiCompactCover E.toPreZeroHypercover

Tactic:
.of_isOpenMap fun i ↦ hP _ (Scheme.Cover.map_prop E i)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.QuasiCompactCover.of_isOpenMap, AlgebraicGeometry.Scheme.Cover.map_prop, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
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
⊢ QuasiCompactCover E.toPreZeroHypercover

Tactic:
exact .of_isOpenMap fun i ↦ hP _ (Scheme.Cover.map_prop E i)
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
⊢ zariskiPrecoverage ≤ qcPrecoverage

Tactic:
precoverage_le_qcPrecoverage_of_isOpenMap fun _ _ f _ ↦ f.isOpenEmbedding.isOpenMap

Premises used: Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Surjective f
inst_1 : QuasiCompact f
E : Cover (precoverage ⊤) Y := cover (P := ⊤) f trivial
rw : ∃ (E : PreZeroHypercover Y), qcCoverFamily.property E ∧ Presieve.singleton f = E.presieve₀
⊢ Presieve.singleton f ∈ qcPrecoverage.coverings Y

Tactic:
rw [qcPrecoverage, PreZeroHypercoverFamily.mem_precoverage_iff]

Premises used: CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff, AlgebraicGeometry.Scheme.qcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
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 =
    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage ⊤) (cover (P := ⊤) f trivial)).presieve₀

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Surjective f
inst_1 : QuasiCompact f
E : Cover (precoverage ⊤) Y := cover (P := ⊤) f trivial
refine :
  qcCoverFamily.property
    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage ⊤) (cover (P := ⊤) f trivial))
⊢ ∃ (E : PreZeroHypercover Y), qcCoverFamily.property E ∧ Presieve.singleton f = E.presieve₀

Tactic:
refine ⟨(f.cover (P := ⊤) trivial).toPreZeroHypercover, ?_, by simp⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Surjective f
inst_1 : QuasiCompact f
E : Cover (precoverage ⊤) Y := cover (P := ⊤) f trivial
⊢ QuasiCompactCover (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage ⊤) (cover (P := ⊤) f trivial))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
⊢ propQCPrecoverage P ≤ precoverage P

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P Q : MorphismProperty Scheme
h : P ≤ Q
h₂ : precoverage P ≤ precoverage Q
⊢ qcPrecoverage ⊓ precoverage P ≤ qcPrecoverage ⊓ precoverage Q

Tactic:
gcongr
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ precoverage P ≤ precoverage Q

Tactic:
precoverage_mono h

Premises used: AlgebraicGeometry.Scheme.precoverage_mono
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ precoverage P ≤ precoverage Q

Tactic:
exact precoverage_mono h

Premises used: AlgebraicGeometry.Scheme.precoverage_mono
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
rw : zariskiPrecoverage ≤ qcPrecoverage ∧ zariskiPrecoverage ≤ precoverage P
⊢ zariskiPrecoverage ≤ propQCPrecoverage P

Tactic:
rw [propQCPrecoverage, le_inf_iff]

Premises used: AlgebraicGeometry.Scheme.propQCPrecoverage, le_inf_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
⊢ zariskiPrecoverage ≤ qcPrecoverage ∧ zariskiPrecoverage ≤ precoverage P

Tactic:
⟨zariskiPrecoverage_le_qcPrecoverage, precoverage_mono fun X Y f hf ↦ ?_⟩

Premises used: AlgebraicGeometry.Scheme.precoverage_mono, And.intro, AlgebraicGeometry.Scheme.zariskiPrecoverage_le_qcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
refine : ∀ (X Y : Scheme.{u}) (f : X ⟶ Y) (hf : IsOpenImmersion f), P f
⊢ zariskiPrecoverage ≤ qcPrecoverage ∧ zariskiPrecoverage ≤ precoverage P

Tactic:
refine ⟨zariskiPrecoverage_le_qcPrecoverage, precoverage_mono fun X Y f hf ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsOpenImmersion f
⊢ P f

Tactic:
apply IsZariskiLocalAtSource.of_isOpenImmersion

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{u_1, u} (propQCPrecoverage P) S
rw : PreZeroHypercover.presieve₀.{u_1, u, u + 1} 𝒰.toPreZeroHypercover ∈ qcPrecoverage.coverings S
⊢ QuasiCompactCover 𝒰.toPreZeroHypercover

Tactic:
rw [← Scheme.presieve₀_mem_qcPrecoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{u_1, u} (propQCPrecoverage P) S
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1} 𝒰.toPreZeroHypercover ∈ qcPrecoverage.coverings S

Tactic:
𝒰.mem₀.1

Premises used: And.left, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{u_1, u} (propQCPrecoverage P) S
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1} 𝒰.toPreZeroHypercover ∈ qcPrecoverage.coverings S

Tactic:
exact 𝒰.mem₀.1

Premises used: And.left, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ ⊥ ∈ (propQCPrecoverage P).coverings X

Tactic:
⟨bot_mem_qcPrecoverage _, bot_mem_precoverage _ _⟩

Premises used: AlgebraicGeometry.Scheme.bot_mem_precoverage, Set.Mem, setOf, Set.inter, And.intro, AlgebraicGeometry.Scheme.bot_mem_qcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{u_1, u} (propQCPrecoverage P) S
dsimp : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ QuasiCompactCover 𝒰.forgetQc (P := P).toPreZeroHypercover

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{u_1, u} (propQCPrecoverage P) S
⊢ QuasiCompactCover 𝒰.toPreZeroHypercover

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
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)
⊢ (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).presieve₀ ∈ (precoverage P).coverings S

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
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)

Tactic:
⟨fun x ↦ ⟨.inl x, 𝒰.covers _⟩, fun i ↦ ?_⟩

Premises used: AlgebraicGeometry.Scheme.Cover.covers, Sum.inl, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
refine :
  ∀ (i : (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).I₀),
    P ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f i)
⊢ (∀ (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:
refine ⟨fun x ↦ ⟨.inl x, 𝒰.covers _⟩, fun i ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
i : (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).I₀
inl :
  ∀ (val : 𝒰.ulift (P := P).I₀),
    P (X := (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X (Sum.inl val))
      ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f (Sum.inl val))
inr :
  ∀ (val : (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover).I₀),
    P (X := (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X (Sum.inr val))
      ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f (Sum.inr val))
⊢ P ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f i)

Tactic:
induction i
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
val : 𝒰.ulift (P := P).I₀
⊢ P (X := (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X (Sum.inl val))
    ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f (Sum.inl val))

Tactic:
𝒰.map_prop _

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop, Sum.elim
-- Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Goal:
S_1 : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover.{w, u} (precoverage P) S
inst : QuasiCompactCover 𝒰.toPreZeroHypercover
val : 𝒰.ulift (P := P).I₀
⊢ P (X := (𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).X (Sum.inl val))
    ((𝒰.ulift (P := P).sum (QuasiCompactCover.ulift.{w, u} 𝒰.toPreZeroHypercover)).f (Sum.inl val))

Tactic:
exact 𝒰.map_prop _

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop