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

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.

• I’m not exact sure how ring works, but you are using here that the rationals are a field, not just a ring. Also assuming somehow ring can handle division, it is also a few steps of reasoning that x isn’t 0. Commented Aug 2 at 10:28

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.

• This is the correct answer for working in Mathlib, but for this book it has its own list of tactics and I don’t think field_simp is among them. Commented Aug 6 at 21:51
• Thanks for the link towards the paper! Commented Aug 7 at 10:29

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).

• Thanks for the hint. Commented Aug 7 at 10:29