awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
bot :
  Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
⊢ injectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥

Tactic:
simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, Equiv.subsingleton_congr, CategoryTheory.injectiveDimension_eq_bot_iff, ModuleCat.localizedModule, equivShrink, iSup_eq_bot
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))

Tactic:
⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩

Premises used: MaximalSpectrum.asIdeal, LocalizedModule.instSubsingleton, Iff.intro, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
bot :
  ∀ (h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))),
    Subsingleton.{v + 1} (↑M : Type v)
⊢ Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))

Tactic:
refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
bot : ∀ (P : Ideal R) [inst_3 : P.IsMaximal], Subsingleton (LocalizedModule.{u, v} P.primeCompl (↑M : Type v))
⊢ Subsingleton.{v + 1} (↑M : Type v)

Tactic:
apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)

Premises used: Module.subsingleton_of_localization_maximal, LocalizedModule, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
p : Ideal R
hp : p.IsMaximal
⊢ Subsingleton (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
h ⟨p, hp⟩

Premises used: MaximalSpectrum.mk
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
p : Ideal R
hp : p.IsMaximal
⊢ Subsingleton (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
exact h ⟨p, hp⟩

Premises used: MaximalSpectrum.mk
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ injectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑⊤ : WithBot ℕ∞)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
n : ℕ
⊢ injectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑(↑n : ℕ∞) : WithBot ℕ∞)

Tactic:
simpa using aux n
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : ℕ∞
coe :
  injectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑⊤ : WithBot ℕ∞)
coe₁ :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑(↑n : ℕ∞) : WithBot ℕ∞)
⊢ injectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)

Tactic:
induction N with
    | top => simp
    | coe n => simpa using aux n
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
bot :
  injectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
coe :
  ∀ (N : ℕ∞),
    injectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
      ⨆ (p : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl) ≤
        (↑N : WithBot ℕ∞)
⊢ injectiveDimension M ≤ N ↔
    ⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N

Tactic:
induction N with
  | bot =>
    simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, Module.subsingleton_of_localization_maximal, LocalizedModule, Equiv.subsingleton_congr, ModuleCat.carrier, CategoryTheory.injectiveDimension_eq_bot_iff, LocalizedModule.mkLinearMap, Ideal.primeCompl, ModuleCat.localizedModule, equivShrink, iSup_eq_bot
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
⊢ IsIntegrallyClosed.{u_2} ↥(⨅ (i : ι), S i)

Tactic:
(isIntegrallyClosed_iff K).mpr (fun {x} hx ↦ CanLift.prf x (Algebra.mem_iInf.mpr ?_))

Premises used: Iff.mpr, Algebra.mem_iInf, isIntegrallyClosed_iff, CanLift.prf
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
refine : ∀ {x : K} (hx : IsIntegral (↥(⨅ (i : ι), S i)) x) (i : ι), x ∈ S i
⊢ IsIntegrallyClosed.{u_2} ↥(⨅ (i : ι), S i)

Tactic:
refine (isIntegrallyClosed_iff K).mpr (fun {x} hx ↦ CanLift.prf x (Algebra.mem_iInf.mpr ?_))

Premises used: Iff.mpr, Algebra.mem_iInf, isIntegrallyClosed_iff, CanLift.prf
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
x : K
hx : IsIntegral (↥(⨅ (i : ι), S i)) x
i : ι
⊢ ⨅ (i : ι), S i ≤ S i

Tactic:
have le : (⨅ i : ι, S i : Subalgebra R K) ≤ S i := iInf_le S i
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
x : K
hx : IsIntegral (↥(⨅ (i : ι), S i)) x
i : ι
le : ⨅ (i : ι), S i ≤ S i
algInst : Algebra ↥(⨅ (i : ι), S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
⊢ IsScalarTower (↥(⨅ (i : ι), S i)) (↥(S i)) K

Tactic:
have : IsScalarTower ↥(⨅ i, S i) (S i) K := Subalgebra.inclusion.isScalarTower_right le K
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
x : K
hx : IsIntegral (↥(⨅ (i : ι), S i)) x
i : ι
le : ⨅ (i : ι), S i ≤ S i
algInst : Algebra ↥(⨅ (i : ι), S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
this : IsScalarTower (↥(⨅ (i : ι), S i)) (↥(S i)) K
rcases :
  ∀ (val : K) (hin : val ∈ S i)
    (hy : (algebraMap (↥(S i)) K : (a : ↥(S i)) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ S i) val hin) = x), x ∈ S i
⊢ x ∈ S i

Tactic:
rcases (isIntegrallyClosed_iff K).mp (h i) hx.tower_top with ⟨⟨_, hin⟩, hy⟩

Premises used: Iff.mp, isIntegrallyClosed_iff, IsIntegral.tower_top
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
x : K
hx : IsIntegral (↥(⨅ (i : ι), S i)) x
i : ι
le : ⨅ (i : ι), S i ≤ S i
algInst : Algebra ↥(⨅ (i : ι), S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
this : IsScalarTower (↥(⨅ (i : ι), S i)) (↥(S i)) K
val : K
hin : val ∈ S i
hy : (algebraMap (↥(S i)) K : (a : ↥(S i)) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ S i) val hin) = x
rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (α := K) (S i)
    ((algebraMap (↥(S i)) K : (a : ↥(S i)) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ S i) val hin) : K)
