R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
this : radical I ≤ radical I
⊢ ∃ n, radical I ^ n ≤ I
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
⊢ ∃ n, radical I ^ n ≤ I
have := le_refl I.radical
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
⊢ radical I ≤ radical I → ∃ n, radical I ^ n ≤ I
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
this : radical I ≤ radical I
⊢ ∃ n, radical I ^ n ≤ I
revert this
case refine'_1
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
⊢ ∀ (x : R), (fun J => J ≤ radical I → ∃ n, J ^ n ≤ I) (Submodule.span R {x})

case refine'_2
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
⊢ ∀ (M₁ M₂ : Submodule R R),
    (fun J => J ≤ radical I → ∃ n, J ^ n ≤ I) M₁ →
      (fun J => J ≤ radical I → ∃ n, J ^ n ≤ I) M₂ → (fun J => J ≤ radical I → ∃ n, J ^ n ≤ I) (M₁ ⊔ M₂)
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
⊢ radical I ≤ radical I → ∃ n, radical I ^ n ≤ I
refine' Submodule.fg_induction _ _ (fun J => J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I) _ _ _ h
case refine'_1
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
x : R
hx : Submodule.span R {x} ≤ radical I
⊢ ∃ n, Submodule.span R {x} ^ n ≤ I
case refine'_1
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
⊢ ∀ (x : R), (fun J => J ≤ radical I → ∃ n, J ^ n ≤ I) (Submodule.span R {x})
intro x hx
case refine'_1.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
x : R
hx : Submodule.span R {x} ≤ radical I
n : ℕ
hn : x ^ n ∈ I
⊢ ∃ n, Submodule.span R {x} ^ n ≤ I
case refine'_1
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
x : R
hx : Submodule.span R {x} ≤ radical I
⊢ ∃ n, Submodule.span R {x} ^ n ≤ I
obtain ⟨n, hn⟩ := hx (subset_span (Set.mem_singleton x))
no goals
case refine'_1.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
x : R
hx : Submodule.span R {x} ≤ radical I
n : ℕ
hn : x ^ n ∈ I
⊢ ∃ n, Submodule.span R {x} ^ n ≤ I
exact ⟨n, by rwa [← Ideal.span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩
no goals
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
x : R
hx : Submodule.span R {x} ≤ radical I
n : ℕ
hn : x ^ n ∈ I
⊢ Submodule.span R {x} ^ n ≤ I
rwa [← Ideal.span, span_singleton_pow, span_le, Set.singleton_subset_iff]
case refine'_2
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I
case refine'_2
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
⊢ ∀ (M₁ M₂ : Submodule R R),
    (fun J => J ≤ radical I → ∃ n, J ^ n ≤ I) M₁ →
      (fun J => J ≤ radical I → ∃ n, J ^ n ≤ I) M₂ → (fun J => J ≤ radical I → ∃ n, J ^ n ≤ I) (M₁ ⊔ M₂)
intro J K hJ hK hJK
case refine'_2.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
n : ℕ
hn : J ^ n ≤ I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I
case refine'_2
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I
obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| Ideal.mem_sup_left hx
case refine'_2.intro.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I
case refine'_2.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
n : ℕ
hn : J ^ n ≤ I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I
obtain ⟨m, hm⟩ := hK fun x hx => hJK <| Ideal.mem_sup_right hx
case refine'_2.intro.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ (J ⊔ K) ^ (n + m) ≤ I
case refine'_2.intro.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I
use n + m
case refine'_2.intro.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∀ (b : ℕ), b ∈ Finset.range (n + m + 1) → J ^ b * K ^ (n + m - b) * ↑(Nat.choose (n + m) b) ≤ I
case refine'_2.intro.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ (J ⊔ K) ^ (n + m) ≤ I
rw [← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup, Finset.sup_le_iff]
case refine'_2.intro.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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
case refine'_2.intro.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∀ (b : ℕ), b ∈ Finset.range (n + m + 1) → J ^ b * K ^ (n + m - b) * ↑(Nat.choose (n + m) b) ≤ I
refine' fun i _ => Ideal.mul_le_right.trans _
case refine'_2.intro.intro.inl
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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 refine'_2.intro.intro.inr
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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
case refine'_2.intro.intro
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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
obtain h | h := le_or_lt n i
no goals
case refine'_2.intro.intro.inl
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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
apply Ideal.mul_le_right.trans ((Ideal.pow_le_pow h).trans hn)
case refine'_2.intro.intro.inr
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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
case refine'_2.intro.intro.inr
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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
apply Ideal.mul_le_left.trans
case refine'_2.intro.intro.inr
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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
case refine'_2.intro.intro.inr
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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
refine' (Ideal.pow_le_pow _).trans hm
case refine'_2.intro.intro.inr
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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)
case refine'_2.intro.intro.inr
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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
rw [add_comm, Nat.add_sub_assoc h.le]
no goals
case refine'_2.intro.intro.inr
R✝ : Type ?u.375076
M : Type ?u.375079
inst✝³ : Semiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h✝ : FG (radical I)
J K : Submodule R R
hJ : J ≤ radical I → ∃ n, J ^ n ≤ I
hK : K ≤ radical I → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ radical I
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)
apply Nat.le_add_right