-- 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:
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 ⊤
⊢ P U

Tactic:
apply h₁

Result:
case a
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), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

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 ⊤

Tactic:
apply h₃

Result:
no goals

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
⊢ P U'

Tactic:
obtain ⟨_, _, rfl, rfl, h₂'⟩ := h₂ _ _ (X.affineBasisCover.map j)

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 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' := ⋯ }
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

Tactic:
let i' : U' ⟶ U := homOfLE 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
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

Proof state:
case a
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), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

Tactic:
intro x

Result:
case a
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
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

Proof state:
case a
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
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

Tactic:
obtain ⟨_, ⟨j, rfl⟩, hx, i⟩ :=
  X.affineBasisCover_is_basis.exists_subset_of_mem_open (SetLike.mem_coe.2 x.prop) U.isOpen

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
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V