⊢ x ∈ S i

Tactic:
rwa [← hy]
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
hs : Eq.{u_2 + 1} (α := Subalgebra R K) (⨅ (i : ι), S i) ⊥
⊢ IsIntegrallyClosed R

Tactic:
have f : (⊥ : Subalgebra R K) ≃ₐ[R] R :=
    Algebra.botEquivOfInjective (FaithfulSMul.algebraMap_injective R K)
  (IsIntegrallyClosed.iInf S h).of_equiv (hs ▸ f).toRingEquiv

Premises used: Algebra.botEquivOfInjective, IsIntegrallyClosed.of_equiv, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ι : Type u_3
S : ι → Submonoid R
h : ∀ (i : ι), S i ≤ R⁰
hi : ∀ (i : ι), IsIntegrallyClosed.{u_1} (Localization (M := R) (S i))
hs : Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R)) (⨅ (i : ι), subalgebra (FractionRing R) (S i) ⋯) ⊥
⊢ IsIntegrallyClosed R

Tactic:
IsIntegrallyClosed.of_iInf_eq_bot (fun i ↦ Localization.subalgebra (FractionRing R) (S i) (h i))
    (fun i ↦ (hi i).of_equiv (IsLocalization.algEquiv (S i) (Localization (S i)) _).toRingEquiv) hs

Premises used: FractionRing, Membership.mem, Localization.subalgebra, Subtype, Localization, IsIntegrallyClosed.of_equiv, IsLocalization.algEquiv, AlgEquiv.toRingEquiv, IsIntegrallyClosed.of_iInf_eq_bot
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Set (PrimeSpectrum R)
h : ∀ p ∈ S, IsIntegrallyClosed.{u_1} (Localization.AtPrime p.asIdeal)
hs : Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R)) (⨅ p ∈ S, subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯) ⊥
apply :
  Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (i : (↑S : Type u_1)), subalgebra (FractionRing R) (↑i : PrimeSpectrum R).asIdeal.primeCompl ⋯) ⊥
⊢ IsIntegrallyClosed R

Tactic:
apply IsIntegrallyClosed.of_localization_submonoid (fun p : S ↦ p.1.1.primeCompl)
    (fun p ↦ p.1.1.primeCompl_le_nonZeroDivisors) (fun p ↦ h p.1 p.2)

Premises used: IsIntegrallyClosed.of_localization_submonoid, Ideal.primeCompl_le_nonZeroDivisors, Ideal.primeCompl, Subtype.val, PrimeSpectrum.asIdeal, Subtype.property
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Set (PrimeSpectrum R)
h : ∀ p ∈ S, IsIntegrallyClosed.{u_1} (Localization.AtPrime p.asIdeal)
hs : Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R)) (⨅ p ∈ S, subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯) ⊥
h₁ :
  ∀ (x : FractionRing R),
    Membership.mem (γ := Subalgebra R (FractionRing R))
        (⨅ (i : (↑S : Type u_1)), subalgebra (FractionRing R) (↑i : PrimeSpectrum R).asIdeal.primeCompl ⋯) x ↔
      Membership.mem (γ := Subalgebra R (FractionRing R)) ⊥ x
⊢ Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (i : (↑S : Type u_1)), subalgebra (FractionRing R) (↑i : PrimeSpectrum R).asIdeal.primeCompl ⋯) ⊥

