get the denominator and numerator from a rational number

Stream: Is there code for X?

[Huajian Xin]

Is there any direct method to get the denominator and numerator from a rational number? For example, how to solve the tactic state

m: ℚ
h: m = 1 / 4
⊢ m.num = 1
```?

[Kevin Buzzard]

You don't get this completely for free because somewhere you'll need that 1/4 is in lowest terms. For example m is also 2/8 but the numerator isn't 2.

I would try subst h and then either rfl or norm_num or simp.

[Kalle Kytölä]

import Mathlib.Data.Rat.Basic

example (q : ℚ) (h : q = -773 / 28601) :
    q.den = 37 := by
  rw [h]
  rfl

[Huajian Xin]

Thanks! But it seems that the rat defined in Lean 3 mathlib forces the denominator and numerator should be coprime, and these tactic seems fail. :smiling_face_with_tear:

[Huajian Xin]

Kevin Buzzard said:

You don't get this completely for free because somewhere you'll need that 1/4 is in lowest terms. For example m is also 2/8 but the numerator isn't 2.

I would try subst h and then either rfl or norm_num or simp.

[Huajian Xin]

Kalle Kytölä said:

import Mathlib.Data.Rat.Basic

example (q : ℚ) (h : q = -773 / 28601) :
    q.den = 37 := by
  rw [h]
  rfl

Thanks! I apology for my unclear that I'm using Lean 3, and could you please provide a Lean 3 code? I seems that rfl in Lean 3 cannot fix this.

[Scott Morrison]

Is there something blocking you from upgrading to Lean 4? We're hoping everyone is able to switch soon! :-)