Converse to `Multiset.toFinset_card_of_nodup`?

Stream: Is there code for X?

[Jz Pan]

I think we only have this in mathlib:

theorem Multiset.toFinset_card_of_nodup {α : Type*} [DecidableEq α] {m : Multiset α} (h : Multiset.Nodup m) :
    Finset.card (Multiset.toFinset m) = ↑Multiset.card m

But in fact its converse is also true.

[Jz Pan]

theorem Multiset.toFinset_card_eq_card_iff_nodup {α : Type*} [DecidableEq α] {m : Multiset α} :
    m.toFinset.card = card m ↔ m.Nodup := ⟨by
  intro h
  rw [← dedup_eq_self]
  by_contra h1
  have : m.toFinset.card < card m := card_lt_of_lt (Ne.lt_of_le h1 (dedup_le m))
  linarith only [h, this],
  toFinset_card_of_nodup⟩

[Junyan Xu]

(deleted)

[Junyan Xu]

@loogle Finset.card, Multiset.Nodup

[loogle]

:search: Finset.card_mk, Multiset.toFinset_card_of_nodup

[Yaël Dillies]

In fact you should first prove card m.dedup = card m ↔ m.Nodup.

[Eric Wieser]

@loogle Multiset.card, Multiset.dedup

[Eric Wieser]

@loogle Multiset.card, Multiset.dedup

[loogle]

:search: Multiset.card_toFinset

[Ruben Van de Velde]

open Multiset in
example (α : Type*) [DecidableEq α] (m : Multiset α) : card m.dedup = card m ↔ m.Nodup :=
  .trans ⟨fun h => eq_of_le_of_card_le (dedup_le m) h.ge, congr_arg _⟩ dedup_eq_self

[Jz Pan]

Ruben Van de Velde said:

open Multiset in
example (α : Type*) [DecidableEq α] (m : Multiset α) : card m.dedup = card m ↔ m.Nodup :=
  .trans ⟨fun h => eq_of_le_of_card_le (dedup_le m) h.ge, congr_arg _⟩ dedup_eq_self

Cool! This is much shorter than my proof. Should this be added in mathlib?

[Ruben Van de Velde]

What do you think, @Yaël Dillies ? :)

[Jz Pan]

I opened the PR #8515. Comments are welcomed.