Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelL_mul_neg (Lean4Axiomatic/Rational/Sign.lean)

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
⊢ sgn r ≃ -1 → sgn (r * p - r * q) ≃ sgn (q - p)
Tactic:
intro (_ : sgn r ≃ -1)
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ -1
⊢ sgn (r * p - r * q) ≃ sgn (q - p)

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ -1
⊢ sgn (r * p - r * q) ≃ sgn (q - p)
Tactic:
calc
  _ ≃ sgn (r * p - r * q) := Rel.refl
  _ ≃ sgn (r * (p - q))   := sgn_subst (eqv_symm mul_distribL_sub)
  _ ≃ sgn r * sgn (p - q) := sgn_compat_mul
  _ ≃ -1 * sgn (p - q)    := AA.substL ‹sgn r ≃ -1›
  _ ≃ -sgn (p - q)        := Integer.mul_neg_one
  _ ≃ sgn (-(p - q))      := Rel.symm sgn_compat_neg
  _ ≃ sgn (q - p)         := sgn_subst neg_sub
State after:
no goals