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

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

Tactic:
refine add_mem ?_ hs

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 ∈ I

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

Tactic:
refine le_antisymm (fun r ↦ ?_) (le_inf (fun _ ↦ ?_) ?_)

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

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})

case intro.intro.refine_3
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
⊢ I ≤ I + span {b ^ n}

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

Tactic:
let f : ℕ → Ideal R := fun n ↦ (I.colon (span {b ^ n}))

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

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

Tactic:
rw [← h]

Result:
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 + span {b ^ n} ∨ b ∈ (I + span {b ^ n}).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
⊢ I ≤ Submodule.colon I (span {b})

Tactic:
intro

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

Proof state:
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 + span {b ^ n} ∨ b ∈ (I + span {b ^ n}).radical

Tactic:
refine Or.inr ⟨n, ?_⟩

Result:
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
⊢ b ^ n ∈ I + span {b ^ n}

Proof state:
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
⊢ b ^ n ∈ I + span {b ^ n}

Tactic:
simpa using mem_sup_right (mem_span_singleton_self _)

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 * 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 = Submodule.colon I (span {b})
⊢ a ∈ I ∨ b ∈ I.radical

Tactic:
rw [← mem_colon_singleton, ← h] at hab

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

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

Tactic:
rcases h with ⟨-, h⟩

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