# Zulip Chat Archive

## Stream: new members

### Topic: Linarith weirdness

#### Peter Nelson (Aug 16 2020 at 04:52):

I'm trying to do problem 79 from the tutorials, and I have the following.

```
lemma bdd_below_segment {f : ℝ → ℝ} {a b : ℝ} (hf : ∀ x ∈ Icc a b, continuous_at_pt f x) :
∃ m, ∀ x ∈ Icc a b, m ≤ f x :=
begin
have negfcont : ∀ x ∈ Icc a b, continuous_at_pt (λ x, -f(x)) x,
{ intros x xicc,
apply continuous_opposite,
exact hf x xicc, },
have negfub := bdd_above_segment negfcont,
cases negfub with m hm,
use -m,
intros x xicc,
specialize hm x xicc,
linarith,
end
```

Before the last `linarith`

line, my last hypothesis is `hm: -f x ≤ m`

my goal is `-m ≤ f x`

. However, linarith can't finish this. My solution seems isomorphic to the one in the solutions file.

I'm sure I'm missing something simple, but I'm stumped. Can anyone help me with this?

#### Kyle Miller (Aug 16 2020 at 04:58):

I'll check, but in the meantime, try uncommenting `set_option pp.beta true`

at the top. You should then see that hypothesis or goal is not what you think it is. Use `dsimp only`

or `dsimp only at hm`

to beta reduce the lambda expression.

#### Alex J. Best (Aug 16 2020 at 04:59):

`library_search`

will find the lemma that does this in this case.

#### Alex J. Best (Aug 16 2020 at 05:00):

I'm not sure why linarith doesn't but by setting `set_option trace.linarith true`

we can see that it makes it to `[f x - -m < 0, -f x - m ≤ 0]`

#### Kyle Miller (Aug 16 2020 at 05:00):

Ok, I just checked. The hypothesis is actually

```
hm : (λ (x : ℝ), -f x) x ≤ m,
```

The issue is that `linarith`

does not try to beta reduce terms when it figures out all the variables and coefficients.

#### Kyle Miller (Aug 16 2020 at 05:02):

I remember it being especially frustrating running into this exact issue in this exact exercise when I was first learning Lean. (I've been meaning to submit a PR to remove the `set_option pp.beta true`

from the tutorial, but I haven't gotten around to it.)

#### Kyle Miller (Aug 16 2020 at 05:04):

Another thing you can do instead of `dsimp only at hm`

is

```
change -f x ≤ m at hm,
```

which tells Lean to try to unify `hm`

with the given expression, replacing `hm`

with the given expression. You can put `_`

holes in a `change`

tactic, too.

Last updated: Dec 20 2023 at 11:08 UTC