-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem is_localization_basicOpen_of_qcqs {X : Scheme} {U : X.Opens} (hU : IsCompact U.1)
    (hU' : IsQuasiSeparated U.1) (f : Γ(X, U)) :
    IsLocalization.Away f (Γ(X, X.basicOpen f))

Proof state:
case exists_of_eq.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
H : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0
n : ℕ
e : f ^ n * z = 0
⊢ ↑⟨(fun x => f ^ x) n, ⋯⟩ * z = 0

Tactic:
simpa [mul_comm z] using e

Result:
no goals

Proof state:
case map_units'
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (y : ↥(Submonoid.powers f)), IsUnit ((algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑y)

Tactic:
rintro ⟨_, n, rfl⟩

Result:
case map_units'.mk.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
n : ℕ
⊢ IsUnit ((algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑⟨(fun x => f ^ x) n, ⋯⟩)

Proof state:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [← sub_eq_zero, ← map_sub, RingHom.algebraMap_toAlgebra]

Result:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (x - y) = 0 → ∃ c, ↑c * x = ↑c * y

Proof state:
case exists_of_eq.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
H : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0
n : ℕ
e : f ^ n * z = 0
⊢ ∃ c, ↑c * z = 0

Tactic:
refine ⟨⟨_, n, rfl⟩, ?_⟩

Result:
case exists_of_eq.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
H : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0
n : ℕ
e : f ^ n * z = 0
⊢ ↑⟨(fun x => f ^ x) n, ⋯⟩ * z = 0

Proof state:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (x - y) = 0 → ∃ c, ↑c * x = ↑c * y

Tactic:
simp_rw [← @sub_eq_zero _ _ (_ * x) (_ * y), ← mul_sub]

Result:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (x - y) = 0 → ∃ c, ↑c * (x - y) = 0

Proof state:
case surj'.intro.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
z : ↑Γ(X, X.basicOpen f)
n : ℕ
y : ↑Γ(X, U)
e : (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * z
⊢ z * (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

Tactic:
simpa only [map_pow, Subtype.coe_mk, RingHom.algebraMap_toAlgebra, mul_comm z] using e.symm

Result:
no goals

Proof state:
case surj'
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
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

Tactic:
obtain ⟨n, y, e⟩ := exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated X U hU hU' f z

Result:
case surj'.intro.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
z : ↑Γ(X, X.basicOpen f)
n : ℕ
y : ↑Γ(X, U)
e : (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * z
⊢ ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1

Proof state:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (x - y) = 0 → ∃ c, ↑c * (x - y) = 0

Tactic:
generalize x - y = z

Result:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0 → ∃ c, ↑c * z = 0

Proof state:
case map_units'.mk.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
n : ℕ
⊢ IsUnit ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n)

Tactic:
exact IsUnit.pow _ (RingedSpace.isUnit_res_basicOpen _ f)

Result:
no goals

Proof state:
case surj'.intro.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
z : ↑Γ(X, X.basicOpen f)
n : ℕ
y : ↑Γ(X, U)
e : (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * z
⊢ ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1

Tactic:
refine ⟨⟨y, _, n, rfl⟩, ?_⟩

Result:
case surj'.intro.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
z : ↑Γ(X, X.basicOpen f)
n : ℕ
y : ↑Γ(X, U)
e : (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * z
⊢ z * (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

Proof state:
case map_units'.mk.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
n : ℕ
⊢ IsUnit ((algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑⟨(fun x => f ^ x) n, ⋯⟩)

Tactic:
simp only [map_pow, Subtype.coe_mk, RingHom.algebraMap_toAlgebra]

Result:
case map_units'.mk.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
n : ℕ
⊢ IsUnit ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n)

Proof state:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ {x y : ↑Γ(X, U)},
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y

Tactic:
intro x y

Result:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y

Proof state:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
H : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0
⊢ ∃ c, ↑c * z = 0

Tactic:
obtain ⟨n, e⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU _ _ H

Result:
case exists_of_eq.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
H : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0
n : ℕ
e : f ^ n * z = 0
⊢ ∃ c, ↑c * z = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

Tactic:
constructor

Result:
case map_units'
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (y : ↥(Submonoid.powers f)), IsUnit ((algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑y)

case surj'
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (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

case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ {x y : ↑Γ(X, U)},
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y