Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelL_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 (r * p - r * q) ≃ 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 (r * p - r * q) ≃ 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 (r * p - r * q) ≃ sgn (p - q)
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)         := AA.identL
State after:
no goals