mathlib3
ea9f964b - fix(analysis/calculus/fderiv_symmetric): speed up tactic block from 3.6s to 180ms (#11426)

Commit
4 years ago
fix(analysis/calculus/fderiv_symmetric): speed up tactic block from 3.6s to 180ms (#11426) The timings are measured for the single small begin/end block. The proof as a whole is still around 7.6s, down from 11s. The fault here was likely the `convert`, which presumably spent a lot of time trying to unify typeclass arguments.
Author
Parents
Loading