diff --git a/Mathlib/Algebra/Homology/LocalCohomology.lean b/Mathlib/Algebra/Homology/LocalCohomology.lean
index 2f79abd6cd9080..0fd9c317ded471 100644
--- a/Mathlib/Algebra/Homology/LocalCohomology.lean
+++ b/Mathlib/Algebra/Homology/LocalCohomology.lean
@@ -219,7 +219,7 @@ def idealPowersToSelfLERadical (J : Ideal R) : ℕᵒᵖ ⥤ SelfLERadical J :=
     change _ ≤ (J ^ unop k).radical
     cases' unop k with n
     · simp [Ideal.radical_top, pow_zero, Ideal.one_eq_top, le_top, Nat.zero_eq]
-    · simp only [J.radical_pow _ n.succ_pos, Ideal.le_radical]
+    · simp only [J.radical_pow n.succ_ne_zero, Ideal.le_radical]
 #align local_cohomology.ideal_powers_to_self_le_radical localCohomology.idealPowersToSelfLERadical
 
 variable {I J K : Ideal R}
diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
index 19d33ce9ac55f0..e2f955dcca14b8 100644
--- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
+++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
@@ -374,9 +374,9 @@ theorem zeroLocus_singleton_mul (f g : R) :
 #align prime_spectrum.zero_locus_singleton_mul PrimeSpectrum.zeroLocus_singleton_mul
 
 @[simp]
-theorem zeroLocus_pow (I : Ideal R) {n : ℕ} (hn : 0 < n) :
+theorem zeroLocus_pow (I : Ideal R) {n : ℕ} (hn : n ≠ 0) :
     zeroLocus ((I ^ n : Ideal R) : Set R) = zeroLocus I :=
-  zeroLocus_radical (I ^ n) ▸ (I.radical_pow n hn).symm ▸ zeroLocus_radical I
+  zeroLocus_radical (I ^ n) ▸ (I.radical_pow hn).symm ▸ zeroLocus_radical I
 #align prime_spectrum.zero_locus_pow PrimeSpectrum.zeroLocus_pow
 
 @[simp]
diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
index 9ed0a0bc8d6526..bc05e153db2131 100644
--- a/Mathlib/RingTheory/Ideal/Operations.lean
+++ b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -1092,20 +1092,9 @@ variable {R}
 
 variable (I)
 
-theorem radical_pow (n : ℕ) (H : n > 0) : radical (I ^ n) = radical I :=
-  Nat.recOn n (Not.elim (by decide))
-    (fun n ih H =>
-      Or.casesOn (lt_or_eq_of_le <| Nat.le_of_lt_succ H)
-        (fun H =>
-          calc
-            radical (I ^ (n + 1)) = radical I ⊓ radical (I ^ n) := by
-              rw [pow_succ]
-              exact radical_mul _ _
-            _ = radical I ⊓ radical I := by rw [ih H]
-            _ = radical I := inf_idem
-            )
-        fun H => H ▸ (pow_one I).symm ▸ rfl)
-    H
+lemma radical_pow : ∀ {n}, n ≠ 0 → radical (I ^ n) = radical I
+  | 1, _ => by simp
+  | n + 2, _ => by rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]
 #align ideal.radical_pow Ideal.radical_pow
 
 theorem IsPrime.mul_le {I J P : Ideal R} (hp : IsPrime P) : I * J ≤ P ↔ I ≤ P ∨ J ≤ P := by