This PR fixes a bug in the pattern selection in the `grind`.
Int.tdiv
Int.tmod
Simp.Config.implicitDefEqProofs
Lean.loadPlugin