Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_mul_pos (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 (p * r - q * r) ≃ sgn (p - q)
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 (p * r - q * r) ≃ sgn (p - q)

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 (p * r - q * r) ≃ sgn (p - q)
Tactic:
calc
  _ ≃ sgn (p * r - q * r) := Rel.refl
  _ ≃ sgn (r * p - q * r) := sgn_subst (sub_substL mul_comm)
  _ ≃ sgn (r * p - r * q) := sgn_subst (sub_substR mul_comm)
  _ ≃ sgn (p - q)         := sgn_sub_cancelL_mul_pos ‹sgn r ≃ 1›
State after:
no goals