calc
  _ = (p^a)^b                                       := rfl
  _ ≃ ((p^n)^k/(p^m)^k) / ((p^n)^j/(p^m)^j)         := pow_expand
  _ ≃ ((p^n)^k*(p^m)^j) / ((p^m)^k*(p^n)^j)         := div_div_div
  _ ≃ p^(n*k + m*j) / ((p^m)^k*(p^n)^j)             := div_substL pow_combine
  _ ≃ p^(n*k + m*j) / p^(m*k + n*j)                 := div_substR pow_combine
  _ ≃ p^(((n*k + m*j : ℕ):ℤ) - ((m*k + n*j : ℕ):ℤ)) := eqv_symm pow_diff
  _ ≃ p^(a * b)                                     := pow_substR pow_reduce
ℕ ℤ : 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)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
diff_expand : ∀ {w x y z : ℤ}, (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
pow_reduce : Coe.coe (n * k + m * j) - Coe.coe (m * k + n * j) ≃ a * b
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
no goals