equality of multisets

Stream: general

[Johan Commelin]

How is one supposed to prove

lemma test {σ : Type*} (s t : σ) : ([s, s, t] : multiset σ) = [t, s, s] := _

[Mario Carneiro]

by simp [insert_comm]?

[Mario Carneiro]

alternatively, apply quotient.sound and then use perm.swap and friends

[Johan Commelin]

Aha... ok.

[Johan Commelin]

I didn't know about insert_comm.

[Mario Carneiro]

I actually just guessed it existed

[Mario Carneiro]

thanks yesterday mario

[Kevin Buzzard]

When I look at files like multiset.lean I honestly think "golly, I'm glad I didn't take up Lean about 18 months earlier than I did"

[Kevin Buzzard]

Those files are so huge, and so complete, and because everything is a quotient the proofs are often extremely cryptic and would be very hard indeed for a beginner to generate.

[Kenny Lau]

maybe we should write a tactic that will sort the elements

[Mario Carneiro]

there is a function for that, multiset.sort

[Mario Carneiro]

as for sorting it syntactically, that's what simp does