-- 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
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

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

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 }
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

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:
intro x

Result:
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

Proof state:
case refine_2.refine_2.mk
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 := ⋯ }
Y : Q.Over ⊤ S
i : 𝒰.J
⊢ Hom.asOverProp (𝒰.map i) S ∈ R.arrows

Tactic:
exact hf i

Result:
no goals

Proof state:
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
⊢ (∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows) ↔
    ∀ (x : ↑↑X.left.toPresheafedSpace), ∃ Y f y, R.arrows f ∧ P f.left ∧ (ConcreteCategory.hom f.left.base) y = x

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Result:
case 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
⊢ (∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows) →
    ∀ (x : ↑↑X.left.toPresheafedSpace), ∃ Y f y, R.arrows f ∧ P f.left ∧ (ConcreteCategory.hom f.left.base) y = x

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
h : ∀ (x : ↑↑X.left.toPresheafedSpace), ∃ Y f y, R.arrows f ∧ P f.left ∧ (ConcreteCategory.hom f.left.base) y = x
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

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
h : ∀ (x : ↑↑X.left.toPresheafedSpace), ∃ Y f y, R.arrows f ∧ P f.left ∧ (ConcreteCategory.hom f.left.base) y = x
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

Tactic:
choose Y f y hf hP hy using h

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
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows