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

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
⊢ p ∉ PrimeSpectrum.zeroLocus ↑I

Tactic:
rw [PrimeSpectrum.mem_zeroLocus, Set.not_subset]

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
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal

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) ⋯
⊢ ∃ c_1, ↑c_1 * (↑⟨d, hd⟩ * a) = ↑c_1 * (↑⟨b, hb⟩ * c)

Tactic:
let I : Ideal R :=
  { carrier := { r : R | r * (d * a) = r * (b * c) }
    zero_mem' := by simp only [Set.mem_setOf_eq, zero_mul]
    add_mem' := fun {r₁ r₂} hr₁ hr₂ => by dsimp at hr₁ hr₂ ⊢; simp only [add_mul, hr₁, hr₂]
    smul_mem' := fun {r₁ r₂} hr₂ => by dsimp at hr₂ ⊢; simp only [mul_assoc, hr₂] }

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' := ⋯ }
⊢ ∃ c_1, ↑c_1 * (↑⟨d, hd⟩ * a) = ↑c_1 * (↑⟨b, hb⟩ * 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' := ⋯ }
p : PrimeSpectrum R
hfp : p ∈ PrimeSpectrum.zeroLocus ↑I
⊢ f ∈ p.asIdeal

Tactic:
contrapose 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 : f ∉ p.asIdeal
⊢ p ∉ PrimeSpectrum.zeroLocus ↑I

Proof state:
R : Type u
inst✝ : CommRing R
f : R
⊢ Function.Injective ⇑(toBasicOpen R f)

Tactic:
intro s t h_eq

Result:
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

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' := ⋯ }
⊢ f ∈ I.radical

Tactic:
rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.mem_vanishingIdeal]

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' := ⋯ }
⊢ ∀ x ∈ PrimeSpectrum.zeroLocus ↑I, f ∈ x.asIdeal

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 :
  (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⟩

Tactic:
simp only [toBasicOpen_mk'] at h_eq

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) ⋯
⊢ IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩ = IsLocalization.mk' (Localization.Away f) c ⟨d, hd⟩

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
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal

Tactic:
have := congr_fun (congr_arg Subtype.val h_eq) ⟨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 : f ∉ p.asIdeal
this : ↑(const R a b (PrimeSpectrum.basicOpen f) ⋯) ⟨p, hfp⟩ = ↑(const R c d (PrimeSpectrum.basicOpen f) ⋯) ⟨p, hfp⟩
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal

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 : ↑(const R a b (PrimeSpectrum.basicOpen f) ⋯) ⟨p, hfp⟩ = ↑(const R c d (PrimeSpectrum.basicOpen f) ⋯) ⟨p, hfp⟩
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal

Tactic:
dsimp 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 :
  IsLocalization.mk' (Localization.AtPrime p.asIdeal) a ⟨b, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime p.asIdeal) c ⟨d, ⋯⟩
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal

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₂ ∈ { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
⊢ r₁ • r₂ ∈ { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
dsimp at 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)
⊢ r₁ * r₂ * (d * a) = r₁ * r₂ * (b * c)