[Merged by Bors] - feat: port Data.Set.Basic

[semorrison]

1b36dabc50929b36caec16306358a5cc44ab441e

If more PRs arrive in mathlib that slice up Data.Set.Basic, that's okay, we'll just delete the relevant sections here.

TODO: finish linting

[Ruben-VandeVelde]

Lint failures:

./build/bin/runLinter
-- Found 2 errors in 15315 declarations (plus 44200 automatically generated ones) in mathlib with 13 linters

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.Data.Set.Basic
#check Set.sep_union.{u} /- Left-hand side simplifies from
  { x | x ∈ s ∪ t ∧ p x }
to
  { x | (x ∈ s ∨ x ∈ t) ∧ p x }
using
  simp only [Set.mem_union]
Try to change the left-hand side to the simplified term!
 -/
#check Set.sep_inter.{u} /- Left-hand side simplifies from
  { x | x ∈ s ∩ t ∧ p x }
to
  { x | (x ∈ s ∧ x ∈ t) ∧ p x }
using
  simp only [Set.mem_inter_iff]
Try to change the left-hand side to the simplified term!
 -/

[eric-wieser]

It looks like this is because set.sep is now unfolded syntactically like coe?

[winstonyin]

simp_rw [th] in mathlib3 can rewrite ∃ h : p, ..., where p can be proven using theorem th, into ∃ h : true, ..., but is unable to do so in mathlib4.

Tangentially, the pretty printer also doesn't properly render ∃ h : p, ... but instead as Exists fun h ↦ ..., so the type of h is somewhat obscured.

[kbuzzard]

People are aware about the prettyprinter issue with Exists, which was caused by the introduction of the ↦ notation; at the porting meeting the idea was discussed about reverting the ↦ notation change or doing it "properly" (which would involve changes in core Lean).

I've also seen other discussions about the simplifier behaving differently, including this issue; it is hopefully covered by leanprover/lean4#1937 .

[Ruben-VandeVelde]

I think this can probably land now

[semorrison]

bors merge

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style