mathlib

bcbdebaa - chore(tactic/apply_fun): add doc string and remove duplication (#2485)

chore(tactic/apply_fun): add doc string and remove duplication (#2485) I was just adding a docstring to `tactic.apply_fun`, and then saw some duplication and removed it. An example of a use of #2484. <br> <br> <br> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>