chore(data/multiset): move has_repr into its own file to remove data.string.basic import

[ChrisHughes24]

---

I did it like this instead of moving the deifnition of le to string.defs because the repr instance also depends on some properties of the ordering to prove it is well defined on multisets.

[jcommelin]

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

[bors]

✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ChrisHughes24]

I built this locally

bors r+

[bors]

👎 Rejected by label

[ChrisHughes24]

bors r+

[ChrisHughes24]

Maybe it's better to make these into meta instances

bors r-

[bors]

Canceled.

[eric-wieser]

I think a better approach would be to hide the meta behind a typeclass instance: something like:

import logic.embedding.basic
import data.prod.lex
import data.pi.lex
import logic.equiv.basic
import data.string.basic
import data.multiset.sort

/-- When printing collections of `α`, sort via a representation in `αo` -/
class has_repr_order_key (α : Type*) (αo : out_param Type*) [linear_order αo] :=
(to_key : α ↪ αo)

instance linear_order.to_has_repr_order_key {α} [linear_order α] : has_repr_order_key α α :=
⟨function.embedding.refl _⟩

instance prod.to_has_repr_order_key {α β αo βo}
  [linear_order αo] [linear_order βo] [has_repr_order_key α αo] [has_repr_order_key β βo] :
  has_repr_order_key (α × β) (αo ×ₗ βo) :=
⟨(has_repr_order_key.to_key.prod_map has_repr_order_key.to_key).trans to_lex.to_embedding⟩

-- TODO: `pi` order

instance (α αo : Type*) [linear_order αo] [has_repr_order_key α αo]:
  is_linear_order α ((≤) on has_repr_order_key.to_key) :=
@has_le.le.is_linear_order _ $
  linear_order.lift' (has_repr_order_key.to_key : α → αo) has_repr_order_key.to_key.injective

/-- fallback instance using string sorting -/
@[priority 100, instance]
meta instance has_repr.to_has_repr_order_key {α} [has_repr α] :
  has_repr_order_key α string :=
⟨⟨repr, sorry⟩⟩  -- We can cheat to make this not a sorry since this is meta, right?

#eval ({1, (1, 5), (5, 1), 11} : multiset (ℕ × ℕ)).sort ((≤) on has_repr_order_key.to_key)

[eric-wieser]

I've created #18166 to track my suggestion above, we can always revisit it in Mathlib4 after the port.

I assume this PR should be closed in light of your new PR, #18163?