-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology (hPQ : P ≤ Q) :
    S.smallGrothendieckTopologyOfLE hPQ = (S.smallPretopology P Q).toGrothendieck

Proof state:
case h.h.h.mp.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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
le : 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows
hj : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
Y : Q.Over ⊤ S
i : 𝒰.J
fi : (𝒰.obj i).asOverProp S ⋯ ⟶ X := Hom.asOverProp (𝒰.map i) S
⊢ Hom.asOverProp (𝒰.map i) S ∈ R.arrows

Tactic:
have : R.functorPushforward _ ((MorphismProperty.Over.forget Q ⊤ S).map fi) := le _ ⟨i⟩

Result:
case h.h.h.mp.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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
le : 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows
hj : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
Y : Q.Over ⊤ S
i : 𝒰.J
fi : (𝒰.obj i).asOverProp S ⋯ ⟶ X := Hom.asOverProp (𝒰.map i) S
this :
  (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows ((MorphismProperty.Over.forget Q ⊤ S).map fi)
⊢ Hom.asOverProp (𝒰.map i) S ∈ R.arrows

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
hPQ : P ≤ Q
⊢ S.smallGrothendieckTopologyOfLE hPQ = Pretopology.toGrothendieck (Q.Over ⊤ S) (smallPretopology P Q)

Tactic:
ext X R

Result:
case h.h.h
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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
⊢ R ∈ (S.smallGrothendieckTopologyOfLE hPQ) X ↔ R ∈ (Pretopology.toGrothendieck (Q.Over ⊤ S) (smallPretopology P Q)) X

Proof state:
case h.h.h.mp.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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
le : 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows
hj : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
⊢ 𝒰.toPresieveOverProp hj ≤ R.arrows

Tactic:
rintro - - ⟨i⟩

Result:
case h.h.h.mp.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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
le : 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows
hj : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
Y : Q.Over ⊤ S
i : 𝒰.J
⊢ Hom.asOverProp (𝒰.map i) S ∈ R.arrows

Proof state:
case h.h.h
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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows) ↔
    ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

Tactic:
constructor

Result:
case h.h.h.mp
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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows) →
    ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

case h.h.h.mpr
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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
⊢ (∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows) →
    ∃ 𝒰 x, 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows