mathlib
35fbfe0a - fix(tactic/linarith): use refine instead of apply to avoid apply bug (#3199)

Commit

5 years ago

fix(tactic/linarith): use refine instead of apply to avoid apply bug (#3199) closes #3142 Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

Author

robertylewis

Parents