[Merged by Bors] - feat(data/finset/basic): A finset has card two iff it's {x, y} for some x ≠ y

[YaelDillies]

and the similar result for card three. Dumb but surprisingly annoying!

---

[tb65536]

Here are the list and multiset analogs. Maybe they can be used to simplify the proof?

namespace list

lemma length_eq_two {l : list α} : l.length = 2 ↔ ∃ a b, l = [a, b] :=
⟨match l with [a, b], _ := ⟨a, b, rfl⟩ end, λ ⟨a, b, e⟩, e.symm ▸ rfl⟩

lemma length_eq_three {l : list α} : l.length = 3 ↔ ∃ a b c, l = [a, b, c] :=
⟨match l with [a, b, c], _ := ⟨a, b, c, rfl⟩ end, λ ⟨a, b, c, e⟩, e.symm ▸ rfl⟩

end list

namespace multiset

lemma card_eq_two {s : multiset α} : s.card = 2 ↔ ∃ x y, s = {x, y} :=
⟨quot.induction_on s (λ l h, (list.length_eq_two.mp h).imp
  (λ a, Exists.imp (λ b, congr_arg coe))), λ ⟨a, b, e⟩, e.symm ▸ rfl⟩

lemma card_eq_three {s : multiset α} : s.card = 3 ↔ ∃ x y z, s = {x, y, z} :=
⟨quot.induction_on s (λ l h, (list.length_eq_three.mp h).imp
  (λ a, Exists.imp (λ b, Exists.imp (λ c, congr_arg coe)))), λ ⟨a, b, c, e⟩, e.symm ▸ rfl⟩

end multiset

[jcommelin]

@YaelDillies Could you please include those variants 🆙
Whether it allows you to golf, I don't know.

[YaelDillies]

I tried golfing from the multiset version but extracting x ≠ y from {x, y}.nodup is just as hard as what the current proof does.

[ocfnash]

Thanks

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests