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

#mwe

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