-- 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})
hf : Monotone f
⊢ a ∈ I ∨ b ∈ I.radical

Tactic:
obtain ⟨n, hn⟩ := monotone_stabilizes_iff_noetherian.mpr ‹_› ⟨f, hf⟩

Result:
case intro
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})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
⊢ a ∈ I ∨ b ∈ I.radical

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})
⊢ Monotone f

Tactic:
intro n m hnm

Result:
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
⊢ f n ≤ f m

Proof state:
case intro.intro
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
⊢ a ∈ I ∨ b ∈ I.radical

Tactic:
specialize @h (I.colon (span {b ^ n})) (I + (span {b ^ n})) ?_

Result:
case intro.intro
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
⊢ Submodule.colon I (span {b ^ n}) ⊓ (I + span {b ^ n}) = I

case intro.intro
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 + span {b ^ n} = I
⊢ a ∈ I ∨ b ∈ I.radical

Proof state:
case intro.intro
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 + span {b ^ n} = I
⊢ a ∈ I ∨ b ∈ I.radical

Tactic:
rcases h with (h|h)

Result:
case intro.intro.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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : Submodule.colon I (span {b ^ n}) = I
⊢ a ∈ I ∨ b ∈ I.radical

case intro.intro.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 : I + span {b ^ n} = I
⊢ a ∈ I ∨ b ∈ I.radical

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})
⊢ a ∈ I ∨ b ∈ I.radical

Tactic:
have hf : Monotone f := by
  intro n m hnm
  simp_rw [f]
  exact (Submodule.colon_mono le_rfl (Ideal.span_singleton_le_span_singleton.mpr
    (pow_dvd_pow b hnm)))

Result:
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})
hf : Monotone f
⊢ a ∈ I ∨ b ∈ I.radical

Proof state:
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
x✝ : R
⊢ x✝ ∈ I → x✝ ∈ Submodule.colon I (span {b})

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
r : R
⊢ r * b ^ n ∈ I → ∀ (x x_1 : R), x_1 ∈ I → x * b ^ n + x_1 = r → r ∈ I

Tactic:
rintro hrb t s hs rfl

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
⊢ t * b ^ n + s ∈ I

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

Tactic:
refine ⟨h.ne_top, fun {a b} hab ↦ ?_⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : InfIrred I
a b : R
hab : a * b ∈ I
⊢ a ∈ I ∨ b ∈ I.radical

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
r : R
⊢ r ∈ Submodule.colon I (span {b ^ n}) ⊓ (I + span {b ^ n}) → r ∈ I

Tactic:
simp only [Submodule.add_eq_sup, sup_comm I, mem_inf, mem_colon_singleton,
  mem_span_singleton_sup, and_imp, forall_exists_index]

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
r : R
⊢ r * b ^ n ∈ I → ∀ (x x_1 : R), x_1 ∈ I → x * b ^ n + x_1 = r → r ∈ I

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 : ∀ ⦃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
⊢ n ≤ n + n

Tactic:
simp

Result:
no goals