Proving two inequalities in a single calc line

Stream: new members

[Gunnar Þór Magnússon]

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]

#mwe

[Mario Carneiro]

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]

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]

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]

You don't have to remember add_le_add, you can use linarith [hN p hp, hN q hq],