Multiset.powerset lemmas

Stream: mathlib4

[Alessandra Simmons]

I formalized a few small lemmas relating to Multiset.powerset (mainly Monotonicity and Injectivity, but also a few small utility lemmas), and I think they would probably be useful results to someone else, but I've never contributed to Mathlib before.

Could I get a second opinion on if these are good candidates for inclusion in Mathlib, and if any of them should be cut?

[Ruben Van de Velde]

Seems mostly sensible; some suggestions below:

import Mathlib

-- Not about Multisets
def ne_cards_ne {α : Type} {m n : Multiset α} : m.card ≠ n.card → m ≠ n :=
  ne_of_apply_ne _

-- Not about Multisets
def ne_one_not_empty {α : Type} {m n : Multiset α} : m ≠ n → m ≠ 0 ∨ n ≠ 0 :=
  fun a => Ne.ne_or_ne 0 a

def self_ne_cons {α : Type} {m : Multiset α} {a : α} : m ≠ a ::ₘ m := by
  induction m using Multiset.induction
  case empty =>
    exact Multiset.zero_ne_cons
  case cons head tail ih =>
    rw [@Multiset.cons_swap, ne_eq, Multiset.cons_inj_right]
    exact Ne.intro ih

def ne_exists_nonmember {α : Type} {m n : Multiset α} [DecidableEq α] : m ≠ n → ∃ a, m.count a ≠ n.count a := by
  contrapose!
  exact Multiset.ext.mpr

-- Should be called something like powerset_eq_singleton_empty_iff in this direction
def empty_iff_powerset_empty {α : Type} {m : Multiset α} : m.powerset = {0} ↔ m = 0 where
  mpr := by
    rintro rfl
    exact Multiset.powerset_zero
  mp powerset := by
    simpa using congr(Multiset.card $powerset)

-- zero_mem_powerset
def empty_in_powerset {α : Type} {m : Multiset α} : 0 ∈ m.powerset :=
  Multiset.mem_powerset.mpr m.zero_le

-- self_mem_powerset
def self_in_powerset {α : Type} {m : Multiset α} : m ∈ m.powerset :=
  Multiset.mem_powerset.mpr le_rfl

def List.Subperm.append {l₁ l₂ r₁ r₂ : List α}
    (hl : l₁.Subperm l₂) (hr : r₁.Subperm r₂) :
    (l₁ ++ r₁).Subperm (l₂ ++ r₂) := by
  obtain ⟨l, hl_perm, hl_sub⟩ := hl
  obtain ⟨r, hr_perm, hr_sub⟩ := hr
  exact ⟨l ++ r, hl_perm.append hr_perm, hl_sub.append hr_sub⟩

def List.Subperm.map {l₁ l₂ : List α} (f : α → β)
    (h : l₁.Subperm l₂) :
    (l₁.map f).Subperm (l₂.map f) := by
  obtain ⟨l, hl_perm, hl_sub⟩ := h
  exact ⟨l.map f, hl_perm.map f, hl_sub.map f⟩

def List.Subperm.sublists'_subperm_sublists' {l₁ l₂ : List α}
    (sublist : l₁.Sublist l₂) :
    l₁.sublists'.Subperm l₂.sublists' := by
  induction sublist with
  | slnil => exact .refl _
  | cons a _ ih =>
    rw [List.sublists'_cons]
    exact ih.trans (List.sublist_append_left ..).subperm
  | cons₂ a _ ih =>
    rw [List.sublists'_cons, List.sublists'_cons]
    exact ih.append (ih.map _)

def le_powerset_iff_le {α : Type} {m n : Multiset α} : m.powerset ≤ n.powerset ↔ m ≤ n where
  mp powerset := Multiset.mem_powerset.mp <| Multiset.mem_of_le powerset self_in_powerset
  mpr le :=
    Multiset.leInductionOn le fun {l₁ l₂} hsub => by
      rw [Multiset.powerset_coe', Multiset.powerset_coe', Multiset.coe_le]
      exact (List.Subperm.sublists'_subperm_sublists' hsub).map Multiset.ofList

instance powerset_mono {α : Type} : Monotone (@Multiset.powerset α) := by
  unfold Monotone
  intro a₁ a₂ a
  exact le_powerset_iff_le.mpr a

-- Should be powerset_injective
instance powerset_inj {α : Type} : Function.Injective (@Multiset.powerset α) := by
  unfold Function.Injective
  intro a₁ a₂ a
  exact le_antisymm
    (le_powerset_iff_le.mp (le_of_eq a))
    (le_powerset_iff_le.mp (le_of_eq a.symm))

[Alessandra Simmons]

Hey, thanks for the suggestions! I thought that the naming changes made sense given the policy, that the Ne results being unrelated to Multisets made a lot of sense, and that a lot of your definitions seemed a lot simpler/more maintainable, so I opened a PR against Mathlib with those revisions (and a few other changes): https://github.com/leanprover-community/mathlib4/pull/35465

[Violeta Hernández]

You can also write #35465 to link to your PRs more easily