intro (_ : a₁ ≃ a₂)
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Integer.Induction ℤ
ℚ : 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
p : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → p ^ a₁ ≃ p ^ a₂
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Integer.Induction ℤ
ℚ : 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
p : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ p ^ a₁ ≃ p ^ a₂