Multiset equality by simple tactic / way

Stream: general

[SnO2WMaN]

I'm currently formalizing a Multiset-based sequent caliculi, and I frequently using rewriting by equality as follows (actually elements are logical formulae but these are decidableEq so might be sufficient)

import Mathlib.Data.Multiset.Basic

example : ({0, 1, 2, 2, 3} : Multiset Nat) = ({3, 2, 2, 1, 0} : Multiset Nat) := by sorry

In case that the set is consists by two elements is easy. However, 3, 4, ..., elements cases might be proved by nth_rw, etc. but it becomes very tedious. Can we prove this more simpler method or tactic?

[Eric Wieser]

by decide should work

[SnO2WMaN]

(actually elements are logical formulae but these are decidableEq so might be sufficient)

Sorry this is not sufficient. In Nat case decide gonna be worked, but in my formulae case not worked.

[Mitchell Lee]

Are you trying to prove that two multiset literals, which have the same (syntactically equal) elements but in a different order, are equal? If so, I don't think there is any single existing tactic that can do it easily on its own. If you are willing to use classical logic, then you can do it using the following sequence of tactics:

import Mathlib.Data.Multiset.Basic

example (X : Type*) (a b c d : X) : ({a, b, c, c, d} : Multiset X) = ({c, a, c, d, b} : Multiset X) := by
  classical
  ext
  simp_rw [Multiset.insert_eq_cons, Multiset.count_cons, Multiset.count_singleton]
  omega

Otherwise, you could try to make your own tactic that normalizes multiset literals.

[Violeta Hernández]

import Mathlib.Data.Multiset.Basic
import Mathlib.Tactic.Abel

example (X : Type*) (a b c d : X) : ({a, b, c, c, d} : Multiset X) = ({c, a, c, d, b} : Multiset X) := by
  simp_rw [Multiset.insert_eq_cons, ← Multiset.singleton_add]
  abel