mathlib

2fb6022e - feat(mk_iff_of_inductive_prop): add, use, and document command (#2490)

feat(mk_iff_of_inductive_prop): add, use, and document command (#2490) This existed as an (undocumented) tactic that was being called with `run_cmd`. It deserves to be a documented user command. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>