no goals
α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
rw [mul_invOf_eq_iff_eq_mul_right, ← Int.commute_cast, mul_assoc,
  ← mul_left_eq_iff_eq_invOf_mul, Int.commute_cast]