awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P_1 P : MorphismProperty Scheme
inst : P.IsStableUnderComposition
⊢ (jointlySurjectivePrecoverage ⊓ P.precoverage).IsStableUnderComposition

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P_1 P : MorphismProperty Scheme
inst : P.ContainsIdentities
inst_1 : P.RespectsIso
⊢ (jointlySurjectivePrecoverage ⊓ P.precoverage).HasIsos

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
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)
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)
⊢ Presieve.ofArrows T p₁ ∈ (precoverage P).coverings Y

Tactic:
rw [ofArrows_mem_precoverage_iff] at hf ⊢

Premises used: AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
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)

Tactic:
⟨fun x ↦ ?_, fun i ↦ P.of_isPullback (H i).flip (hf.2 i)⟩

Premises used: CategoryTheory.MorphismProperty.of_isPullback, And.right, CategoryTheory.IsPullback.flip, And.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
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)
refine : ∀ (x : ↥Y), ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x
⊢ (∀ (x : ↥Y), ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x) ∧ ∀ (i : ι), P (p₁ i)

Tactic:
refine ⟨fun x ↦ ?_, fun i ↦ P.of_isPullback (H i).flip (hf.2 i)⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
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
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
⊢ ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x

Tactic:
obtain ⟨i, y, hy⟩ := hf.1 (g x)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.left, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
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)
⊢ HasPullback g (f i)

Tactic:
have := (H i).hasPullback
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
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)
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
⊢ ∃ (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

Premises used: And.right, Eq.symm, AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
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
h : (p₁ i) ((Iso.inv ⋯.isoPullback) w : ↥(T i)) = x
⊢ ∃ (i : ι), Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(T i)) ⇑(p₁ i)) x

Tactic:
use i, (H i).isoPullback.inv w

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.IsPullback.isoPullback, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
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
⊢ (p₁ i) ((Iso.inv ⋯.isoPullback) w : ↥(T i)) = x

