calc
  _ = (p * q)^a                 := rfl
  _ ≃ (p * q)^((n:ℤ)-m)         := pow_substR a_eqv
  _ ≃ (p * q)^n / (p * q)^m     := pow_diff
  _ ≃ (p^n * q^n) / (p * q)^m   := div_substL Natural.pow_distribR_mul
  _ ≃ (p^n * q^n) / (p^m * q^m) := div_substR Natural.pow_distribR_mul
  _ ≃ (p^n / p^m) * (q^n / q^m) := eqv_symm div_mul_swap
  _ ≃ p^((n:ℤ)-m) * (q^n / q^m) := mul_substL (eqv_symm pow_diff)
  _ ≃ p^((n:ℤ)-m) * q^((n:ℤ)-m) := mul_substR (eqv_symm pow_diff)
  _ ≃ p^a * q^((n:ℤ)-m)         := mul_substL (pow_substR (Rel.symm a_eqv))
  _ ≃ p^a * q^a                 := mul_substR (pow_substR (Rel.symm a_eqv))
ℕ ℤ : 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 q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
a : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
⊢ (p * q) ^ a ≃ p ^ a * q ^ a
no goals