no goals
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hr : r ≠ 0
h : LiouvilleWith p (x * ↑r)
⊢ LiouvilleWith p x
simpa only [mul_assoc, ← Rat.cast_mul, mul_inv_cancel hr, Rat.cast_one, mul_one] using
  h.mul_rat (inv_ne_zero hr)