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

Tactic:
have hyi : y.2.1 ∈ I := by
  intro a ha
  rcases mem_span_singleton'.mp ha with ⟨b, hb⟩
  apply mem_span_singleton'.mpr ⟨b * y.1, _⟩
  rw [← hb, ← mul_assoc, mul_comm y.2.1 b, mul_assoc, mul_assoc]
  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:
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

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}
⊢ 1 ∈ I

Tactic:
apply I.eq_top_iff_one.mp

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}
⊢ I = ⊤

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⁰)) (Localization.mk y.1 y.2) =
    (algebraMap (Localization.AtPrime p) (FractionRing R)) (Quot.mk (⇑(OreLocalization.oreEqv p.primeCompl R)) y)

Tactic:
rfl

Result:
no goals

Proof state:
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

Tactic:
have hic := h p (Ring.ne_bot_of_isMaximal_of_not_isField hpm hf)

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
hic : IsIntegrallyClosed (Localization.AtPrime p)
⊢ False

Proof state:
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
hic : IsIntegrallyClosed (Localization.AtPrime p)
hxp : IsIntegral (Localization.AtPrime p) (Localization.mk x.1 x.2)
⊢ False

Tactic:
rcases (isIntegrallyClosed_iff (FractionRing R)).mp hic hxp with ⟨⟨y⟩, hy⟩

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

Proof state:
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
hic : IsIntegrallyClosed (Localization.AtPrime p)
⊢ False

Tactic:
have hxp : IsIntegral (Localization.AtPrime p) (mk x.1 x.2) := hx.tower_top

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
hic : IsIntegrallyClosed (Localization.AtPrime p)
hxp : IsIntegral (Localization.AtPrime p) (Localization.mk x.1 x.2)
⊢ 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
⊢ IsIntegrallyClosed R

Tactic:
apply (isIntegrallyClosed_iff (FractionRing R)).mpr

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