-- Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean
lemma grothendieckTopology_cover {X : Scheme.{u}} (𝒰 : Cover.{v} P X) :
    grothendieckTopology P X (Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map))

Proof state:
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Scheme
𝒰 : Cover P X
𝒱 : Cover P X :=
  { J := ↑↑X.toPresheafedSpace, obj := fun x => 𝒰.obj (𝒰.f x), map := fun x => 𝒰.map (𝒰.f x), f := id, covers := ⋯,
    map_prop := ⋯ }
⊢ (grothendieckTopology P) X (Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map))

Tactic:
refine ⟨_, pretopology_cover 𝒱, ?_⟩

Result:
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Scheme
𝒰 : Cover P X
𝒱 : Cover P X :=
  { J := ↑↑X.toPresheafedSpace, obj := fun x => 𝒰.obj (𝒰.f x), map := fun x => 𝒰.map (𝒰.f x), f := id, covers := ⋯,
    map_prop := ⋯ }
⊢ Presieve.ofArrows 𝒱.obj 𝒱.map ≤ (Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map)).arrows

Proof state:
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Scheme
𝒰 : Cover P X
𝒱 : Cover P X :=
  { J := ↑↑X.toPresheafedSpace, obj := fun x => 𝒰.obj (𝒰.f x), map := fun x => 𝒰.map (𝒰.f x), f := id, covers := ⋯,
    map_prop := ⋯ }
Y : Scheme
y : 𝒱.J
⊢ 𝟙 (𝒱.obj y) ≫ 𝒰.map (𝒰.f y) = 𝒱.map y

Tactic:
simp [𝒱]

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Scheme
𝒰 : Cover P X
⊢ (grothendieckTopology P) X (Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map))

Tactic:
let 𝒱 : Cover.{u} P X :=
  { J := X
    obj := fun x ↦ 𝒰.obj (𝒰.f x)
    map := fun x ↦ 𝒰.map (𝒰.f x)
    f := id
    covers := 𝒰.covers
    map_prop := fun _ ↦ 𝒰.map_prop _
  }

Result:
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Scheme
𝒰 : Cover P X
𝒱 : Cover P X :=
  { J := ↑↑X.toPresheafedSpace, obj := fun x => 𝒰.obj (𝒰.f x), map := fun x => 𝒰.map (𝒰.f x), f := id, covers := ⋯,
    map_prop := ⋯ }
⊢ (grothendieckTopology P) X (Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map))

Proof state:
case mk
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Scheme
𝒰 : Cover P X
𝒱 : Cover P X :=
  { J := ↑↑X.toPresheafedSpace, obj := fun x => 𝒰.obj (𝒰.f x), map := fun x => 𝒰.map (𝒰.f x), f := id, covers := ⋯,
    map_prop := ⋯ }
Y : Scheme
y : 𝒱.J
⊢ 𝒱.map y ∈ (Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map)).arrows

Tactic:
exact ⟨_, 𝟙 _, 𝒰.map (𝒰.f y), ⟨_⟩, by simp [𝒱]⟩

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Scheme
𝒰 : Cover P X
𝒱 : Cover P X :=
  { J := ↑↑X.toPresheafedSpace, obj := fun x => 𝒰.obj (𝒰.f x), map := fun x => 𝒰.map (𝒰.f x), f := id, covers := ⋯,
    map_prop := ⋯ }
⊢ Presieve.ofArrows 𝒱.obj 𝒱.map ≤ (Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map)).arrows

Tactic:
rintro _ _ ⟨y⟩

Result:
case mk
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : P.RespectsIso
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving P
X : Scheme
𝒰 : Cover P X
𝒱 : Cover P X :=
  { J := ↑↑X.toPresheafedSpace, obj := fun x => 𝒰.obj (𝒰.f x), map := fun x => 𝒰.map (𝒰.f x), f := id, covers := ⋯,
    map_prop := ⋯ }
Y : Scheme
y : 𝒱.J
⊢ 𝒱.map y ∈ (Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map)).arrows