Tactic:
simpa [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
⊢ jointlySurjectivePrecoverage.IsStableUnderBaseChange

Tactic:
isStableUnderBaseChange_comap_jointlySurjectivePrecoverage _
    fun f g _ ↦ pullbackComparison_forget_surjective f g

Premises used: CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage, AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
⊢ Sieve.ofArrows 𝒰.X 𝒰.f ∈ (grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X

Tactic:
Precoverage.generate_mem_toGrothendieck 𝒰.mem₀

Premises used: Set.Mem, setOf, CategoryTheory.Precoverage.generate_mem_toGrothendieck, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
rw : Sieve.generate ⊥ ∈ (grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X
⊢ ⊥ ∈ (grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X

Tactic:
rw [← Sieve.generate_bot]

Premises used: CategoryTheory.Sieve.generate_bot
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ Sieve.generate ⊥ ∈ (grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X

Tactic:
Precoverage.generate_mem_toGrothendieck (bot_mem_precoverage _ X)

Premises used: AlgebraicGeometry.Scheme.bot_mem_precoverage, Set.Mem, CategoryTheory.Precoverage.generate_mem_toGrothendieck
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ Sieve.generate ⊥ ∈ (grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X

Tactic:
exact Precoverage.generate_mem_toGrothendieck (bot_mem_precoverage _ X)

Premises used: AlgebraicGeometry.Scheme.bot_mem_precoverage, CategoryTheory.Precoverage.generate_mem_toGrothendieck
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ∈ (pretopology P).coverings X

Tactic:
𝒰.mem₀

Premises used: Set.Mem, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
R : Presieve X
⊢ R ∈ (pretopology P).coverings X ↔ ∃ (𝒰 : Cover (precoverage P) X), R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
Precoverage.mem_iff_exists_zeroHypercover

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover, AlgebraicGeometry.Scheme.precoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
S : Sieve X
simp_rw :
  (∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows) ↔
    ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
⊢ S ∈ (grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X ↔
    ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

Tactic:
simp_rw [grothendieckTopology, Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition]

Premises used: AlgebraicGeometry.Scheme.grothendieckTopology, CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
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

Tactic:
⟨fun ⟨R, hR, hle⟩ ↦ ?_, fun ⟨𝒰, hle⟩ ↦ ⟨.ofArrows 𝒰.X 𝒰.f, 𝒰.mem_pretopology, hle⟩⟩

Premises used: CategoryTheory.PreZeroHypercover.f, Membership.mem, Exists, CategoryTheory.Sieve.arrows, CategoryTheory.PreZeroHypercover.X, LE.le, And, And.intro, Iff.intro, Exists.intro, CategoryTheory.Precoverage.coverings, _private.0.AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff.match_1, AlgebraicGeometry.Scheme.precoverage, AlgebraicGeometry.Scheme.Cover.mem_pretopology, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.Presieve.ofArrows, _private.0.AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff.match_2
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
S : Sieve X
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
⊢ (∃ R ∈ (precoverage P).coverings X, 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⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
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
⊢ ∃ (𝒰 : (precoverage P).ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
rw [Precoverage.mem_iff_exists_zeroHypercover] at hR

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
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
hR₁ : ∃ (𝒰 : (precoverage P).ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ R ≤ S.arrows

Tactic:
rw [Precoverage.mem_iff_exists_zeroHypercover] at hR

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
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
obtain :
  ∀ (𝒰 : Cover (precoverage P) X) (hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows),
    ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
⊢ ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

Tactic:
obtain ⟨(𝒰 : Scheme.Cover _ _), rfl⟩ := hR

Premises used: AlgebraicGeometry.Scheme.Cover, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
X : Scheme
S : Sieve X
h_1 : ∃ R ∈ (precoverage P).coverings X, R ≤ S.arrows
𝒰 : Cover (precoverage P) X
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
w : Cover (precoverage P) X
h : Presieve.ofArrows 𝒰.ulift (P := P).X 𝒰.ulift (P := P).f ≤ S.arrows
⊢ ∃ (𝒰 : Cover (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

Tactic:
use 𝒰.ulift, le_trans (fun Y g ⟨i⟩ ↦ .mk _) hle

Premises used: AlgebraicGeometry.Scheme.Cover.ulift, le_trans
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
X : Scheme
s : Sieve X
⊢ s ∈ (jointlySurjectiveTopology : (a : Scheme) → Set (Sieve a)) X ↔ s.arrows ∈ jointlySurjectivePretopology.coverings X

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
⊢ jointlySurjectiveTopology = jointlySurjectivePretopology.toGrothendieck

Tactic:
GrothendieckTopology.copy_eq

Premises used: AlgebraicGeometry.Scheme.jointlySurjectiveTopology, CategoryTheory.GrothendieckTopology.copy_eq
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
⊢ pretopology P = jointlySurjectivePretopology ⊓ P.pretopology

Tactic:
rfl

Premises used: CategoryTheory.Precoverage.toPretopology, AlgebraicGeometry.Scheme.pretopology, AlgebraicGeometry.Scheme.precoverage, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
rw :
  Pretopology.toGrothendieck (Precoverage.toPretopology Scheme (precoverage P)) =
    (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck
⊢ grothendieckTopology P = (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck

Tactic:
rw [grothendieckTopology, ← Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck]

Premises used: AlgebraicGeometry.Scheme.grothendieckTopology, CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
⊢ Pretopology.toGrothendieck (Precoverage.toPretopology Scheme (precoverage P)) =
    (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P Q : MorphismProperty Scheme
hPQ : P ≤ Q
⊢ grothendieckTopology P ≤ grothendieckTopology Q

Tactic:
Precoverage.toGrothendieck_mono (precoverage_mono hPQ)

Premises used: AlgebraicGeometry.Scheme.precoverage_mono, CategoryTheory.Precoverage.toGrothendieck_mono
-- Module: Mathlib.AlgebraicGeometry.Sites.Pretopology
Goal:
P Q : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : P.IsStableUnderBaseChange
inst_2 : Q.IsMultiplicative
inst_3 : Q.IsStableUnderBaseChange
hPQ : P ≤ Q
⊢ pretopology P ≤ pretopology Q

Tactic:
precoverage_mono hPQ

Premises used: AlgebraicGeometry.Scheme.precoverage_mono
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
⊢ proetalePrecoverage ≤ MorphismProperty.precoverage @WeaklyEtale

Tactic:
le_trans inf_le_right inf_le_right

Premises used: inf_le_right, le_trans
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
⊢ proetalePrecoverage ≤ fpqcPrecoverage

Tactic:
propQCPrecoverage_monotone fun _ _ _ _ ↦ inferInstance

Premises used: inferInstance, AlgebraicGeometry.Scheme.propQCPrecoverage_monotone
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
⊢ proetaleTopology = propQCTopology @WeaklyEtale

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.proetalePrecoverage, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
rw : precoverage @Etale ≤ qcPrecoverage ∧ precoverage @Etale ≤ precoverage @WeaklyEtale
⊢ etalePrecoverage ≤ proetalePrecoverage

Tactic:
rw [proetalePrecoverage, propQCPrecoverage, etalePrecoverage, le_inf_iff]

Premises used: AlgebraicGeometry.Scheme.propQCPrecoverage, le_inf_iff, AlgebraicGeometry.Scheme.proetalePrecoverage, AlgebraicGeometry.Scheme.etalePrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
⊢ precoverage @Etale ≤ qcPrecoverage ∧ precoverage @Etale ≤ precoverage @WeaklyEtale

Tactic:
⟨precoverage_le_qcPrecoverage_of_isOpenMap fun X Y f hf ↦ f.isOpenMap, ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.isOpenMap, And.intro, AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
refine : precoverage @Etale ≤ precoverage @WeaklyEtale
⊢ precoverage @Etale ≤ qcPrecoverage ∧ precoverage @Etale ≤ precoverage @WeaklyEtale

Tactic:
refine ⟨precoverage_le_qcPrecoverage_of_isOpenMap fun X Y f hf ↦ f.isOpenMap, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
h : @Etale ≤ @WeaklyEtale
⊢ precoverage @Etale ≤ precoverage @WeaklyEtale

Tactic:
apply precoverage_mono

Premises used: AlgebraicGeometry.Scheme.precoverage_mono
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ WeaklyEtale f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
⊢ etaleTopology ≤ proetaleTopology

Tactic:
Precoverage.toGrothendieck_mono etalePrecoverage_le_proetalePrecoverage

Premises used: AlgebraicGeometry.Scheme.etalePrecoverage_le_proetalePrecoverage, CategoryTheory.Precoverage.toGrothendieck_mono
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
⊢ proetaleTopology ≤ fpqcTopology

Tactic:
Precoverage.toGrothendieck_mono proetalePrecoverage_le_fpqcPrecoverage

Premises used: CategoryTheory.Precoverage.toGrothendieck_mono, AlgebraicGeometry.Scheme.proetalePrecoverage_le_fpqcPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
⊢ proetaleTopology.Subcanonical

Tactic:
.of_le proetaleTopology_le_fpqcTopology

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.of_le, AlgebraicGeometry.Scheme.proetaleTopology_le_fpqcTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
𝒰 : Cover.{u_1, u} (precoverage @WeaklyEtale) S
i : 𝒰.I₀
⊢ WeaklyEtale (𝒰.f i)

Tactic:
𝒰.map_prop i

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
U : S.ProEt
⊢ WeaklyEtale U.toComma (P := @WeaklyEtale) (Q := ⊤) (W := ⊤).hom

Tactic:
U.prop

Premises used: CategoryTheory.MorphismProperty.Comma.prop
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ (ProEt.forget S).Full

Tactic:
inferInstanceAs <| (MorphismProperty.Over.forget _ _ _).Full

Premises used: _private.0.AlgebraicGeometry.Scheme.ProEt.instFullOverForget._proof_1
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ (ProEt.forget S).Faithful

Tactic:
inferInstanceAs <| (MorphismProperty.Over.forget _ _ _).Faithful

Premises used: _private.0.AlgebraicGeometry.Scheme.ProEt.instFaithfulOverForget._proof_1
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ PreservesFiniteLimits (ProEt.forget S)

Tactic:
inferInstanceAs <| PreservesFiniteLimits (MorphismProperty.Over.forget _ _ _)

Premises used: _private.0.AlgebraicGeometry.Scheme.ProEt.instPreservesFiniteLimitsOverForget._proof_1
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ RepresentablyFlat (ProEt.forget S)

Tactic:
flat_of_preservesFiniteLimits _

Premises used: CategoryTheory.flat_of_preservesFiniteLimits
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
H : proetalePrecoverage ≤ MorphismProperty.precoverage @WeaklyEtale
⊢ (ProEt.forget S).LocallyCoverDense (proetaleTopology.over S)

Tactic:
apply MorphismProperty.locallyCoverDense_forget_of_le

Premises used: CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ proetalePrecoverage ≤ MorphismProperty.precoverage @WeaklyEtale

Tactic:
proetalePrecoverage_le_precoverage_weaklyEtale

Premises used: AlgebraicGeometry.Scheme.proetalePrecoverage_le_precoverage_weaklyEtale
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ proetalePrecoverage ≤ MorphismProperty.precoverage @WeaklyEtale

Tactic:
exact proetalePrecoverage_le_precoverage_weaklyEtale

Premises used: AlgebraicGeometry.Scheme.proetalePrecoverage_le_precoverage_weaklyEtale
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
H : proetalePrecoverage ≤ MorphismProperty.precoverage @WeaklyEtale
⊢ topology S = (ProEt.forget S).inducedTopology (proetaleTopology.over S)

Tactic:
apply MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology

Premises used: CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
rw :
  (ProEt.forget S).IsContinuous ((ProEt.forget S).inducedTopology (proetaleTopology.over S)) (proetaleTopology.over S)
⊢ (ProEt.forget S).IsContinuous (topology S) (proetaleTopology.over S)

Tactic:
rw [topology_eq_inducedTopology]

Premises used: AlgebraicGeometry.Scheme.ProEt.topology_eq_inducedTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Proetale
Goal:
S : Scheme
⊢ (ProEt.forget S).IsContinuous ((ProEt.forget S).inducedTopology (proetaleTopology.over S)) (proetaleTopology.over S)

Tactic:
Functor.isContinuous_of_coverPreserving (compatiblePreservingOfFlat _ _) ?_

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

Tactic:
refine Functor.isContinuous_of_coverPreserving (compatiblePreservingOfFlat _ _) ?_

Premises used: CategoryTheory.compatiblePreservingOfFlat, CategoryTheory.Functor.isContinuous_of_coverPreserving