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

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

Tactic:
obtain ⟨m, hm⟩ := hK fun x hx => hJK <| Ideal.mem_sup_right hx

Result:
case refine_2.intro.intro
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I

Proof state:
case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
apply Ideal.mul_le_left.trans

Result:
case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ K ^ (n + m - i) ≤ I

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

Tactic:
refine Submodule.fg_induction _ _ (fun J => J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I) ?_ ?_ _ h

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

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

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

Tactic:
intro J K hJ hK hJK

Result:
case refine_2
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
⊢ ∃ n, (J ⊔ K) ^ n ≤ I

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

Tactic:
rw [← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup, Finset.sup_le_iff]

Result:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * ↑((n + m).choose b) ≤ I

Proof state:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * ↑((n + m).choose b) ≤ I

Tactic:
refine fun i _ => Ideal.mul_le_right.trans ?_

Result:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
⊢ J ^ i * K ^ (n + m - i) ≤ I

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

Tactic:
exact ⟨n, by rwa [← Ideal.span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩

Result:
no goals

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

Tactic:
obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| Ideal.mem_sup_left hx

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

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

Tactic:
have := le_refl I.radical

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

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

Tactic:
rwa [← Ideal.span, span_singleton_pow, span_le, Set.singleton_subset_iff]

Result:
no goals

Proof state:
case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ m ≤ m + (n - i)

Tactic:
apply Nat.le_add_right

Result:
no goals

Proof state:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
obtain h | h := le_or_lt n i

Result:
case h.inl
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : n ≤ i
⊢ J ^ i * K ^ (n + m - i) ≤ I

case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ J ^ i * K ^ (n + m - i) ≤ I

Proof state:
case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ K ^ (n + m - i) ≤ I

Tactic:
refine (Ideal.pow_le_pow_right ?_).trans hm

Result:
case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ m ≤ n + m - i

Proof state:
case h.inl
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : n ≤ i
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
apply Ideal.mul_le_right.trans ((Ideal.pow_le_pow_right h).trans hn)

Result:
no goals