exact this
ℕ ℤ : 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
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝³ : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this✝² : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
this✝¹ : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
this✝ : p ^ n₁ / p ^ m₁ / (p ^ n₂ / p ^ m₂) ≃ 1
this : p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
no goals