intro (_ : p₁ ≃ p₂)
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p₁ p₂ q : ℚ
⊢ p₁ ≃ p₂ → p₁ - q ≃ p₂ - q
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ p₁ - q ≃ p₂ - q