mathlib3

1c110ada - fix(tactic/linarith): elaborate and insert arguments before destructing hypotheses (#5501)

fix(tactic/linarith): elaborate and insert arguments before destructing hypotheses (#5501) closes #5480 Arguments to `linarith` can depend on hypotheses (e.g. conjunctions) that get destructed during preprocessing, after which the arguments will no longer elaborate or typecheck. This just moves the elaboration earlier and adds these arguments as hypotheses themselves. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>