Theorem: Lean4Axiomatic.Rational.sgn_sub_cancelR_div_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 : ℚ
inst✝ : AP (sgn r ≃ 1)
⊢ sgn (p / r - q / r) ≃ sgn (p - q)
Tactic:
have : sgn (r⁻¹) ≃ 1 := Rel.trans sgn_recip ‹AP (sgn r ≃ 1)›.ev
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 : ℚ
inst✝ : AP (sgn r ≃ 1)
this : 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 : ℚ
inst✝ : AP (sgn r ≃ 1)
this : sgn (r⁻¹) ≃ 1
⊢ sgn (p / r - q / r) ≃ sgn (p - q)
Tactic:
calc
  _ ≃ sgn (p/r - q/r)         := Rel.refl
  _ ≃ sgn (p * r⁻¹ - q/r)     := sgn_subst (sub_substL div_mul_recip)
  _ ≃ sgn (p * r⁻¹ - q * r⁻¹) := sgn_subst (sub_substR div_mul_recip)
  _ ≃ sgn (p - q)             := sgn_sub_cancelR_mul_pos this
State after:
no goals