Tactic:
ext x
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Set (PrimeSpectrum R)
h : ∀ p ∈ S, IsIntegrallyClosed.{u_1} (Localization.AtPrime p.asIdeal)
hs : Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R)) (⨅ p ∈ S, subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯) ⊥
x : FractionRing R
⊢ Membership.mem (γ := Subalgebra R (FractionRing R))
      (⨅ (i : (↑S : Type u_1)), subalgebra (FractionRing R) (↑i : PrimeSpectrum R).asIdeal.primeCompl ⋯) x ↔
    Membership.mem (γ := Subalgebra R (FractionRing R)) ⊥ x

Tactic:
simp only [← hs, Algebra.mem_iInf, Subtype.forall]

Premises used: Algebra.mem_iInf, Subtype.forall
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
pos : ∀ (hf : IsField R), IsIntegrallyClosed R
neg : ∀ (hf : ¬IsField R), IsIntegrallyClosed R
⊢ IsIntegrallyClosed R

Tactic:
by_cases hf : IsField R

Premises used: IsField
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : IsField R
⊢ IsIntegrallyClosed R

Tactic:
hf.toField.instIsIntegrallyClosed

Premises used: Field.instIsIntegrallyClosed
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : IsField R
⊢ IsIntegrallyClosed R

Tactic:
exact hf.toField.instIsIntegrallyClosed

Premises used: Field.instIsIntegrallyClosed
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
⊢ IsIntegrallyClosed R

Tactic:
of_localization (.range MaximalSpectrum.toPrimeSpectrum) (fun _ ↦ ?_) ?_

Premises used: IsIntegrallyClosed.of_localization, MaximalSpectrum.toPrimeSpectrum, Set.range
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
neg :
  ∀ (x : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range MaximalSpectrum.toPrimeSpectrum) x →
      IsIntegrallyClosed.{u_1} (Localization.AtPrime x.asIdeal)
neg₁ :
  Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (p : PrimeSpectrum R),
      ⨅ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range MaximalSpectrum.toPrimeSpectrum) p),
        subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯)
    ⊥
⊢ IsIntegrallyClosed R

Tactic:
refine of_localization (.range MaximalSpectrum.toPrimeSpectrum) (fun _ ↦ ?_) ?_

Premises used: IsIntegrallyClosed.of_localization, MaximalSpectrum.toPrimeSpectrum, Set.range
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
p : MaximalSpectrum R
⊢ IsIntegrallyClosed.{u_1} (Localization.AtPrime p.toPrimeSpectrum.asIdeal)

Tactic:
h p.asIdeal (Ring.ne_bot_of_isMaximal_of_not_isField p.isMaximal hf)

Premises used: MaximalSpectrum.asIdeal, Ring.ne_bot_of_isMaximal_of_not_isField, MaximalSpectrum.isMaximal
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
p : MaximalSpectrum R
⊢ IsIntegrallyClosed.{u_1} (Localization.AtPrime p.toPrimeSpectrum.asIdeal)

Tactic:
exact h p.asIdeal (Ring.ne_bot_of_isMaximal_of_not_isField p.isMaximal hf)

Premises used: MaximalSpectrum.asIdeal, Ring.ne_bot_of_isMaximal_of_not_isField, MaximalSpectrum.isMaximal
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
neg :
  Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (i : MaximalSpectrum R), subalgebra (FractionRing R) i.toPrimeSpectrum.asIdeal.primeCompl ⋯) ⊥
⊢ Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (p : PrimeSpectrum R),
      ⨅ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range MaximalSpectrum.toPrimeSpectrum) p),
        subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯)
    ⊥

Tactic:
rw [iInf_range]

Premises used: iInf_range
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
⊢ Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (v : MaximalSpectrum R), subalgebra.ofField (FractionRing R) v.asIdeal.primeCompl ⋯) ⊥

Tactic:
MaximalSpectrum.iInf_localization_eq_bot R (FractionRing R)

Premises used: FractionRing, MaximalSpectrum.iInf_localization_eq_bot
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
h₁ :
  ∀ (x : MaximalSpectrum R),
    Eq (α := Subalgebra R (FractionRing R))
      (subalgebra (FractionRing R) x.toPrimeSpectrum.asIdeal.primeCompl ⋯ : Subalgebra R (FractionRing R))
      (subalgebra.ofField (FractionRing R) x.asIdeal.primeCompl ⋯ : Subalgebra R (FractionRing R))
⊢ Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (i : MaximalSpectrum R), subalgebra (FractionRing R) i.toPrimeSpectrum.asIdeal.primeCompl ⋯) ⊥

Tactic:
convert! MaximalSpectrum.iInf_localization_eq_bot R (FractionRing R)

Premises used: FractionRing, MaximalSpectrum.iInf_localization_eq_bot