-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem toBasicOpen_injective (f : R) : Function.Injective (toBasicOpen R f)

Proof state:
case intro.intro.mk.intro.intro.mk.intro
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
r : ↥p.asIdeal.primeCompl
hr : ↑r * (↑⟨d, ⋯⟩ * a) = ↑r * (↑⟨b, ⋯⟩ * c)
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal

Tactic:
exact ⟨r.1, hr, r.2⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
r₁ r₂ : R
hr₁ : r₁ * (d * a) = r₁ * (b * c)
hr₂ : r₂ * (d * a) = r₂ * (b * c)
⊢ (r₁ + r₂) * (d * a) = (r₁ + r₂) * (b * c)

Tactic:
simp only [add_mul, hr₁, hr₂]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f : R
s t : Localization.Away f
h_eq : (toBasicOpen R f) s = (toBasicOpen R f) t
⊢ s = t

Tactic:
obtain ⟨a, ⟨b, hb⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers f) s

Result:
case intro.intro.mk
R : Type u
inst✝ : CommRing R
f : R
t : Localization.Away f
a b : R
hb : b ∈ Submonoid.powers f
h_eq : (toBasicOpen R f) (IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩) = (toBasicOpen R f) t
⊢ IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩ = t

Proof state:
case intro.intro.mk
R : Type u
inst✝ : CommRing R
f : R
t : Localization.Away f
a b : R
hb : b ∈ Submonoid.powers f
h_eq : (toBasicOpen R f) (IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩) = (toBasicOpen R f) t
⊢ IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩ = t

Tactic:
obtain ⟨c, ⟨d, hd⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers f) t

Result:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq :
  (toBasicOpen R f) (IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩) =
    (toBasicOpen R f) (IsLocalization.mk' (Localization.Away f) c ⟨d, hd⟩)
⊢ IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩ = IsLocalization.mk' (Localization.Away f) c ⟨d, hd⟩

Proof state:
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
this : f ∈ I.radical
⊢ ∃ c_1, ↑c_1 * (↑⟨d, hd⟩ * a) = ↑c_1 * (↑⟨b, hb⟩ * c)

Tactic:
obtain ⟨n, hn⟩ := this

Result:
case intro
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
n : ℕ
hn : f ^ n ∈ I
⊢ ∃ c_1, ↑c_1 * (↑⟨d, hd⟩ * a) = ↑c_1 * (↑⟨b, hb⟩ * c)

Proof state:
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
r₁ r₂ : R
hr₁ : r₁ ∈ {r | r * (d * a) = r * (b * c)}
hr₂ : r₂ ∈ {r | r * (d * a) = r * (b * c)}
⊢ r₁ + r₂ ∈ {r | r * (d * a) = r * (b * c)}

Tactic:
dsimp at hr₁ hr₂ ⊢

Result:
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
r₁ r₂ : R
hr₁ : r₁ * (d * a) = r₁ * (b * c)
hr₂ : r₂ * (d * a) = r₂ * (b * c)
⊢ (r₁ + r₂) * (d * a) = (r₁ + r₂) * (b * c)

Proof state:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ∃ c_1, ↑c_1 * (↑⟨d, hd⟩ * a) = ↑c_1 * (↑⟨b, hb⟩ * c)

Tactic:
suffices f ∈ I.radical by
  obtain ⟨n, hn⟩ := this
  exact ⟨⟨f ^ n, n, rfl⟩, hn⟩

Result:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ f ∈ I.radical

Proof state:
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
⊢ 0 ∈ { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯ }.carrier

Tactic:
simp only [Set.mem_setOf_eq, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
r₁ r₂ : R
hr₂ : r₂ * (d * a) = r₂ * (b * c)
⊢ r₁ * r₂ * (d * a) = r₁ * r₂ * (b * c)

Tactic:
simp only [mul_assoc, hr₂]

Result:
no goals

Proof state:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ∀ x ∈ PrimeSpectrum.zeroLocus ↑I, f ∈ x.asIdeal

Tactic:
intro p hfp

Result:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
p : PrimeSpectrum R
hfp : p ∈ PrimeSpectrum.zeroLocus ↑I
⊢ f ∈ p.asIdeal

Proof state:
case intro
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
n : ℕ
hn : f ^ n ∈ I
⊢ ∃ c_1, ↑c_1 * (↑⟨d, hd⟩ * a) = ↑c_1 * (↑⟨b, hb⟩ * c)

Tactic:
exact ⟨⟨f ^ n, n, rfl⟩, hn⟩

Result:
no goals

Proof state:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
this :
  IsLocalization.mk' (Localization.AtPrime p.asIdeal) a ⟨b, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime p.asIdeal) c ⟨d, ⋯⟩
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal

Tactic:
rw [IsLocalization.eq (S := Localization.AtPrime p.asIdeal)] at this

Result:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
this : ∃ c_1, ↑c_1 * (↑⟨d, ⋯⟩ * a) = ↑c_1 * (↑⟨b, ⋯⟩ * c)
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal