Division in calc

Stream: new members

[u7122029]

Hi, Lean noob here. Sorry if the question is dumb. (Oops! I just realised this should be in the #maths stream. Sorry about this too.)
Basically I'm trying to show the following example from chapter 1 of the mechanics of proof book

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=
  calc
    y = -(2*x - y*x) / x + 2 := sorry -- x
    _ = - 0 / x + 2 := by rw [h2]
    _ = 2 := by ring

It seems I can't use ring at the line marked with an x since division is not an axiom of the rings. I tried looking for a field tactic but I couldn't find one. I also tried finding a group tactic which I did find, but that didn't work. Could I please have some help with this step?

Thanks in advance!

[Ruben Van de Velde]

You may be looking for field_simp, but you'll need to convince it that x ≠ 0

[Patrick Massot]

You are trying to do way too much at the same time on the first line.

[Kevin Buzzard]

For what it's worth:

import Mathlib.Tactic

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 := by
  nlinarith

[Kevin Buzzard]

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 := by
  polyrith

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 := by
  linear_combination (-(1 / 2 * y) + 1) * h1 + -1 * h2 / 2

[Heather Macbeth]

Shhh Kevin, this problem is meant to be done with just rw and ring :)