have pow_expand : (p^a)^b ≃ ((p^n)^k/(p^m)^k) / ((p^n)^j/(p^m)^j) := calc
  _ = (p^a)^b                               := rfl
  _ ≃ (p^((n:ℤ)-m))^b                       := pow_substL (pow_substR a_eqv)
  _ ≃ (p^n/p^m)^b                           := pow_substL pow_diff
  _ ≃ (p^n/p^m)^((k:ℤ)-j)                   := pow_substR b_eqv
  _ ≃ (p^n/p^m)^k / (p^n/p^m)^j             := pow_diff
  _ ≃ ((p^n)^k/(p^m)^k) / (p^n/p^m)^j       := div_substL pow_distribR_div
  _ ≃ ((p^n)^k/(p^m)^k) / ((p^n)^j/(p^m)^j) := div_substR pow_distribR_div
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
⊢ (p ^ a) ^ b ≃ p ^ (a * b)