-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma locallyCoverDense_of_le (hPQ : P ≤ Q) :
    (MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S) where
  functorPushforward_functorPullback_mem X

Proof state:
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
⊢ ∀ (T : ↑((overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X))),
    Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
        (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑T) ∈
      (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)

Tactic:
intro ⟨T, hT⟩

Result:
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
⊢ Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
      (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩) ∈
    (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)

Proof state:
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
⊢ Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
      (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩) ∈
    (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)

Tactic:
rw [mem_overGrothendieckTopology] at hT ⊢

Result:
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT✝ : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : ∃ 𝒰 x, 𝒰.toPresieveOver ≤ T.arrows
⊢ ∃ 𝒰 x,
    𝒰.toPresieveOver ≤
      (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
          (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT✝⟩)).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
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover P ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
⊢ 𝒰.toPresieveOver ≤
    (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
        (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩)).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
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover P ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.J
⊢ Hom.asOver (𝒰.map i) S ∈
    (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
        (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩)).arrows

Proof state:
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT✝ : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : ∃ 𝒰 x, 𝒰.toPresieveOver ≤ T.arrows
⊢ ∃ 𝒰 x,
    𝒰.toPresieveOver ≤
      (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
          (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT✝⟩)).arrows

Tactic:
obtain ⟨𝒰, h, hle⟩ := hT

Result:
case intro.intro
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover P ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
⊢ ∃ 𝒰 x,
    𝒰.toPresieveOver ≤
      (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
          (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩)).arrows

Proof state:
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover P ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
Y : Over S
i : 𝒰.J
⊢ Q (𝒰.map i ≫ ((MorphismProperty.Over.forget Q ⊤ S).obj X).left ↘ S)

Tactic:
exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop i) X.prop

Result:
no goals