# Zulip Chat Archive

## Stream: new members

### Topic: Proving two inequalities in a single calc line

#### Gunnar Þór Magnússon (Jan 29 2021 at 19:56):

I'm working through the Lean tutorial and have one example down to a fairly standard triangle inequality calculation. I basically have this:

```
calc |u p - u q| = |u p - l - (u q - l)| : by ring
... ≤ |u p - l| + |u q - l| : by apply ad_hoc_lemma
... ≤ ε/2 + ε/2 : by exact hN p hp; exact hN q hq
... = ε : by linarith,
```

where `hN`

takes an integer `p`

, a proof `hp`

that it is greater than some fixed number, and outputs a proof that `|u p - l| <= \epsilon`

.

My problem is in the third line, which Lean doesn't like. I'd like to apply two inequalities at once, that `|u p - l| <= \epsilon`

and `|u q - l| <= \epsilon`

but can't figure out the syntax to do so. Any hints?

#### Mario Carneiro (Jan 29 2021 at 20:00):

#### Mario Carneiro (Jan 29 2021 at 20:01):

You shouldn't be using `exact`

twice; rather you should apply `add_le_add`

, which produces two subgoals, that are then closed by `exact`

#### Mario Carneiro (Jan 29 2021 at 20:02):

so that means something like `by apply add_le_add; [exact hN p hp, exact hN q hq]`

or more simply `add_le_add (hN p hp) (hN q hq)`

since this is basically just a term proof, you don't need `by`

anything

#### Gunnar Þór Magnússon (Jan 29 2021 at 20:06):

Sorry for not posting an mwe. Will do that next time.

But thanks for the hint. That did it. I'm still learning the ins and outs here.

#### Patrick Massot (Jan 29 2021 at 20:11):

You don't have to remember `add_le_add`

, you can use `linarith [hN p hp, hN q hq]`

,

Last updated: Dec 20 2023 at 11:08 UTC