mathlib3

2e72f352 - refactor(data/opposite): Remove the `op_induction` tactic (#9660)

refactor(data/opposite): Remove the `op_induction` tactic (#9660) The `induction` tactic is already powerful enough for this; we don't have `order_dual_induction` or `nat_induction` as tactics. The bulk of this change is replacing `op_induction x` with `induction x using opposite.rec`. This leaves behind the non-interactive `op_induction'` which is still needed as a `tidy` hook. This also renames the def `opposite.op_induction` to `opposite.rec` to match `order_dual.rec` etc.