-- Mathlib/RingTheory/Lasker.lean
lemma _root_.InfIrred.isPrimary {I : Ideal R} (h : InfIrred I) : I.IsPrimary

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : InfIrred I
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
n m : ℕ
hnm : n ≤ m
⊢ Submodule.colon I (span {b ^ n}) ≤ Submodule.colon I (span {b ^ m})

Tactic:
exact (Submodule.colon_mono le_rfl (Ideal.span_singleton_le_span_singleton.mpr
  (pow_dvd_pow b hnm)))

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : Submodule.colon I (span {b ^ n}) = I
⊢ I = Submodule.colon I (span {b})

Tactic:
rcases eq_or_ne n 0 with rfl|hn'

Result:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
hn : ∀ (m : ℕ), 0 ≤ m → { toFun := f, monotone' := hf } 0 = { toFun := f, monotone' := hf } m
h : Submodule.colon I (span {b ^ 0}) = I
⊢ I = Submodule.colon I (span {b})

case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : Submodule.colon I (span {b ^ n}) = I
hn' : n ≠ 0
⊢ I = Submodule.colon I (span {b})

Proof state:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : Submodule.colon I (span {b ^ n}) = I
hn' : n ≠ 0
⊢ I = Submodule.colon I (span {b})

Tactic:
refine le_antisymm ?_ (h.le.trans' (Submodule.colon_mono le_rfl ?_))

Result:
case inr.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : Submodule.colon I (span {b ^ n}) = I
hn' : n ≠ 0
⊢ I ≤ Submodule.colon I (span {b})

case inr.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : Submodule.colon I (span {b ^ n}) = I
hn' : n ≠ 0
⊢ span {b ^ n} ≤ span {b}

Proof state:
case intro.intro.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Ideal R⦄, b ⊓ c = I → b = I ∨ c = I
x✝ : R
⊢ x✝ ∈ I → x✝ ∈ Submodule.colon I (span {b ^ n})

Tactic:
simpa only [mem_colon_singleton] using mul_mem_right _ _

Result:
no goals

Proof state:
case intro.intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Ideal R⦄, b ⊓ c = I → b = I ∨ c = I
t s : R
hs : s ∈ I
hrb : (t * b ^ n + s) * b ^ n ∈ I
this : { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } (n + n)
⊢ t * b ^ n ∈ I

Tactic:
simp only [OrderHom.coe_mk, f] at this

Result:
case intro.intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Ideal R⦄, b ⊓ c = I → b = I ∨ c = I
t s : R
hs : s ∈ I
hrb : (t * b ^ n + s) * b ^ n ∈ I
this : Submodule.colon I (span {b ^ n}) = Submodule.colon I (span {b ^ (n + n)})
⊢ t * b ^ n ∈ I

Proof state:
case intro.intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Ideal R⦄, b ⊓ c = I → b = I ∨ c = I
t s : R
hs : s ∈ I
hrb : (t * b ^ n + s) * b ^ n ∈ I
this : Submodule.colon I (span {b ^ n}) = Submodule.colon I (span {b ^ (n + n)})
⊢ t * b ^ n ∈ I

Tactic:
rw [add_mul, mul_assoc, ← pow_add] at hrb

Result:
case intro.intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Ideal R⦄, b ⊓ c = I → b = I ∨ c = I
t s : R
hs : s ∈ I
hrb : t * b ^ (n + n) + s * b ^ n ∈ I
this : Submodule.colon I (span {b ^ n}) = Submodule.colon I (span {b ^ (n + n)})
⊢ t * b ^ n ∈ I

Proof state:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
hn : ∀ (m : ℕ), 0 ≤ m → { toFun := f, monotone' := hf } 0 = { toFun := f, monotone' := hf } m
h : Submodule.colon I (span {b ^ 0}) = I
⊢ I = Submodule.colon I (span {b})

Tactic:
simpa [f] using hn 1 zero_le_one

Result:
no goals

Proof state:
case intro.intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Ideal R⦄, b ⊓ c = I → b = I ∨ c = I
t s : R
hs : s ∈ I
hrb : t * b ^ (n + n) + s * b ^ n ∈ I
this : Submodule.colon I (span {b ^ n}) = Submodule.colon I (span {b ^ (n + n)})
⊢ t * b ^ n ∈ I

Tactic:
rwa [← mem_colon_singleton, this, mem_colon_singleton,
     ← Ideal.add_mem_iff_left _ (Ideal.mul_mem_right _ _ hs)]

Result:
no goals

Proof state:
case intro.intro.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : I = Submodule.colon I (span {b})
⊢ a ∈ I ∨ b ∈ I.radical

Tactic:
exact Or.inl hab

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : InfIrred I
⊢ I.IsPrimary

Tactic:
rw [Ideal.isPrimary_iff]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : InfIrred I
⊢ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Proof state:
case inr.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : Submodule.colon I (span {b ^ n}) = I
hn' : n ≠ 0
⊢ span {b ^ n} ≤ span {b}

Tactic:
exact span_singleton_le_span_singleton.mpr (dvd_pow_self b hn')

Result:
no goals