-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem _root_.AlgebraicGeometry.exists_basicOpen_le_affine_inter
    {V : X.Opens} (hV : IsAffineOpen V) (x : X) (hx : x ∈ U ⊓ V) :
    ∃ (f : Γ(X, U)) (g : Γ(X, V)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hx : x ∈ U ⊓ V
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := hU.exists_basicOpen_le ⟨x, hx.2⟩ hx.1

Result:
case intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Proof state:
case intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
obtain ⟨g, hg₁, hg₂⟩ := hV.exists_basicOpen_le ⟨x, hf₂⟩ hx.2

Result:
case intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
g : ↑Γ(X, V)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
g : ↑Γ(X, V)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g
f' : ↑Γ(X, U)
hf' : X.basicOpen f' = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE hf₁).op)) g)
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
replace hf' := (hf'.trans (RingedSpace.basicOpen_res _ _ _)).trans (inf_eq_right.mpr hg₁)

Result:
case intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
g : ↑Γ(X, V)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g
f' : ↑Γ(X, U)
hf' : X.basicOpen f' = X.toRingedSpace.basicOpen g
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
g : ↑Γ(X, V)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g
f' : ↑Γ(X, U)
hf' : X.basicOpen f' = X.toRingedSpace.basicOpen g
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
exact ⟨f', g, hf', hf'.symm ▸ hg₂⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
g : ↑Γ(X, V)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
obtain ⟨f', hf'⟩ :=
  basicOpen_basicOpen_is_basicOpen hU f (X.presheaf.map (homOfLE hf₁ : _ ⟶ V).op g)

Result:
case intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↑↑X.toPresheafedSpace
hx : x ∈ U ⊓ V
f : ↑Γ(X, U)
hf₁ : X.basicOpen f ≤ V
hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f
g : ↑Γ(X, V)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g
f' : ↑Γ(X, U)
hf' : X.basicOpen f' = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE hf₁).op)) g)
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f