-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem exists_eq_pow_mul_of_isAffineOpen (X : Scheme) (U : X.Opens) (hU : IsAffineOpen U)
    (f : Γ(X, U)) (x : Γ(X, X.basicOpen f)) :
    ∃ (n : ℕ) (y : Γ(X, U)), y |_ X.basicOpen f = (f |_ X.basicOpen f) ^ n * x

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
⊢ ∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Tactic:
have := (hU.isLocalization_basicOpen f).2

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
this :
  ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1
⊢ ∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Proof state:
case intro.mk.mk.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
this :
  ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1
y : ↑Γ(X, U)
n : ℕ
d :
  x * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑(y, ⟨(fun x => f ^ x) n, ⋯⟩).2 =
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) (y, ⟨(fun x => f ^ x) n, ⋯⟩).1
⊢ ∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Tactic:
use n, y

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
this :
  ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1
y : ↑Γ(X, U)
n : ℕ
d :
  x * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑(y, ⟨(fun x => f ^ x) n, ⋯⟩).2 =
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) (y, ⟨(fun x => f ^ x) n, ⋯⟩).1
⊢ (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
this :
  ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1
⊢ ∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Tactic:
obtain ⟨⟨y, _, n, rfl⟩, d⟩ := this x

Result:
case intro.mk.mk.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
this :
  ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1
y : ↑Γ(X, U)
n : ℕ
d :
  x * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑(y, ⟨(fun x => f ^ x) n, ⋯⟩).2 =
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) (y, ⟨(fun x => f ^ x) n, ⋯⟩).1
⊢ ∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
this :
  ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1
y : ↑Γ(X, U)
n : ℕ
d :
  x * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑(y, ⟨(fun x => f ^ x) n, ⋯⟩).2 =
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) (y, ⟨(fun x => f ^ x) n, ⋯⟩).1
⊢ (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Tactic:
simpa [mul_comm x] using d.symm

Result:
no goals