chore(NumberTheory/Divisors): golf (#8698)

- use `∃ j ≤ k, _` instead of `∃ j (_ : j ≤ k)` in `Nat.mem_divisors_prime_pow`;
- golf `Nat.divisors_prime_pow`.

Mathlib/NumberTheory/Divisors.lean

@@ -318,9 +318,8 @@ theorem perfect_iff_sum_divisors_eq_two_mul (h : 0 < n) :
 #align nat.perfect_iff_sum_divisors_eq_two_mul Nat.perfect_iff_sum_divisors_eq_two_mul
 
 theorem mem_divisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} :
-    x ∈ divisors (p ^ k) ↔ ∃ (j : ℕ) (_ : j ≤ k), x = p ^ j := by
+    x ∈ divisors (p ^ k) ↔ ∃ j ≤ k, x = p ^ j := by
   rw [mem_divisors, Nat.dvd_prime_pow pp, and_iff_left (ne_of_gt (pow_pos pp.pos k))]
-  simp
 #align nat.mem_divisors_prime_pow Nat.mem_divisors_prime_pow
 
 theorem Prime.divisors {p : ℕ} (pp : p.Prime) : divisors p = {1, p} := by
@@ -333,18 +332,11 @@ theorem Prime.properDivisors {p : ℕ} (pp : p.Prime) : properDivisors p = {1} :
     pp.divisors, pair_comm, erase_insert fun con => pp.ne_one (mem_singleton.1 con)]
 #align nat.prime.proper_divisors Nat.Prime.properDivisors
 
--- Porting note: Specified pow to Nat.pow
 theorem divisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) :
-    divisors (p ^ k) = (Finset.range (k + 1)).map ⟨Nat.pow p, pow_right_injective pp.two_le⟩ := by
+    divisors (p ^ k) = (Finset.range (k + 1)).map ⟨(p ^ ·), pow_right_injective pp.two_le⟩ := by
   ext a
-  simp only [mem_divisors, mem_map, mem_range, lt_succ_iff, Function.Embedding.coeFn_mk, Nat.pow_eq,
-    mem_divisors_prime_pow pp k]
-  have := mem_divisors_prime_pow pp k (x := a)
-  rw [mem_divisors] at this
-  rw [this]
-  refine ⟨?_, ?_⟩
-  · intro h; rcases h with ⟨x, hx, hap⟩; use x; tauto
-  · tauto
+  rw [mem_divisors_prime_pow pp]
+  simp [Nat.lt_succ, eq_comm]
 #align nat.divisors_prime_pow Nat.divisors_prime_pow
 
 theorem divisors_injective : Function.Injective divisors :=