-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem iInf_localization_eq_bot [Algebra R K] [hK : IsFractionRing R K] :
    (⨅ v : HeightOneSpectrum R,
        Localization.subalgebra.ofField K _ v.asIdeal.primeCompl_le_nonZeroDivisors) = ⊥

Proof state:
case h.mp
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

case h.mpr
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ → ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Tactic:
on_goal 1 => by_cases hR : IsField R

Result:
case pos
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

case neg
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

case h.mpr
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ → ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Proof state:
case h
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) ↔ x ∈ ⊥

Tactic:
constructor

Result:
case h.mp
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

case h.mpr
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ → ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Proof state:
case h.mpr
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Tactic:
exact fun hx ⟨v, hv, hbot⟩ => hx ⟨v, hv.isMaximal hbot⟩

Result:
no goals

Proof state:
case h.mp
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

Tactic:
by_cases hR : IsField R

Result:
case pos
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

case neg
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

Proof state:
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
⊢ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥

Tactic:
ext x

Result:
case h
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ ↔ x ∈ ⊥

Proof state:
case h
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ ↔ x ∈ ⊥

Tactic:
rw [Algebra.mem_iInf]

Result:
case h
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) ↔ x ∈ ⊥

Proof state:
case pos.intro.intro
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
algebra_map_inv : K → R
left✝ : Function.LeftInverse algebra_map_inv ⇑(algebraMap R K)
algebra_map_right_inv : Function.RightInverse algebra_map_inv ⇑(algebraMap R K)
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

Tactic:
exact fun _ => Algebra.mem_bot.mpr ⟨algebra_map_inv x, algebra_map_right_inv x⟩

Result:
no goals

Proof state:
case neg
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

case h.mpr
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ → ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Tactic:
all_goals rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]

Result:
case neg
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

case h.mpr
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Proof state:
case pos
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

Tactic:
rcases Function.bijective_iff_has_inverse.mp
  (IsField.localization_map_bijective (Rₘ := K) (flip nonZeroDivisors.ne_zero rfl : 0 ∉ R⁰) hR)
  with ⟨algebra_map_inv, _, algebra_map_right_inv⟩

Result:
case pos.intro.intro
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
algebra_map_inv : K → R
left✝ : Function.LeftInverse algebra_map_inv ⇑(algebraMap R K)
algebra_map_right_inv : Function.RightInverse algebra_map_inv ⇑(algebraMap R K)
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥

Proof state:
case neg
R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : IsDedekindDomain R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Tactic:
exact fun hx ⟨v, hv⟩ => hx ((equivMaximalSpectrum hR).symm ⟨v, hv⟩)

Result:
no goals