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

Tactic:
rcases mem_span_singleton'.mp ha with ⟨b, hb⟩

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

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
a : R
ha : a ∈ span {x.1}
b : R
hb : b * x.1 = a
⊢ b * y.1 * ↑x.2 = ↑y.2 * a

Tactic:
rw [← hb, ← mul_assoc, mul_comm y.2.1 b, mul_assoc, mul_assoc]

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) = b * (↑y.2 * x.1)

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 = ⊤
⊢ False

Tactic:
rcases I.exists_le_maximal hn with ⟨p, hpm, hpi⟩

Result:
case intro.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
⊢ False

Proof state:
case neg
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}, IsIntegral R x → ∃ y, (algebraMap R (FractionRing R)) y = x

Tactic:
rintro ⟨x⟩ hx

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)
⊢ ∃ 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
a : R
ha : a ∈ span {x.1}
b : R
hb : b * x.1 = a
⊢ b * (y.1 * ↑x.2) = b * (↑y.2 * x.1)

Tactic:
exact congrArg (HMul.hMul b) <| (mul_comm y.1 x.2.1).trans <|
  FaithfulSMul.algebraMap_injective R (Localization R⁰) <| mk'_eq_iff_eq.mp <|
    (mk'_eq_algebraMap_mk'_of_submonoid_le _ _ p.primeCompl_le_nonZeroDivisors y.1 y.2).trans
      <| show algebraMap (Localization.AtPrime p) _ (mk' _ y.1 y.2) = mk' _ x.1 x.2
        by simpa only [← mk_eq_mk', ← hy] using by rfl

Result:
no goals

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
a : R
ha : a ∈ span {x.1}
b : R
hb : b * x.1 = a
⊢ (algebraMap (Localization.AtPrime p) (Localization R⁰)) (mk' (Localization.AtPrime p) y.1 y.2) =
    mk' (Localization R⁰) x.1 x.2

Tactic:
simpa only [← mk_eq_mk', ← hy] using by rfl

Result:
no goals

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

Tactic:
by_cases hf : IsField R

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

case neg
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