feat(Algebra/Order/Ring/WithTop): add generalised and specialised power of top (#14019)

- [x] Add generalised version of `top_pow` in `Algebra/Order/Ring/WithTop`
- [x] Add specialised version of `top_pow` in `Data/ENat/Basic.lean`
- [x] Add specialised version of `top_pow` in `Data/ENNReal/Operations.lean` 

Co-authored by @D-Thomine.

Author: pitmonticone

Mathlib/Algebra/Order/Ring/WithTop.lean

@@ -167,6 +167,10 @@ instance instMonoidWithZero : MonoidWithZero (WithTop α) where
 
 @[simp, norm_cast] lemma coe_pow (a : α) (n : ℕ) : (↑(a ^ n) : WithTop α) = a ^ n := rfl
 
+theorem top_pow {n : ℕ} (n_pos : 0 < n) : (⊤ : WithTop α) ^ n = ⊤ :=
+  Nat.le_induction (pow_one _) (fun m _ hm => by rw [pow_succ, hm, top_mul_top]) _
+    (Nat.succ_le_of_lt n_pos)
+
 end MonoidWithZero
 
 instance instCommMonoidWithZero [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :

Mathlib/Data/ENNReal/Operations.lean

@@ -219,10 +219,7 @@ theorem top_mul_top : ∞ * ∞ = ∞ := WithTop.top_mul_top
 #align ennreal.top_mul_top ENNReal.top_mul_top
 
 -- Porting note (#11215): TODO: assume `n ≠ 0` instead of `0 < n`
--- Porting note (#11215): TODO: generalize to `WithTop`
-theorem top_pow {n : ℕ} (h : 0 < n) : ∞ ^ n = ∞ :=
-  Nat.le_induction (pow_one _) (fun m _ hm => by rw [pow_succ, hm, top_mul_top]) _
-    (Nat.succ_le_of_lt h)
+theorem top_pow {n : ℕ} (n_pos : 0 < n) : (∞ : ℝ≥0∞) ^ n = ∞ := WithTop.top_pow n_pos
 #align ennreal.top_pow ENNReal.top_pow
 
 theorem mul_eq_top : a * b = ∞ ↔ a ≠ 0 ∧ b = ∞ ∨ a = ∞ ∧ b ≠ 0 :=

Mathlib/Data/ENat/Basic.lean

@@ -89,6 +89,8 @@ theorem coe_sub (m n : ℕ) : ↑(m - n) = (m - n : ℕ∞) :=
 @[simp] theorem mul_top (hm : m ≠ 0) : m * ⊤ = ⊤ := WithTop.mul_top hm
 @[simp] theorem top_mul (hm : m ≠ 0) : ⊤ * m = ⊤ := WithTop.top_mul hm
 
+theorem top_pow {n : ℕ} (n_pos : 0 < n) : (⊤ : ℕ∞) ^ n = ⊤ := WithTop.top_pow n_pos
+
 instance canLift : CanLift ℕ∞ ℕ (↑) (· ≠ ⊤) := WithTop.canLift
 #align enat.can_lift ENat.canLift