-- Mathlib/RingTheory/Finiteness/Ideal.lean
lemma exists_pow_le_of_le_radical_of_fg {R : Type*} [CommSemiring R] {I J : Ideal R}
    (h' : I ≤ J.radical) (h : I.FG) :
    ∃ n : ℕ, I ^ n ≤ J

Proof state:
case h
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
I₁ I₂ : Submodule R R
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
hJ : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
n₂ : ℕ
hn₂ : I₂ ^ n₂ ≤ J
⊢ (I₁ ⊔ I₂) ^ (n₁ + n₂) ≤ J

Tactic:
exact Ideal.sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
I₁ I₂ : Submodule R R
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
hJ : I₁ ⊔ I₂ ≤ J.radical
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans hJ)

Result:
case intro
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
I₁ I₂ : Submodule R R
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
hJ : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
x : R
hJ : Submodule.span R {x} ≤ J.radical
⊢ ∃ n, Submodule.span R {x} ^ n ≤ J

Tactic:
simp only [Ideal.submodule_span_eq, Ideal.span_le,
  Set.singleton_subset_iff, SetLike.mem_coe] at hJ

Result:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
x : R
hJ : x ∈ J.radical
⊢ ∃ n, Submodule.span R {x} ^ n ≤ J

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
⊢ ∀ (M₁ M₂ : Submodule R R),
    (M₁ ≤ J.radical → ∃ n, M₁ ^ n ≤ J) →
      (M₂ ≤ J.radical → ∃ n, M₂ ^ n ≤ J) → M₁ ⊔ M₂ ≤ J.radical → ∃ n, (M₁ ⊔ M₂) ^ n ≤ J

Tactic:
intros I₁ I₂ h₁ h₂ hJ

Result:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
I₁ I₂ : Submodule R R
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
hJ : I₁ ⊔ I₂ ≤ J.radical
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Proof state:
case intro.intro
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
I₁ I₂ : Submodule R R
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
hJ : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
n₂ : ℕ
hn₂ : I₂ ^ n₂ ≤ J
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
use n₁ + n₂

Result:
case h
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
I₁ I₂ : Submodule R R
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
hJ : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
n₂ : ℕ
hn₂ : I₂ ^ n₂ ≤ J
⊢ (I₁ ⊔ I₂) ^ (n₁ + n₂) ≤ J

Proof state:
case intro
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
I₁ I₂ : Submodule R R
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
hJ : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans hJ)

Result:
case intro.intro
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
I₁ I₂ : Submodule R R
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
hJ : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
n₂ : ℕ
hn₂ : I₂ ^ n₂ ≤ J
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h' : I ≤ J.radical
h : I.FG
⊢ ∃ n, I ^ n ≤ J

Tactic:
revert h'

Result:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
⊢ I ≤ J.radical → ∃ n, I ^ n ≤ J

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
⊢ ∀ (x : R), Submodule.span R {x} ≤ J.radical → ∃ n, Submodule.span R {x} ^ n ≤ J

Tactic:
intro x hJ

Result:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
x : R
hJ : Submodule.span R {x} ≤ J.radical
⊢ ∃ n, Submodule.span R {x} ^ n ≤ J

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
⊢ I ≤ J.radical → ∃ n, I ^ n ≤ J

Tactic:
apply Submodule.fg_induction _ _ _ _ _ I h

Result:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
⊢ ∀ (x : R), Submodule.span R {x} ≤ J.radical → ∃ n, Submodule.span R {x} ^ n ≤ J

R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
⊢ ∀ (M₁ M₂ : Submodule R R),
    (M₁ ≤ J.radical → ∃ n, M₁ ^ n ≤ J) →
      (M₂ ≤ J.radical → ∃ n, M₂ ^ n ≤ J) → M₁ ⊔ M₂ ≤ J.radical → ∃ n, (M₁ ⊔ M₂) ^ n ≤ J

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
x : R
n : ℕ
hn : x ^ n ∈ J
⊢ Submodule.span R {x} ^ n ≤ J

Tactic:
simpa [Ideal.span_singleton_pow, Ideal.span_le]

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
x : R
hJ : x ∈ J.radical
⊢ ∃ n, Submodule.span R {x} ^ n ≤ J

Tactic:
obtain ⟨n, hn⟩ := hJ

Result:
case intro
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
x : R
n : ℕ
hn : x ^ n ∈ J
⊢ ∃ n, Submodule.span R {x} ^ n ≤ J

Proof state:
case intro
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
h : I.FG
x : R
n : ℕ
hn : x ^ n ∈ J
⊢ ∃ n, Submodule.span R {x} ^ n ≤ J

Tactic:
refine ⟨n, by simpa [Ideal.span_singleton_pow, Ideal.span_le]⟩

Result:
no goals