# Zulip Chat Archive

## 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?

Thanks in advance!

#### 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