-- Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean
/--
The Grothendieck topology defined by `P`-covers agrees with the Grothendieck
topology induced by the intersection of the pretopology of surjective families with
the pretopology defined by `P`.

Note: Because of size issues, this does not hold on the level of pretopologies: A presieve
in the intersection can have up to `Type (u + 1)` many components, while in the definition
of `AlgebraicGeometry.Scheme.pretopology` we only allow `Type u` many components.
-/
lemma grothendieckTopology_eq_inf [IsJointlySurjectivePreserving ⊤] :
    grothendieckTopology P = (surjectiveFamiliesPretopology ⊓ P.pretopology).toGrothendieck

Proof state:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
⊢ grothendieckTopology P = Pretopology.toGrothendieck Scheme (surjectiveFamiliesPretopology ⊓ P.pretopology)

Tactic:
apply le_antisymm ((Pretopology.gi Scheme.{u}).gc.monotone_l (pretopology_le_inf P))

Result:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
⊢ Pretopology.toGrothendieck Scheme (surjectiveFamiliesPretopology ⊓ P.pretopology) ≤
    Pretopology.toGrothendieck Scheme (pretopology P)

Proof state:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
⊢ Pretopology.toGrothendieck Scheme (surjectiveFamiliesPretopology ⊓ P.pretopology) ≤
    Pretopology.toGrothendieck Scheme (pretopology P)

Tactic:
intro X S ⟨T, ⟨hs, hP⟩, hle⟩

Result:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
S : Sieve X
T : Presieve X
hs : T ∈ surjectiveFamiliesPretopology.coverings X
hP : T ∈ P.pretopology.coverings X
hle : T ≤ S.arrows
⊢ S ∈ (Pretopology.toGrothendieck Scheme (pretopology P)) X

Proof state:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
S : Sieve X
T : Presieve X
hP : T ∈ P.pretopology.coverings X
hle : T ≤ S.arrows
x✝ : Type (u + 1) := Presieve X
J : Type (u + 1) := (Y : Scheme) × (Y ⟶ X)
Y : ↑↑X.toPresheafedSpace → Scheme
y : (x : ↑↑X.toPresheafedSpace) → ↑↑(Y x).toPresheafedSpace
f : (x : ↑↑X.toPresheafedSpace) → Y x ⟶ X
hf : ∀ (x : ↑↑X.toPresheafedSpace), T (f x)
hy : ∀ (x : ↑↑X.toPresheafedSpace), (ConcreteCategory.hom (f x).base) (y x) = x
𝒰 : Cover P X := { J := ↑↑X.toPresheafedSpace, obj := Y, map := f, f := id, covers := ⋯, map_prop := ⋯ }
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map ≤ S.arrows

Tactic:
rintro Z g ⟨x⟩

Result:
case mk
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
S : Sieve X
T : Presieve X
hP : T ∈ P.pretopology.coverings X
hle : T ≤ S.arrows
x✝ : Type (u + 1) := Presieve X
J : Type (u + 1) := (Y : Scheme) × (Y ⟶ X)
Y✝ : ↑↑X.toPresheafedSpace → Scheme
y : (x : ↑↑X.toPresheafedSpace) → ↑↑(Y✝ x).toPresheafedSpace
f : (x : ↑↑X.toPresheafedSpace) → Y✝ x ⟶ X
hf : ∀ (x : ↑↑X.toPresheafedSpace), T (f x)
hy : ∀ (x : ↑↑X.toPresheafedSpace), (ConcreteCategory.hom (f x).base) (y x) = x
𝒰 : Cover P X := { J := ↑↑X.toPresheafedSpace, obj := Y✝, map := f, f := id, covers := ⋯, map_prop := ⋯ }
Y : Scheme
x : 𝒰.J
⊢ 𝒰.map x ∈ S.arrows

