-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem exists_basicOpen_le {V : X.Opens} (x : V) (h : ↑x ∈ U) :
    ∃ f : Γ(X, U), X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Tactic:
obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, h₁, h₂⟩ :=
  (isBasis_basicOpen U).exists_subset_of_mem_open (x.2 : (⟨x, h⟩ : U) ∈ _)
    ((Opens.map U.inclusion').obj V).isOpen

Result:
case intro.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appIso U.ι ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Tactic:
rw [Scheme.basicOpen_res_eq]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appIso U.ι ⊤).inv) r) = X.basicOpen r

Proof state:
case intro.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this✝ : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
this : U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Tactic:
use X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top.symm).op r

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this✝ : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
this : U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r) ≤ V ∧
    ↑x ∈ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this✝ : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
this : U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r) ≤ V ∧
    ↑x ∈ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Tactic:
rw [← this]

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this✝ : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
this : U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)
⊢ U.ι ''ᵁ (↑U).basicOpen r ≤ V ∧ ↑x ∈ U.ι ''ᵁ (↑U).basicOpen r

Proof state:
case intro.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Tactic:
have :
  U.ι ''ᵁ (U.toScheme.basicOpen r) =
    X.basicOpen (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top.symm).op r) := by
  refine (Scheme.image_basicOpen U.ι r).trans ?_
  rw [Scheme.basicOpen_res_eq]
  simp only [Scheme.Opens.toScheme_presheaf_obj, Scheme.Opens.ι_appIso, Iso.refl_inv,
    CommRingCat.id_apply]

Result:
case intro.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this✝ : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
this : U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
⊢ U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Tactic:
refine (Scheme.image_basicOpen U.ι r).trans ?_

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appIso U.ι ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appIso U.ι ⊤).inv) r) = X.basicOpen r

Tactic:
simp only [Scheme.Opens.toScheme_presheaf_obj, Scheme.Opens.ι_appIso, Iso.refl_inv,
  CommRingCat.id_apply]

Result:
no goals

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this✝ : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion' U)).obj V)
this : U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)
⊢ U.ι ''ᵁ (↑U).basicOpen r ≤ V ∧ ↑x ∈ U.ι ''ᵁ (↑U).basicOpen r

Tactic:
exact ⟨Set.image_subset_iff.mpr h₂, ⟨_, h⟩, h₁, rfl⟩

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Tactic:
have : IsAffine _ := hU

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f