## Stream: new members

### Topic: Division in calc

#### u7122029 (Nov 12 2023 at 15:26):

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?

#### Ruben Van de Velde (Nov 12 2023 at 15:41):

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

#### Patrick Massot (Nov 12 2023 at 15:47):

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

#### Kevin Buzzard (Nov 12 2023 at 16:21):

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 (Nov 12 2023 at 16:22):

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 (Nov 12 2023 at 19:03):

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

Last updated: Dec 20 2023 at 11:08 UTC