# Zulip Chat Archive

## Stream: new members

### Topic: Why is this simp lemma failing?

#### Marc Masdeu (Dec 15 2020 at 10:08):

Hi,

I don't understand why this fails:

```
@[simp] lemma mul_div_eq {a x : ℝ} (h : x ≠ 0) : a * x / x = a :=
begin
suffices : x / x = 1,
rw [mul_div_assoc, this, mul_one],
rw div_eq_one_iff_eq h,
end
example {a x : ℝ} (h : x ≠ 0) : a * x / x = a :=
begin
simp only [mul_div_eq], -- fails
end
```

When I look at the trace, I see that it can't prove that x is nonzero, which is in fact a hypothesis in the example.

More generally, I am surprised that it takes quite a bit of effort to prove the following multiplicative identity:

```
example (x : ℝ) (h : x ≠ 0): 1 / 12 * (x / 2)⁻¹ * x ^ 3 = 1 / 6 * x ^ 2 := sorry
```

Is there something that I am missing?

Thank you!

#### Kevin Buzzard (Dec 15 2020 at 10:09):

[grumble grumble not MWE grumble]

#### Anne Baanen (Dec 15 2020 at 10:09):

Presumably `simp only [mul_div_eq, h]`

will work?

#### Kevin Buzzard (Dec 15 2020 at 10:10):

It doesn't, but `simp only [mul_div_eq h]`

does.

#### Marc Masdeu (Dec 15 2020 at 10:14):

Kevin Buzzard said:

[grumble grumble not MWE grumble]

Yes, I should have sorry'ed the first lemma. But it was 3 lines...

#### Kevin Buzzard (Dec 15 2020 at 10:14):

no it's a missing import :-)

#### Kevin Buzzard (Dec 15 2020 at 10:15):

Sometimes you get people saying "this doesn't work" and then other people say "yes it does" and it's all because someone posted something without any imports and then other people use different imports and get different behaviour. That's why it's important.

#### Marc Masdeu (Dec 15 2020 at 10:16):

I should have known this by now...my apologies. I'll edit it to fix the example.

#### Kenny Lau (Dec 15 2020 at 10:16):

Kevin Buzzard said:

[grumble grumble not MWE grumble]

#### Kevin Buzzard (Dec 15 2020 at 10:17):

So for your example, this should be closed with `field_simp [h], ring`

and I'm surprised it isn't. `field_simp`

is the tactic you're missing, it should clear denominators. But for some reason it's not doing so.

#### Kevin Buzzard (Dec 15 2020 at 10:18):

```
example (x : ℝ) (h : x ≠ 0): 1 / 12 * (x / 2)⁻¹ * x ^ 3 = 1 / 6 * x ^ 2 :=
begin
have h12x : x * 12 ≠ 0 := mul_ne_zero h (by norm_num),
field_simp [h12x],
ring_exp,
end
```

#### Eric Wieser (Dec 15 2020 at 10:19):

Yeah, I was also surprised that I couldn't close this with `field_simp`

#### Kevin Buzzard (Dec 15 2020 at 10:19):

I thought that `field_simp`

knew that 12 wasn't 0 and the product of two nonzero things was nonzero, but apparently it doesn't in this case.

#### Marc Masdeu (Dec 15 2020 at 10:19):

OK, I thought that ring would suffice (I'm happy to add some things are nonzero in the hypotheses list).

#### Eric Wieser (Dec 15 2020 at 10:19):

Even this didn't work:

```
example (x : ℝ) (h : x ≠ 0): 1 / 12 * (x / 2)⁻¹ * x ^ 3 = 1 / 6 * x ^ 2 := by {
have : 12 ≠ 0 := by norm_num,
field_simp [h, this],
ring_exp,
}
```

#### Kevin Buzzard (Dec 15 2020 at 10:20):

That's probably the wrong 12

#### Marc Masdeu (Dec 15 2020 at 10:20):

About simp: is it possible to make it take the context hypotheses into account when you apply it?

#### Kevin Buzzard (Dec 15 2020 at 10:20):

`simp *`

#### Eric Wieser (Dec 15 2020 at 10:20):

Yep, with the right 12 that works:

```
example (x : ℝ) (h : x ≠ 0): 1 / 12 * (x / 2)⁻¹ * x ^ 3 = 1 / 6 * x ^ 2 := by {
have : (12 : ℝ) ≠ 0 := by norm_num,
field_simp [h, this],
ring_exp,
}
```

#### Kevin Buzzard (Dec 15 2020 at 10:21):

`ring`

doesn't know about division, and division is thorny because of division by zero. `field_simp`

is exactly the tactic which puts things over a common denominator and then clears denominators if it can find proofs that they're nonzero.

#### Eric Wieser (Dec 15 2020 at 10:21):

So I guess `field_simp`

doesn't try using `norm_num`

#### Kevin Buzzard (Dec 15 2020 at 10:21):

~~but it does because there's a 1/6 in there. I think the product is the issue.~~ [Eric seems to be right]

#### Marc Masdeu (Dec 15 2020 at 10:22):

Thanks! I'll clear my proofs a bit with this info... Glad to have learned field_simp (which should be called field, right?)

#### Kevin Buzzard (Dec 15 2020 at 10:22):

"The fact that a product is nonzero when all factors are, and that a power of a nonzero number is nonzero, are included in the simpset" (from the `field_simp`

docstring)

#### Kevin Buzzard (Dec 15 2020 at 10:22):

`field_simp`

doesn't attempt to close the goal like `ring`

does, it only attempts to simplify it by clearing denominators.

#### Eric Wieser (Dec 15 2020 at 10:23):

Kevin Buzzard said:

"The fact that a product is nonzero when all factors are, and that a power of a nonzero number is nonzero, are included in the simpset" (from the

`field_simp`

docstring)

I guess that description is missing "a nonzero number is nonzero"?

#### Kevin Buzzard (Dec 15 2020 at 10:25):

```
example {a x : ℝ} (h : x ≠ 0) : a * x / x = a :=
begin
simp *,
end
```

does work.

#### Kevin Buzzard (Dec 15 2020 at 10:26):

As does `simp [h]`

. So it's the `simp only`

which is blocking things. Aah -- `squeeze_simp`

reports that the issue is that the simplifier algorithm also uses `not_false_iff`

and `ne.def`

.

#### Marc Masdeu (Dec 15 2020 at 10:27):

I though that `simp *`

applied simp to the goal and to the hypotheses. But I see that it apply simp to the goal *using* the hypotheses, which is quite different. Thanks!

#### Marc Masdeu (Dec 15 2020 at 10:28):

(OK I see, otherwise it's `simp at h`

, my bad.

#### Kevin Buzzard (Dec 15 2020 at 10:28):

PS Marc -- Lean already has `mul_div_cancel`

marked as simp so

```
@[simp] lemma mul_div_eq {a x : ℝ} (h : x ≠ 0) : a * x / x = a :=
begin
simp [h],
end
```

works.

#### Kevin Buzzard (Dec 15 2020 at 10:33):

Eric you do seem to be right about the 12 though, which really confuses me because the 6 wasn't a problem on the RHS.

#### Kevin Buzzard (Dec 15 2020 at 10:37):

Oh I see my mistake -- the 6 doesn't get cancelled but `ring`

deals with it anyway somehow.

Last updated: May 11 2021 at 23:11 UTC