mathlib3

b82ed0c5 - fix(tactic/apply_fun): beta reduction was too aggressive (#3214)

fix(tactic/apply_fun): beta reduction was too aggressive (#3214) The beta reduction performed by `apply_fun` was previously too aggressive -- in particular it was unfolding `A * B` to `A.mul B` when `A` and `B` are matrices. This fix avoids using `dsimp`, and instead calls `head_beta` separately on the left and right sides of the new hypothesis. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>