-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem basicOpen_basicOpen_is_basicOpen (g : Γ(X, X.basicOpen f)) :
    ∃ f' : Γ(X, U), X.basicOpen f' = X.basicOpen g

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen (f * x) =
    X.basicOpen
      (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩))

Tactic:
rw [Algebra.smul_def, Scheme.basicOpen_mul, Scheme.basicOpen_mul, RingHom.algebraMap_toAlgebra,
  Scheme.basicOpen_res]

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen f ⊓ X.basicOpen x =
    X.basicOpen f ⊓ X.basicOpen x ⊓
      X.basicOpen ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩)

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen f ⊓ X.basicOpen x =
    X.basicOpen f ⊓ X.basicOpen x ⊓
      X.basicOpen ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩)

Tactic:
refine (inf_eq_left.mpr (inf_le_left.trans_eq (Scheme.basicOpen_of_isUnit _ ?_).symm)).symm

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ IsUnit ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩)

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ IsUnit ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩)

Tactic:
exact
  Submonoid.leftInv_le_isUnit _
    (IsLocalization.toInvSubmonoid (Submonoid.powers f) (Γ(X, X.basicOpen f))
      _).prop

Result:
no goals

Proof state:
case intro.intro.mk.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ ∃ f',
    X.basicOpen f' =
      X.basicOpen
        (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩))

Tactic:
use f * x

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen (f * x) =
    X.basicOpen
      (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
g : ↑Γ(X, X.basicOpen f)
⊢ ∃ f', X.basicOpen f' = X.basicOpen g

Tactic:
have := isLocalization_basicOpen hU f

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
g : ↑Γ(X, X.basicOpen f)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ ∃ f', X.basicOpen f' = X.basicOpen g

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
g : ↑Γ(X, X.basicOpen f)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ ∃ f', X.basicOpen f' = X.basicOpen g

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.surj'' (Submonoid.powers f) g

Result:
case intro.intro.mk.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ ∃ f',
    X.basicOpen f' =
      X.basicOpen
        (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩))