no goals
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b
rw [← mul_lt_mul_iff_left d, ← mul_lt_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
  inv_mul_cancel_right]