-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma mem_toGrothendieck_smallPretopology (X : Q.Over ⊤ S) (R : Sieve X) :
    R ∈ (S.smallPretopology P Q).toGrothendieck _ X ↔
      ∀ x : X.left, ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : Y.left),
        R f ∧ P f.left ∧ f.left.base y = x

Proof state:
case refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁶ : P.IsMultiplicative
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : IsJointlySurjectivePreserving P
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
Y : ↑↑X.left.toPresheafedSpace → Q.Over ⊤ S
f : (x : ↑↑X.left.toPresheafedSpace) → Y x ⟶ X
y : (x : ↑↑X.left.toPresheafedSpace) → ↑↑(Y x).left.toPresheafedSpace
hf : ∀ (x : ↑↑X.left.toPresheafedSpace), R.arrows (f x)
hP : ∀ (x : ↑↑X.left.toPresheafedSpace), P (f x).left
hy : ∀ (x : ↑↑X.left.toPresheafedSpace), (ConcreteCategory.hom (f x).left.base) (y x) = x
𝒰 : Cover P X.left :=
  { J := ↑↑X.left.toPresheafedSpace, obj := fun i => (Y i).left, map := fun i => (f i).left, f := id, covers := ⋯,
    map_prop := hP }
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

Tactic:
letI : 𝒰.Over S :=
  { over := fun i ↦ inferInstance
    isOver_map := fun i ↦ inferInstance }

Result:
case refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁶ : P.IsMultiplicative
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : IsJointlySurjectivePreserving P
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
Y : ↑↑X.left.toPresheafedSpace → Q.Over ⊤ S
f : (x : ↑↑X.left.toPresheafedSpace) → Y x ⟶ X
y : (x : ↑↑X.left.toPresheafedSpace) → ↑↑(Y x).left.toPresheafedSpace
hf : ∀ (x : ↑↑X.left.toPresheafedSpace), R.arrows (f x)
hP : ∀ (x : ↑↑X.left.toPresheafedSpace), P (f x).left
hy : ∀ (x : ↑↑X.left.toPresheafedSpace), (ConcreteCategory.hom (f x).left.base) (y x) = x
𝒰 : Cover P X.left :=
  { J := ↑↑X.left.toPresheafedSpace, obj := fun i => (Y i).left, map := fun i => (f i).left, f := id, covers := ⋯,
    map_prop := hP }
this : Cover.Over S 𝒰 := { over := fun i => inferInstance, isOver_map := ⋯ }
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁶ : P.IsMultiplicative
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : IsJointlySurjectivePreserving P
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↑↑X.left.toPresheafedSpace
y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace
hy : (ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) y = x
⊢ Hom.asOverProp (𝒰.map (𝒰.f x)) S ∈ 𝒰.toPresieveOverProp p

Tactic:
use 𝒰.f x

Result:
no goals

Proof state:
case refine_2.refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁶ : P.IsMultiplicative
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : IsJointlySurjectivePreserving P
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
Y : ↑↑X.left.toPresheafedSpace → Q.Over ⊤ S
f : (x : ↑↑X.left.toPresheafedSpace) → Y x ⟶ X
y : (x : ↑↑X.left.toPresheafedSpace) → ↑↑(Y x).left.toPresheafedSpace
hf : ∀ (x : ↑↑X.left.toPresheafedSpace), R.arrows (f x)
hP : ∀ (x : ↑↑X.left.toPresheafedSpace), P (f x).left
hy : ∀ (x : ↑↑X.left.toPresheafedSpace), (ConcreteCategory.hom (f x).left.base) (y x) = x
𝒰 : Cover P X.left :=
  { J := ↑↑X.left.toPresheafedSpace, obj := fun i => (Y i).left, map := fun i => (f i).left, f := id, covers := ⋯,
    map_prop := hP }
this : Cover.Over S 𝒰 := { over := fun i => inferInstance, isOver_map := ⋯ }
⊢ 𝒰.toPresieveOverProp ⋯ ∈ (smallPretopology P Q).coverings X

Tactic:
use 𝒰, inferInstance, fun i ↦ MorphismProperty.Comma.prop _

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.intro
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁶ : P.IsMultiplicative
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : IsJointlySurjectivePreserving P
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↑↑X.left.toPresheafedSpace
⊢ ∃ Y f y, R.arrows f ∧ P f.left ∧ (ConcreteCategory.hom f.left.base) y = x

Tactic:
obtain ⟨y, hy⟩ := 𝒰.covers x

Result:
case refine_1.intro.intro.intro.intro.intro.intro
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁶ : P.IsMultiplicative
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : IsJointlySurjectivePreserving P
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↑↑X.left.toPresheafedSpace
y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace
hy : (ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) y = x
⊢ ∃ Y f y, R.arrows f ∧ P f.left ∧ (ConcreteCategory.hom f.left.base) y = x