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 ∈ ⊥
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)) =
    ⊥
ext x
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 ∈ ⊥
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 ∈ ⊥
rw [Algebra.mem_iInf]
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 ∈ ⊥

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)
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 ∈ ⊥
constructor
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)
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 ∈ ⊥
rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]
no goals
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)
exact fun hx ⟨v, hv⟩ => hx ⟨v, hv.isPrime⟩
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)
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)
rw [Algebra.mem_bot]
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)
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)
rintro ⟨y, rfl⟩ ⟨v, hv⟩
no goals
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)
exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩
no goals
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)⁻¹
rw [map_one, inv_one, mul_one]