Proof state:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
S : Sieve X
T : Presieve X
hs : T ∈ surjectiveFamiliesPretopology.coverings X
hP : T ∈ P.pretopology.coverings X
hle : T ≤ S.arrows
x✝ : Type (u + 1) := Presieve X
⊢ S ∈ (Pretopology.toGrothendieck Scheme (pretopology P)) X

Tactic:
let J := (Y : Scheme.{u}) × (Y ⟶ X)

Result:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
S : Sieve X
T : Presieve X
hs : T ∈ surjectiveFamiliesPretopology.coverings X
hP : T ∈ P.pretopology.coverings X
hle : T ≤ S.arrows
x✝ : Type (u + 1) := Presieve X
J : Type (u + 1) := (Y : Scheme) × (Y ⟶ X)
⊢ S ∈ (Pretopology.toGrothendieck Scheme (pretopology P)) X

Proof state:
case mk
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
S : Sieve X
T : Presieve X
hP : T ∈ P.pretopology.coverings X
hle : T ≤ S.arrows
x✝ : Type (u + 1) := Presieve X
J : Type (u + 1) := (Y : Scheme) × (Y ⟶ X)
Y✝ : ↑↑X.toPresheafedSpace → Scheme
y : (x : ↑↑X.toPresheafedSpace) → ↑↑(Y✝ x).toPresheafedSpace
f : (x : ↑↑X.toPresheafedSpace) → Y✝ x ⟶ X
hf : ∀ (x : ↑↑X.toPresheafedSpace), T (f x)
hy : ∀ (x : ↑↑X.toPresheafedSpace), (ConcreteCategory.hom (f x).base) (y x) = x
𝒰 : Cover P X := { J := ↑↑X.toPresheafedSpace, obj := Y✝, map := f, f := id, covers := ⋯, map_prop := ⋯ }
Y : Scheme
x : 𝒰.J
⊢ 𝒰.map x ∈ S.arrows

Tactic:
exact hle _ (hf x)

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
S : Sieve X
T : Presieve X
hP : T ∈ P.pretopology.coverings X
hle : T ≤ S.arrows
x✝ : Type (u + 1) := Presieve X
J : Type (u + 1) := (Y : Scheme) × (Y ⟶ X)
Y : ↑↑X.toPresheafedSpace → Scheme
y : (x : ↑↑X.toPresheafedSpace) → ↑↑(Y x).toPresheafedSpace
f : (x : ↑↑X.toPresheafedSpace) → Y x ⟶ X
hf : ∀ (x : ↑↑X.toPresheafedSpace), T (f x)
hy : ∀ (x : ↑↑X.toPresheafedSpace), (ConcreteCategory.hom (f x).base) (y x) = x
⊢ S ∈ (Pretopology.toGrothendieck Scheme (pretopology P)) X

Tactic:
let 𝒰 : Cover.{u} P X :=
  { J := X
    obj := Y
    map := f
    f := id
    covers := fun x ↦ ⟨y x, hy x⟩
    map_prop := fun x ↦ hP (hf x)
  }

Result:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
S : Sieve X
T : Presieve X
hP : T ∈ P.pretopology.coverings X
hle : T ≤ S.arrows
x✝ : Type (u + 1) := Presieve X
J : Type (u + 1) := (Y : Scheme) × (Y ⟶ X)
Y : ↑↑X.toPresheafedSpace → Scheme
y : (x : ↑↑X.toPresheafedSpace) → ↑↑(Y x).toPresheafedSpace
f : (x : ↑↑X.toPresheafedSpace) → Y x ⟶ X
hf : ∀ (x : ↑↑X.toPresheafedSpace), T (f x)
hy : ∀ (x : ↑↑X.toPresheafedSpace), (ConcreteCategory.hom (f x).base) (y x) = x
𝒰 : Cover P X := { J := ↑↑X.toPresheafedSpace, obj := Y, map := f, f := id, covers := ⋯, map_prop := ⋯ }
⊢ S ∈ (Pretopology.toGrothendieck Scheme (pretopology P)) X