-- Mathlib/AlgebraicGeometry/Properties.lean
theorem reduce_to_affine_global (P : ∀ {X : Scheme} (_ : X.Opens), Prop)
    {X : Scheme} (U : X.Opens)
    (h₁ : ∀ (X : Scheme) (U : X.Opens),
      (∀ x : U, ∃ (V : _) (_ : x.1 ∈ V) (_ : V ⟶ U), P V) → P U)
    (h₂ : ∀ (X Y) (f : X ⟶ Y) [IsOpenImmersion f],
      ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = f.opensRange ∧ (P U → P V))
    (h₃ : ∀ R : CommRingCat, P (X := Spec R) ⊤) : P U

Proof state:
case a.intro.intro.intro.intro
P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.J
hx : ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base)
i : Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base) ⊆ ↑U
U' : Opens ↑↑X.toPresheafedSpace :=
  { carrier := Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom (X.affineBasisCover.map j)).base), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

Tactic:
refine ⟨U', hx, i', ?_⟩

Result:
case a.intro.intro.intro.intro
P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.J
hx : ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base)
i : Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base) ⊆ ↑U
U' : Opens ↑↑X.toPresheafedSpace :=
  { carrier := Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom (X.affineBasisCover.map j)).base), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
⊢ P U'

Proof state:
case a.intro.intro.intro.intro.intro.intro.intro.intro
P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.J
hx : ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base)
i : Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base) ⊆ ↑U
U' : Opens ↑↑X.toPresheafedSpace :=
  { carrier := Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom (X.affineBasisCover.map j)).base), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
h₂' : P ⊤ → P (Scheme.Hom.opensRange (X.affineBasisCover.map j))
⊢ P U'

Tactic:
apply h₂'

Result:
case a.intro.intro.intro.intro.intro.intro.intro.intro
P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.J
hx : ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base)
i : Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base) ⊆ ↑U
U' : Opens ↑↑X.toPresheafedSpace :=
  { carrier := Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom (X.affineBasisCover.map j)).base), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
h₂' : P ⊤ → P (Scheme.Hom.opensRange (X.affineBasisCover.map j))
⊢ P ⊤

Proof state:
case a.intro.intro.intro.intro
P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.J
hx : ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base)
i : Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base) ⊆ ↑U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

Tactic:
let U' : Opens _ := ⟨_, (X.affineBasisCover.map_prop j).base_open.isOpen_range⟩

Result:
case a.intro.intro.intro.intro
P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.J
hx : ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base)
i : Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map j).base) ⊆ ↑U
U' : Opens ↑↑X.toPresheafedSpace :=
  { carrier := Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom (X.affineBasisCover.map j)).base), is_open' := ⋯ }
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V