-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma overGrothendieckTopology_eq_toGrothendieck_overPretopology :
    S.overGrothendieckTopology P = (S.overPretopology P).toGrothendieck

Proof state:
case right
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
hT : Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows
this✝ : (i : 𝒰.J) → (𝒰.obj i).Over S := fun i => { hom := 𝒰.map i ≫ X.hom }
this : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
⊢ 𝒰.toPresieveOver ≤ R.arrows

Tactic:
rwa [Cover.toPresieveOver_le_arrows_iff]

Result:
no goals

Proof state:
case h.h.h
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
⊢ (∃ R_1 ∈ (pretopology P).coverings X.left, R_1 ≤ ((Sieve.overEquiv X) R).arrows) ↔
    R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Tactic:
constructor

Result:
case h.h.h.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_1 ∈ (pretopology P).coverings X.left, R_1 ≤ ((Sieve.overEquiv X) R).arrows) →
    R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

case h.h.h.mpr
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 →
    ∃ R_1 ∈ (pretopology P).coverings X.left, R_1 ≤ ((Sieve.overEquiv X) R).arrows

Proof state:
case h.h.h.mp.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
hT : Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows
this✝ : (i : 𝒰.J) → (𝒰.obj i).Over S := fun i => { hom := 𝒰.map i ≫ X.hom }
this : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Tactic:
use 𝒰.toPresieveOver, ⟨𝒰, inferInstance, rfl⟩

Result:
case right
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
hT : Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows
this✝ : (i : 𝒰.J) → (𝒰.obj i).Over S := fun i => { hom := 𝒰.map i ≫ X.hom }
this : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
⊢ 𝒰.toPresieveOver ≤ R.arrows

Proof state:
case h.h.h.mpr
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 →
    ∃ R_1 ∈ (pretopology P).coverings X.left, R_1 ≤ ((Sieve.overEquiv X) R).arrows

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

Result:
case h.h.h.mpr.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 𝒰
hT : 𝒰.toPresieveOver ≤ R.arrows
⊢ ∃ R_1 ∈ (pretopology P).coverings X.left, R_1 ≤ ((Sieve.overEquiv X) R).arrows

Proof state:
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
⊢ overGrothendieckTopology P S = Pretopology.toGrothendieck (Over S) (overPretopology P S)

Tactic:
ext X R

Result:
case h.h.h
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 ↔ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Proof state:
case h.h.h.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_1 ∈ (pretopology P).coverings X.left, R_1 ≤ ((Sieve.overEquiv X) R).arrows) →
    R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Tactic:
rintro ⟨T, ⟨𝒰, rfl⟩, hT⟩

Result:
case h.h.h.mp.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
hT : Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Proof state:
case right
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 𝒰
hT : 𝒰.toPresieveOver ≤ R.arrows
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows

Tactic:
rwa [Cover.toPresieveOver_le_arrows_iff] at hT

Result:
no goals

Proof state:
case h.h.h.mp.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
hT : Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows
this : (i : 𝒰.J) → (𝒰.obj i).Over S := fun i => { hom := 𝒰.map i ≫ X.hom }
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

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

Result:
case h.h.h.mp.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
hT : Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows
this✝ : (i : 𝒰.J) → (𝒰.obj i).Over S := fun i => { hom := 𝒰.map i ≫ X.hom }
this : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
⊢ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Proof state:
case h.h.h
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 ↔ R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X

Tactic:
rw [GrothendieckTopology.mem_over_iff, Pretopology.mem_toGrothendieck]

Result:
case h.h.h
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Over S
R : Sieve X
⊢ (∃ R_1 ∈ (pretopology P).coverings X.left, R_1 ≤ ((Sieve.overEquiv X) R).arrows) ↔
    R ∈ (Pretopology.toGrothendieck (Over S) (overPretopology P S)) X