linarith and conjunctions

Stream: general

[Patrick Massot]

In my class I got tired of typing cases h with h1 h2, cases ..., cases ..., linarith all the time and ended up defining

meta def linarith' : tactic unit :=
do try auto.split_hyps,
       `[linarith]

@Rob Lewis Would you mind putting (a more flexible version of) this in mathlib?

[Rob Lewis]

https://github.com/leanprover-community/mathlib/pull/2320

[Patrick Massot]

Thanks!