List.Perm_diff_append_of_Subperm ??

Stream: Is there code for X?

[Malvin Gattinger]

Is there a lemma like this or an easy proof? I've been running in circles between multisets, list counts and (sub)permutations for a bit :thinking:

import Mathlib

theorem List.Perm_diff_append_of_Subperm {α} [DecidableEq α] {L M : List α} (h : M.Subperm L) :
    L.Perm (L.diff M ++ M) := by
  sorry

[Eric Wieser]

To me that looks like one that would be easiest in the multiset spelling

[Malvin Gattinger]

Yes, got it. Probably can be done shorter I guess.

import Mathlib

theorem Multiset_diff_append_of_le [DecidableEq α] {R Rcond Rnew : List α} :
    Multiset.ofList (R.diff Rcond ++ Rnew)
    = Multiset.ofList R - Multiset.ofList Rcond + Multiset.ofList Rnew := by
  rw [@Multiset.coe_sub]
  rw [Multiset.coe_add]

theorem List.Perm_diff_append_of_Subperm {α} [DecidableEq α] {L M : List α} (h : M.Subperm L) :
    L.Perm (L.diff M ++ M) := by
  rw [perm_iff_count]
  intro φ
  rw [← Multiset.coe_count, ← Multiset.coe_count]
  rw [@Multiset_diff_append_of_le α _ L M M]
  rw [tsub_add_cancel_of_le h]

[Eric Wieser]

tsub_add_cancel_of_le is the key step here, you can probably golf things around it