rw [Int.smul_one_eq_coe, Rat.coe_int_den, one_div, mul_inv_rev, ← mul_assoc,
  mul_inv_cancel ((@Nat.cast_ne_zero ℚ _ _ _).mpr hn.ne'), one_mul, ← Int.cast_two,
  Rat.inv_coe_int_den]
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ (x • 1).den ≠ (↑n * (1 / (2 * ↑n))).den
case refine'_2
n : ℕ
hn : 0 < n
x : ℤ
⊢ 1 ≠ if 2 = 0 then 1 else Int.natAbs 2