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

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ -(p * q) ≃ -p * q
Tactic:
have : 0 ≃ -p + p := eqv_symm add_inverseL
State after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
this : 0 ≃ -p + p
⊢ -(p * q) ≃ -p * q

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
this : 0 ≃ -p + p
⊢ -(p * q) ≃ -p * q
Tactic:
calc
  -(p * q)                      ≃ _ := eqv_symm add_identL
  0 + -(p * q)                  ≃ _ := add_substL (eqv_symm mul_absorbL)
  0 * q + -(p * q)              ≃ _ := add_substL (mul_substL ‹0 ≃ -p + p›)
  (-p + p) * q + -(p * q)       ≃ _ := add_substL mul_distribR
  (-p * q + p * q) + -(p * q)   ≃ _ := add_assoc
  (-p) * q + (p * q + -(p * q)) ≃ _ := add_substR add_inverseR
  (-p) * q + 0                  ≃ _ := add_identR
  (-p) * q                      ≃ _ := eqv_refl
State after:
no goals