why I cannot apply `ring` to `y = x * y / x`

Question

I'm teaching myself about Lean4 using The Mechanics of Proof. I'm trying to solve one of the problems in the book 2.1.9 exercise 3

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
  have h3 : x*y > 0 := by addarith[h]
  cancel x at h3
  calc
    y = x * y / x := by ring
    _ = 1 / x := by rw[h]
    _ ≤ 1 / 1 := by rel[h2]
    _ = 1 := by numbers

There is error on y = x * y / x when applying ring tactic. I think it should work but I don't understand why I cannot apply ring here. Thank you for the help!

P.S. I think I should use h3 somewhere where I prove $y > 0$ but I didn't use it anywhere. Maybe that indicates I'm totally wrong on my proof.

Answer 1

The ring tactic expects both sides to be expressions in a ring, so it cannot handle y/x.

I'm not a lean user but the tactic you want is probably field_simp, though you may also have to show that x is nonzero.

See also Proving Equalities in a Commutative Ring Done Right in Coq for more general details on how the ring tactic works.

Answer 2

Since ring can’t handle most uses of division, you need something different. If this was real world Lean, there are other tactics that could work here. (See other answer.)

But luckily for you, this problem can be solved without division. There is a simple calculation using only multiplication (and cancel to get that y > 0 according to the hint in the book).