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

Tactic:
use 𝒰, h

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

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
⊢ Hom.asOverProp (𝒰.map i) S ∈ R.arrows

Tactic:
let fi : (𝒰.obj i).asOverProp S (hj i) ⟶ X := (𝒰.map i).asOverProp S

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
⊢ Hom.asOverProp (𝒰.map i) S ∈ R.arrows

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

Tactic:
rintro - - ⟨i⟩

Result:
case h.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 𝒰
p : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
le : 𝒰.toPresieveOverProp p ≤ R.arrows
Y : Over S
i : 𝒰.J
⊢ Hom.asOver (𝒰.map i) S ∈ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows

Proof state:
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

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

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

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

Tactic:
have hj (j : 𝒰.J) : Q (𝒰.obj j ↘ S) := by
  rw [← comp_over (𝒰.map j)]
  exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop _) X.prop

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
𝒰 : 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)
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ 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
⊢ R ∈ (S.smallGrothendieckTopologyOfLE hPQ) X ↔ R ∈ (Pretopology.toGrothendieck (Q.Over ⊤ S) (smallPretopology P Q)) X

Tactic:
simp only [Pretopology.mem_toGrothendieck, Functor.mem_inducedTopology_sieves_iff,
  MorphismProperty.Comma.forget_obj, mem_overGrothendieckTopology]

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