Theorem: Lean4Axiomatic.Rational.sub_substR (Lean4Axiomatic/Rational/Negation.lean)

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

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ q - p₁ ≃ q - p₂
Tactic:
calc
  q - p₁  ≃ _ := sub_add_neg
  q + -p₁ ≃ _ := add_substR (neg_subst ‹p₁ ≃ p₂›)
  q + -p₂ ≃ _ := eqv_symm sub_add_neg
  q - p₂  ≃ _ := eqv_refl
State after:
no goals