mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
x : R
hx : (Quotient.mk I) x ∈ ↑p'
⊢ x ∈ ↑p ∧ (Quotient.mk I) x = (Quotient.mk I) x

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
x : R
hx : (Quotient.mk I) x ∈ ↑p'
⊢ x ∈ p
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨closedPoint R, ⋯⟩).asIdeal.height ≤ 1
⊢ (e ⟨p₁, ⋯⟩).asIdeal < (e ⟨closedPoint R, ⋯⟩).asIdeal

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨closedPoint R, ⋯⟩).asIdeal.height ≤ 1
⊢ p₁ < closedPoint R
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨closedPoint R, ⋯⟩).asIdeal.height ≤ 1
hph : (e ⟨p₁, ⋯⟩).asIdeal.height ≤ 0
⊢ (e ⟨p₀, ⋯⟩).asIdeal < (e ⟨p₁, ⋯⟩).asIdeal

Tactic:
simpa using

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨closedPoint R, ⋯⟩).asIdeal.height ≤ 1
hph : (e ⟨p₁, ⋯⟩).asIdeal.height ≤ 0
⊢ p₀ < p₁
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ RelSeries.head p = (RelSeries.snoc Q (RelSeries.last p) ⋯).head

Tactic:
by simp [← hh]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: case nil
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M []
⊢ supportDim R (M ⧸ ⊥) + ↑[].length = supportDim R M

Tactic:
simpa using

Goal state after:
case nil
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M []
⊢ supportDim R (M ⧸ ⊥) = supportDim R M
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
x : R
rs' : List R
ih :
  ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module R M] [Module.Finite R M],
    Sequence.IsRegular M rs' → supportDim R (M ⧸ ofList rs' • ⊤) + ↑rs'.length = supportDim R M
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M (x :: rs')
⊢ x ∈ maximalIdeal R

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
x : R
rs' : List R
ih :
  ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module R M] [Module.Finite R M],
    Sequence.IsRegular M rs' → supportDim R (M ⧸ ofList rs' • ⊤) + ↑rs'.length = supportDim R M
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M (x :: rs')
⊢ ¬IsUnit x
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ∀ (g : ↥R), g * ⟨y, hy⟩ = ⟨y, hy⟩ * g
⊢ x * y = y * x

Tactic:
simpa using

Goal state after:
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ∀ (g : ↥R), g * ⟨y, hy⟩ = ⟨y, hy⟩ * g
⊢ x * y = y * x
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : ⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
this : { asIdeal := q, isPrime := hq } ∈ ⨆ i, PrimeSpectrum.basicOpen (f i)
⊢ ∃ i, f i ∉ q

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : ⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
this : { asIdeal := q, isPrime := hq } ∈ ⨆ i, PrimeSpectrum.basicOpen (f i)
⊢ ∃ i, f i ∉ q
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹² : CommRing R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst✝⁹ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁸ : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (Rₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type v'
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝² : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Rₚ I) (Mₚ I)
⊢ ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)

Tactic:
intro P hP

Goal state after:
R : Type u
inst✝¹² : CommRing R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst✝⁹ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁸ : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (Rₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type v'
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝² : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Rₚ I) (Mₚ I)
P : Ideal R
hP : P.IsMaximal
⊢ Injective (Localization.AtPrime P) (LocalizedModule P.primeCompl M)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
X : ModuleCat R
inj : Module.Injective R ↑X
x✝ : Small.{v, u} (Localization S) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Injective (Localization S) ↑((localizedModuleFunctor S).1 X)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
X : ModuleCat R
inj : Module.Injective R ↑X
x✝ : Small.{v, u} (Localization S) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Injective (Localization S) ↑(X.localizedModule S)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑↑n → injectiveDimension (M.localizedModule S) ≤ ↑↑n

Tactic:
simpa using

Goal state after:
case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑↑n → injectiveDimension (M.localizedModule S) ≤ ↑↑n

Tactic:
| coe n =>

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Injective (Localization.AtPrime p) ↑(M.localizedModule p.primeCompl)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
⊢ Injective (M.localizedModule p.primeCompl)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
simpa using

Goal state after:
case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑n ↔ ∀ (i : PrimeSpectrum R), injectiveDimension (M.localizedModule i.asIdeal.primeCompl) ≤ ↑n
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
| coe n =>

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X : ModuleCat R
proj : Module.Projective R ↑X
this : Small.{v, u} (Localization S)
⊢ Module.Projective (Localization S) ↑((localizedModuleFunctor S).1 X)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X : ModuleCat R
proj : Module.Projective R ↑X
this : Small.{v, u} (Localization S)
⊢ Module.Projective (Localization S) ↑(X.localizedModule S)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
simpa using

Goal state after:
case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑n ↔
    ∀ (i : MaximalSpectrum R), injectiveDimension (M.localizedModule i.asIdeal.primeCompl) ≤ ↑n
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
| coe n =>

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑↑n → projectiveDimension (M.localizedModule S) ≤ ↑↑n

Tactic:
simpa using

Goal state after:
case coe.coe
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑↑n → projectiveDimension (M.localizedModule S) ≤ ↑↑n

Tactic:
| coe n =>

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)
this✝ : Module.FinitePresentation R ↑M
p : Ideal R
hp : p.IsMaximal
this : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Projective (Localization.AtPrime p) ↑(M.localizedModule p.primeCompl)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)
this✝ : Module.FinitePresentation R ↑M
p : Ideal R
hp : p.IsMaximal
this : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
⊢ Projective (M.localizedModule p.primeCompl)
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ (frac { asIdeal := P, isMaximal := hP } ↑x).1 ∈
    ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ ∃ i, ∃ x_1 ∈ s i, (frac i x_1).1 = (frac { asIdeal := P, isMaximal := hP } ↑x).1
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
simpa using

Goal state after:
case coe.coe
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑n ↔
    ∀ (i : PrimeSpectrum R), projectiveDimension (M.localizedModule i.asIdeal.primeCompl) ≤ ↑n
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
| coe n =>

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
simpa using

Goal state after:
case coe.coe
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑n ↔
    ∀ (i : MaximalSpectrum R), projectiveDimension (M.localizedModule i.asIdeal.primeCompl) ≤ ↑n
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
h : IsUnit fun i ↦ if i = i₁ then 0 else 1
⊢ IsUnit 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
h : IsUnit fun i ↦ if i = i₁ then 0 else 1
⊢ False
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
h : IsUnit fun i ↦ if i = i₁ then 1 else 0
⊢ IsUnit 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
h : IsUnit fun i ↦ if i = i₁ then 1 else 0
⊢ False