-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma mem_overGrothendieckTopology (X : Over S) (R : Sieve X) :
    R ∈ S.overGrothendieckTopology P X ↔
      ∃ (𝒰 : Cover.{u} P X.left) (_ : 𝒰.Over S), 𝒰.toPresieveOver ≤ R.arrows

Proof state:
case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows) → R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Tactic:
rintro ⟨𝒰, h𝒰, hle⟩

Result:
case mpr.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
𝒰 : Cover P X.left
h𝒰 : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ R.arrows
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Proof state:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X → ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

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

Result:
case mp.intro.intro.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ R.arrows
⊢ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Proof state:
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Tactic:
constructor

Result:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X → ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

case mpr
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows) → R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Proof state:
case mp.intro.intro.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ R.arrows
⊢ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Tactic:
use 𝒰, h

Result:
no goals

Proof state:
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
⊢ R ∈ (overGrothendieckTopology P S) X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Tactic:
rw [overGrothendieckTopology_eq_toGrothendieck_overPretopology]

Result:
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Proof state:
case mpr.intro.intro
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
𝒰 : Cover P X.left
h𝒰 : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ R.arrows
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Tactic:
exact ⟨𝒰.toPresieveOver, ⟨𝒰, h𝒰, rfl⟩, hle⟩

Result:
no goals