<->
grind
This PR adds support for case-splitting on `<->` (and `@Eq Prop`) in the `grind` tactic.
Int.tdiv
Int.tmod
Simp.Config.implicitDefEqProofs
Lean.loadPlugin