Basic ordering for rationals

Stream: mathlib4

[Scott N. Walck]

Hi folks,

I am trying to use Lean to prove that the rational number 2/5 is
less than or equal to the rational number 1/2. I am using
Mathlib rationals.

I was thinking to use Rat.le_def'. In that case, I should be
able to prove 2/5 is less than or equal to 1/2 if I can prove
that the integer 4 is less than or equal to the integer 5.

I can prove that 4 is less than or equal to 5 in some ways of
saying it, but not others. For example, here are two attempts at
a proof. The first one works but the second one doesn't.

(a) Is there a standard or easy way to prove 2/5 is less than or
equal to 1/2?

(b) Why does my first theorem succeed while my second theorem
fails?

Thanks!

import Mathlib

theorem le2512x : ((2 : ℤ) * (2 : ℤ)) ≤ ((1 : ℤ) * (5 : ℤ)) :=
  le_of_lt (Int.lt_succ_self 4)

-- fails
--theorem le2512y : Rat.num (2/5 : ℚ) * Rat.den (1/2 : ℚ) ≤ Rat.num (1/2 : ℚ) * Rat.den (2/5 : ℚ) :=
--  le_of_lt (Int.lt_succ_self 4)

[Yaël Dillies]

That's a subtle point. The issue is that the 2 / 5 notation for rationals unfolds to { num := 2 / Nat.gcd 2 5, den := 5 / Nat.gcd 2 5 , ... }, so to see that (2 / 5 : ℚ).num = 2 Lean needs to compute 2 / Nat.gcd 2 5, which it can't do since docs#Nat.gcd is defined by well-founded recursion.

[Yaël Dillies]

If you use 2 /. 5 instead of 2 / 5, it should Just Work :tm:

[Yaël Dillies]

No wait sorry you need to use { num := 2, den := 5, two more fields } instead of 2 / 5

[Eric Wieser]

The answer to your first question is "use the norm_num tactic"

[Daniel Weber]

I would have expected by decide to also work, since rationals are decidable, but while #eval (2/5 : ℚ) ≤ (1/2 : ℚ) does work theorem le2512y : (2/5 : ℚ) ≤ (1/2 : ℚ) := by decide fails :thinking:. native_decide works, but I see there are some warnings about it because it adds an axiom.