-- Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean
theorem IsIntegrallyClosed.of_localization_maximal {R : Type*} [CommRing R] [IsDomain R]
    (h : ∀ p : Ideal R, p ≠ ⊥ → [p.IsMaximal] → IsIntegrallyClosed (Localization.AtPrime p)) :
    IsIntegrallyClosed R

Proof state:
case neg.mk.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
h1 : 1 ∈ I
y : R
hy : y * ↑x.2 = 1 * x.1
⊢ ∃ y, (algebraMap R (FractionRing R)) y = Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x

Tactic:
exact ⟨y, (eq_mk'_of_mul_eq (hy.trans (one_mul x.1))).trans (mk_eq_mk'_apply x.1 x.2).symm⟩

Result:
no goals

Proof state:
case neg.mk
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
⊢ ∃ y, (algebraMap R (FractionRing R)) y = Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x

Tactic:
let I : Ideal R := span {x.2.1} / span {x.1}

Result:
case neg.mk
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
⊢ ∃ y, (algebraMap R (FractionRing R)) y = Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
hn : ¬I = ⊤
p : Ideal R
hpm : p.IsMaximal
hpi : I ≤ p
hic : IsIntegrallyClosed (Localization.AtPrime p)
hxp : IsIntegral (Localization.AtPrime p) (Localization.mk x.1 x.2)
w✝ : Localization.AtPrime p
y : R × ↥p.primeCompl
hy :
  (algebraMap (Localization.AtPrime p) (FractionRing R)) (Quot.mk (⇑(OreLocalization.oreEqv p.primeCompl R)) y) =
    Localization.mk x.1 x.2
⊢ ↑y.2 ∈ I

Tactic:
intro a ha

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
hn : ¬I = ⊤
p : Ideal R
hpm : p.IsMaximal
hpi : I ≤ p
hic : IsIntegrallyClosed (Localization.AtPrime p)
hxp : IsIntegral (Localization.AtPrime p) (Localization.mk x.1 x.2)
w✝ : Localization.AtPrime p
y : R × ↥p.primeCompl
hy :
  (algebraMap (Localization.AtPrime p) (FractionRing R)) (Quot.mk (⇑(OreLocalization.oreEqv p.primeCompl R)) y) =
    Localization.mk x.1 x.2
a : R
ha : a ∈ span {x.1}
⊢ ↑y.2 * a ∈ span {↑x.2}

Proof state:
case intro.intro.intro.mk
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
hn : ¬I = ⊤
p : Ideal R
hpm : p.IsMaximal
hpi : I ≤ p
hic : IsIntegrallyClosed (Localization.AtPrime p)
hxp : IsIntegral (Localization.AtPrime p) (Localization.mk x.1 x.2)
w✝ : Localization.AtPrime p
y : R × ↥p.primeCompl
hy :
  (algebraMap (Localization.AtPrime p) (FractionRing R)) (Quot.mk (⇑(OreLocalization.oreEqv p.primeCompl R)) y) =
    Localization.mk x.1 x.2
hyi : ↑y.2 ∈ I
⊢ False

Tactic:
exact y.2.2 (hpi hyi)

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
hn : ¬I = ⊤
p : Ideal R
hpm : p.IsMaximal
hpi : I ≤ p
hic : IsIntegrallyClosed (Localization.AtPrime p)
hxp : IsIntegral (Localization.AtPrime p) (Localization.mk x.1 x.2)
w✝ : Localization.AtPrime p
y : R × ↥p.primeCompl
hy :
  (algebraMap (Localization.AtPrime p) (FractionRing R)) (Quot.mk (⇑(OreLocalization.oreEqv p.primeCompl R)) y) =
    Localization.mk x.1 x.2
a : R
ha : a ∈ span {x.1}
b : R
hb : b * x.1 = a
⊢ ↑y.2 * a ∈ span {↑x.2}

Tactic:
apply mem_span_singleton'.mpr ⟨b * y.1, _⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
hn : ¬I = ⊤
p : Ideal R
hpm : p.IsMaximal
hpi : I ≤ p
hic : IsIntegrallyClosed (Localization.AtPrime p)
hxp : IsIntegral (Localization.AtPrime p) (Localization.mk x.1 x.2)
w✝ : Localization.AtPrime p
y : R × ↥p.primeCompl
hy :
  (algebraMap (Localization.AtPrime p) (FractionRing R)) (Quot.mk (⇑(OreLocalization.oreEqv p.primeCompl R)) y) =
    Localization.mk x.1 x.2
a : R
ha : a ∈ span {x.1}
b : R
hb : b * x.1 = a
⊢ b * y.1 * ↑x.2 = ↑y.2 * a

Proof state:
case neg.mk
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
h1 : 1 ∈ I
⊢ ∃ y, (algebraMap R (FractionRing R)) y = Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x

Tactic:
rcases mem_span_singleton'.mp (h1 x.1 (mem_span_singleton_self x.1)) with ⟨y, hy⟩

Result:
case neg.mk.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
h1 : 1 ∈ I
y : R
hy : y * ↑x.2 = 1 * x.1
⊢ ∃ y, (algebraMap R (FractionRing R)) y = Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : IsField R
⊢ IsIntegrallyClosed R

Tactic:
exact hf.toField.instIsIntegrallyClosed

Result:
no goals