[GOAL]
R : Type u
inst✝ : CommRing R
x✝¹ x✝ : MaximalSpectrum R
asIdeal✝¹ : Ideal R
IsMaximal✝¹ : Ideal.IsMaximal asIdeal✝¹
asIdeal✝ : Ideal R
IsMaximal✝ : Ideal.IsMaximal asIdeal✝
h :
  toPrimeSpectrum { asIdeal := asIdeal✝¹, IsMaximal := IsMaximal✝¹ } =
    toPrimeSpectrum { asIdeal := asIdeal✝, IsMaximal := IsMaximal✝ }
⊢ { asIdeal := asIdeal✝¹, IsMaximal := IsMaximal✝¹ } = { asIdeal := asIdeal✝, IsMaximal := IsMaximal✝ }
[PROOFSTEP]
simpa only [MaximalSpectrum.mk.injEq] using (PrimeSpectrum.ext_iff _ _).mp h
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | IsClosed {x}}
[PROOFSTEP]
simp only [isClosed_singleton_iff_isMaximal]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | Ideal.IsMaximal x.asIdeal}
[PROOFSTEP]
ext ⟨x, _⟩
[GOAL]
case h.mk
R : Type u
inst✝ : CommRing R
x : Ideal R
IsPrime✝ : Ideal.IsPrime x
⊢ { asIdeal := x, IsPrime := IsPrime✝ } ∈ range toPrimeSpectrum ↔
    { asIdeal := x, IsPrime := IsPrime✝ } ∈ {x | Ideal.IsMaximal x.asIdeal}
[PROOFSTEP]
exact ⟨fun ⟨y, hy⟩ => hy ▸ y.IsMaximal, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩
[GOAL]
R : Type u
inst✝ : CommRing R
x : MaximalSpectrum R
⊢ toPrimeSpectrum ⁻¹' {toPrimeSpectrum x} = {x}
[PROOFSTEP]
simpa only [← image_singleton] using preimage_image_eq { x } toPrimeSpectrum_injective
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ⨅ (v : MaximalSpectrum R),
      Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal)
        (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) =
    ⊥
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈
      ⨅ (v : MaximalSpectrum R),
        Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal)
          (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) ↔
    x ∈ ⊥
[PROOFSTEP]
rw [Algebra.mem_bot, Algebra.mem_iInf]
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) ↔
    x ∈ range ↑(algebraMap R K)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) →
    x ∈ range ↑(algebraMap R K)
[PROOFSTEP]
contrapose
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ ¬x ∈ range ↑(algebraMap R K) →
    ¬∀ (i : MaximalSpectrum R),
        x ∈
          Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
            (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
intro hrange hlocal
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
⊢ False
[PROOFSTEP]
let denom : Ideal R := (Submodule.span R {1} : Submodule R K).colon (Submodule.span R { x })
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
⊢ False
[PROOFSTEP]
have hdenom : (1 : R) ∉ denom := by
  intro hdenom
  rcases Submodule.mem_span_singleton.mp (Submodule.mem_colon.mp hdenom x <| Submodule.mem_span_singleton_self x) with
    ⟨y, hy⟩
  exact hrange ⟨y, by rw [← mul_one <| algebraMap R K y, ← Algebra.smul_def, hy, one_smul]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
⊢ ¬1 ∈ denom
[PROOFSTEP]
intro hdenom
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : 1 ∈ denom
⊢ False
[PROOFSTEP]
rcases Submodule.mem_span_singleton.mp (Submodule.mem_colon.mp hdenom x <| Submodule.mem_span_singleton_self x) with
  ⟨y, hy⟩
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : 1 ∈ denom
y : R
hy : y • 1 = 1 • x
⊢ False
[PROOFSTEP]
exact hrange ⟨y, by rw [← mul_one <| algebraMap R K y, ← Algebra.smul_def, hy, one_smul]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : 1 ∈ denom
y : R
hy : y • 1 = 1 • x
⊢ ↑(algebraMap R K) y = x
[PROOFSTEP]
rw [← mul_one <| algebraMap R K y, ← Algebra.smul_def, hy, one_smul]
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : ¬1 ∈ denom
⊢ False
[PROOFSTEP]
rcases denom.exists_le_maximal fun h => (h ▸ hdenom) Submodule.mem_top with ⟨max, hmax, hle⟩
[GOAL]
case h.mp.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : ¬1 ∈ denom
max : Ideal R
hmax : Ideal.IsMaximal max
hle : denom ≤ max
⊢ False
[PROOFSTEP]
rcases hlocal ⟨max, hmax⟩ with ⟨n, d, hd, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
⊢ False
[PROOFSTEP]
apply hd (hle <| Submodule.mem_colon.mpr fun _ hy => _)
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
⊢ ∀ (x : K), x ∈ Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹} → d • x ∈ Submodule.span R {1}
[PROOFSTEP]
intro _ hy
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
x✝ : K
hy : x✝ ∈ Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹}
⊢ d • x✝ ∈ Submodule.span R {1}
[PROOFSTEP]
rcases Submodule.mem_span_singleton.mp hy with ⟨y, rfl⟩
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
y : R
hy :
  y • (↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹) ∈ Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹}
