-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma mem_smallGrothendieckTopology [P.HasOfPostcompProperty P] (X : P.Over ⊤ S) (R : Sieve X) :
    R ∈ S.smallGrothendieckTopology P X ↔
      ∃ (𝒰 : Cover.{u} P X.left) (_ : 𝒰.Over S) (h : ∀ j, P (𝒰.obj j ↘ S)),
          𝒰.toPresieveOverProp h ≤ R.arrows

Proof state:
case mp.intro.intro.intro.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Tactic:
use 𝒰, h, p

Result:
no goals

Proof state:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ (∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows) →
    R ∈ (Pretopology.toGrothendieck (P.Over ⊤ S) (smallPretopology P P)) X

Tactic:
rintro ⟨𝒰, h𝒰, p, hle⟩

Result:
case mpr.intro.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h𝒰 : Cover.Over S 𝒰
p : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
⊢ R ∈ (Pretopology.toGrothendieck (P.Over ⊤ S) (smallPretopology P P)) X

Proof state:
case mpr.intro.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h𝒰 : Cover.Over S 𝒰
p : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
⊢ R ∈ (Pretopology.toGrothendieck (P.Over ⊤ S) (smallPretopology P P)) X

Tactic:
exact ⟨𝒰.toPresieveOverProp p, ⟨𝒰, h𝒰, p, rfl⟩, hle⟩

Result:
no goals

Proof state:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (Pretopology.toGrothendieck (P.Over ⊤ S) (smallPretopology P P)) X →
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Tactic:
rintro ⟨T, ⟨𝒰, h, p, rfl⟩, hle⟩

Result:
case mp.intro.intro.intro.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Proof state:
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallGrothendieckTopology P) X ↔ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Tactic:
rw [smallGrothendieckTopology_eq_toGrothendieck_smallPretopology]

Result:
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (Pretopology.toGrothendieck (P.Over ⊤ S) (smallPretopology P P)) X ↔
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Proof state:
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (Pretopology.toGrothendieck (P.Over ⊤ S) (smallPretopology P P)) X ↔
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Tactic:
constructor

Result:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (Pretopology.toGrothendieck (P.Over ⊤ S) (smallPretopology P P)) X →
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ (∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.J), P (𝒰.obj j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows) →
    R ∈ (Pretopology.toGrothendieck (P.Over ⊤ S) (smallPretopology P P)) X