prove the value of numerator and denominator

Stream: general

[Huỳnh Trần Khanh]

I copied this message from an internal chatroom. I have the same question.

Has anyone solved the issue of "I've computed the fraction, now I need to verify numerator+denominator"?
Aka something like this
n : ℝ
j k : ℕ
hj : 0 < j
hk : 0 < k
hjk : j.Coprime k
h3 : n = ↑j / ↑k
hlogb_x : 625 / 256 = n
⊢ j + k = 881

[Chris Wong]

Does n need to be ℝ? If you use ℚ then you can talk about numerator and denominator directly.
I think you can apply docs#Rat.ext and then compare docs#Rat.num_div_eq_of_coprime and docs#Rat.den_div_eq_of_coprime.

[Huỳnh Trần Khanh]

Yeah n being ℝ is why the problem is so hard

[Daniel Weber]

Do you have a #mwe?

[Kyle Miller]

import Mathlib

example
    (n : ℝ)
    (j k : ℕ)
    (hj : 0 < j)
    (hk : 0 < k)
    (hjk : j.Coprime k)
    (h3 : n = ↑j / ↑k)
    (hlogb_x : 625 / 256 = n) :
    j + k = 881 := by
  have h1 : n = (j / k : ℚ) := by push_cast; exact h3
  have h2 : (625 / 256 : ℚ) = n := by push_cast; exact hlogb_x
  rw [h1] at h2
  norm_cast at h2
  have := @Rat.div_int_inj 625 256 j k
            (by simp) (by exact_mod_cast hk) (by norm_num) (by simpa)
            (by push_cast; exact h2)
  norm_cast at this
  obtain ⟨rfl, rfl⟩ := this
  rfl