⊢ d • y • (↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹) ∈ Submodule.span R {1}
[PROOFSTEP]
exact
  Submodule.mem_span_singleton.mpr
    ⟨y * n, by
      rw [Algebra.smul_def, mul_one, map_mul, smul_comm, Algebra.smul_def, Algebra.smul_def,
        mul_comm <| algebraMap R K d,
        inv_mul_cancel_right₀ <|
          (map_ne_zero_iff _ <| NoZeroSMulDivisors.algebraMap_injective R K).mpr fun h => (h ▸ hd) max.zero_mem]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
y : R
hy :
  y • (↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹) ∈ Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹}
⊢ (y * n) • 1 = d • y • (↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹)
[PROOFSTEP]
rw [Algebra.smul_def, mul_one, map_mul, smul_comm, Algebra.smul_def, Algebra.smul_def, mul_comm <| algebraMap R K d,
  inv_mul_cancel_right₀ <|
    (map_ne_zero_iff _ <| NoZeroSMulDivisors.algebraMap_injective R K).mpr fun h => (h ▸ hd) max.zero_mem]
[GOAL]
case h.mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ range ↑(algebraMap R K) →
    ∀ (i : MaximalSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
rintro ⟨y, rfl⟩ ⟨v, hv⟩
[GOAL]
case h.mpr.intro.mk
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : Ideal.IsMaximal v
⊢ ↑(algebraMap R K) y ∈
    Localization.subalgebra.ofField K (Ideal.primeCompl { asIdeal := v, IsMaximal := hv }.asIdeal)
      (_ : Ideal.primeCompl { asIdeal := v, IsMaximal := hv }.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : Ideal.IsMaximal v
⊢ ↑(algebraMap R K) y = ↑(algebraMap R K) y * (↑(algebraMap R K) 1)⁻¹
[PROOFSTEP]
rw [map_one, inv_one, mul_one]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ⨅ (v : PrimeSpectrum R),
      Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal)
        (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) =
    ⊥
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈
      ⨅ (v : PrimeSpectrum R),
        Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal)
          (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) ↔
    x ∈ ⊥
[PROOFSTEP]
rw [Algebra.mem_iInf]
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) ↔
    x ∈ ⊥
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) →
    x ∈ ⊥
[PROOFSTEP]
rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) →
    ∀ (i : MaximalSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
exact fun hx ⟨v, hv⟩ => hx ⟨v, hv.isPrime⟩
[GOAL]
case h.mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ ⊥ →
    ∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
rw [Algebra.mem_bot]
[GOAL]
case h.mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ Set.range ↑(algebraMap R K) →
    ∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
rintro ⟨y, rfl⟩ ⟨v, hv⟩
[GOAL]
case h.mpr.intro.mk
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : Ideal.IsPrime v
⊢ ↑(algebraMap R K) y ∈
    Localization.subalgebra.ofField K (Ideal.primeCompl { asIdeal := v, IsPrime := hv }.asIdeal)
      (_ : Ideal.primeCompl { asIdeal := v, IsPrime := hv }.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : Ideal.IsPrime v
⊢ ↑(algebraMap R K) y = ↑(algebraMap R K) y * (↑(algebraMap R K) 1)⁻¹
[PROOFSTEP]
rw [map_one, inv_one, mul_one]
