Easiest way to prove rational number num and den equality

Stream: general

[Teddy Baker]

I had a lot of trouble proving

import Mathlib.Data.Real.Basic

lemma q_num_den (r : ℚ) (hr : r = (448 : ℝ)/(81 : ℝ)) : r.num = 448 ∧ r.den = 81 := by sorry

I ended up having to cast 448 and 81 to \Q, then use Rat.num_div_eq_of_coprime and Rat.num_den_eq_of_coprime, which involved further cassting 448 and 81 to Int's and then proving that the NatAbs of those ints was coprime, etc. It involved quite a lot of manual casting for what is clearly a rather simple problem. I'm wondering if there is an easier way.

[Kyle Miller]

I'm not happy with it, but here's what I came up with:

lemma q_num_den (r : ℚ) (hr : r = (448 : ℝ)/(81 : ℝ)) : r.num = 448 ∧ r.den = 81 := by
  have : r = (448 : ℚ) / (81 : ℚ) := by
    rw [← Rat.cast_inj (α := ℝ), hr]
    norm_num
  rw [this]
  -- ⊢ (448 / 81).num = 448 ∧ (448 / 81).den = 81
  -- norm_num seems like it should work here
  -- but we can abuse definitional equality:
  constructor <;> rfl

[Teddy Baker]

Better than mine!