-- 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 ⊤
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

Tactic:
let _ : Type (u + 1) := Presieve 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
⊢ 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
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

Tactic:
choose Y y f hf hy using hs

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
⊢ 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 := ⋯ }
⊢ S ∈ (Pretopology.toGrothendieck Scheme (pretopology P)) X

Tactic:
refine ⟨Presieve.ofArrows 𝒰.obj 𝒰.map, ⟨𝒰, rfl⟩, ?_⟩

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 := ⋯ }
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map ≤ S.arrows