How to rewrite the List which I am indexing with pattern matching

Question

I'm working in Lean 4 and I'm trying to understand how to pattern match in tactics mode where one side of the goal state is. Below p is a prime number. Full code available at the bottom if you would like a minimal working example.

(Finset.sort (fun x x_1 => x ≤ x_1)
      (Finset.map { toFun := fun x => p ^ x, inj' := (_ : Function.Injective fun x => p ^ x) }
        (Finset.range (k + 1))))[i]

What I would like it to transform to is

(List.map { toFun := fun x => p ^ x, inj' := (_ : Function.Injective fun x => p ^ x)} 
    (Finset.sort (fun x x_1 => x ≤ x_1)
        (Finset.range (k + 1))))[i]

To achieve this, I have proved a theorem of the type (proof not shown)

theorem sort_monotone_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] 
 (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] 
  (s : β → β → Prop) [DecidableRel s] [IsTrans β s] [IsAntisymm β s] [IsTotal β s] 
    (f : α ↪ β) (preserve_lt : {x : α} → {y : α} → (h : r x y) → (s (f x) (f y))) 
    (fst : Finset α): Finset.sort s (Finset.map f fst) = List.map f (Finset.sort r fst) := by sorry

which when I feed in the proof of the fact that p^n is increasing, namely

theorem pow_p_increasing (p : ℕ) (h1 : Nat.Prime p): {x y: ℕ} → x ≤ y → ((⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) x) ≤ ((⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) y) := by sorry

can yield a proof of the following type

theorem sort_divisor_thm (p k : ℕ) (h1 : Nat.Prime p) : 
  Finset.sort (. ≤ .) (Finset.map (pow_p p h1) (Finset.range (k + 1))) =
  List.map (⇑(pow_p p h1)) (Finset.sort (. ≤ .) (Finset.range (k + 1))) := 
    sort_monotone_map (. ≤ .) (. ≤ .) (⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) (pow_p_increasing p h1) (Finset.range (k + 1))

But I am unable to use it to 'rw' the goal state. For more details, see the full code below

import Mathlib

def sorted_divisors (n : ℕ) : List ℕ := Finset.sort (. ≤ .) (Nat.divisors n) 

def pow_p (p : ℕ) (h1 : Nat.Prime p): ℕ ↪ ℕ := ⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩

theorem pow_p_increasing (p : ℕ) (h1 : Nat.Prime p): {x y: ℕ} → x ≤ y → ((⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) x) ≤ ((⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) y) := by sorry

theorem sort_monotone_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] 
 (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] 
  (s : β → β → Prop) [DecidableRel s] [IsTrans β s] [IsAntisymm β s] [IsTotal β s] 
    (f : α ↪ β) (preserve_lt : {x : α} → {y : α} → (h : r x y) → (s (f x) (f y))) 
    (fst : Finset α): Finset.sort s (Finset.map f fst) = List.map f (Finset.sort r fst) := by sorry

theorem sort_divisor_thm (p k : ℕ) (h1 : Nat.Prime p) : 
  Finset.sort (. ≤ .) (Finset.map (pow_p p h1) (Finset.range (k + 1))) =
  List.map (⇑(pow_p p h1)) (Finset.sort (. ≤ .) (Finset.range (k + 1))) := 
    sort_monotone_map (. ≤ .) (. ≤ .) (⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) (pow_p_increasing p h1) (Finset.range (k + 1))

theorem desired_goal (p k : ℕ) (h1 : Nat.Prime p) (i : Fin (sorted_divisors (p^k)).length): 
  (sorted_divisors (p^k))[i] = p^(i.val) := by 
  have h := Nat.divisors_prime_pow h1 k
  unfold sorted_divisors
  simp_rw [h]
  --unable to proceed here
  sorry

Any help is appreciated. I understand that I can prove my final goal in other ways. I would like to do it using this method of simplifying Finset.sort Finset.map. Thank you.