case intro
R : Type u
inst✝ : CommRing R
I J : Ideal R
hIJ : I ≤ radical J
hJ : FG (radical J)
k : ℕ
hk : radical J ^ k ≤ J
⊢ ∃ k, I ^ k ≤ J
R : Type u
inst✝ : CommRing R
I J : Ideal R
hIJ : I ≤ radical J
hJ : FG (radical J)
⊢ ∃ k, I ^ k ≤ J
obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ
case intro
R : Type u
inst✝ : CommRing R
I J : Ideal R
hIJ : I ≤ radical J
hJ : FG (radical J)
k : ℕ
hk : radical J ^ k ≤ J
⊢ I ^ k ≤ J
case intro
R : Type u
inst✝ : CommRing R
I J : Ideal R
hIJ : I ≤ radical J
hJ : FG (radical J)
k : ℕ
hk : radical J ^ k ≤ J
⊢ ∃ k, I ^ k ≤ J
use k
no goals
case intro
R : Type u
inst✝ : CommRing R
I J : Ideal R
hIJ : I ≤ radical J
hJ : FG (radical J)
k : ℕ
hk : radical J ^ k ≤ J
⊢ I ^ k ≤ J
calc
  I ^ k ≤ J.radical ^ k := Ideal.pow_mono hIJ _
  _ ≤ J := hk