Commit 2022-10-20 09:55 98af8e3d

feat: port Data/Sigma/Basic (#479) My first attempt to port a file to mathlib4. Please review my code style carefully -- I'm still not 100% sure about the rules yet. Notes:

1. The file uses Function.surjective.forall once, and this declaration is in Mathlib.Logic.Function.Basic. Conversely, importing that file gives us everything we need. As a result the imports in this file look totally unrelated to the corresponding imports in the mathlib3 file.
2. The proof of mk.inj_iff in mathlib3 was by simp but this failed in mathlib4 so I knocked up a longer proof (lines 56-57). Should I worry about this? In Lean 3 simp? suggested simp only [implies_true_iff, and.congr_left_iff], which didn't work in Lean 3, and squeeze_simp suggested simp only which (to my mild surprise) does ;-)
3. I also edited the module docstring because I found the Lean 3 docstring claim that a dependent product was "like α × β" and then immediately "a generalization of α ⊕ β" confusing (these are not the same alpha and beta; the idea is that the first alpha is bool in the second example; hopefully my explanation is now better).