Commit 2023-02-01 05:31 f2c39613

feat: port Data.Finsupp.Basic (#1949) porting notes:

1. simps was not working in various places due to the noncomputable, so I had to manually add some lemmas it would have generated. See here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/finding.20.60simps.60.20lemmas
2. Lean 4 really had trouble inferring arguments to mapRange_comp for some reason as compared to Lean 3
3. In several places I had to manually supply decidability instances (from Classical). This should probably be investigated.
4. It looks like the Sigma.mk.inj auto-generated lemma was never created. Why?
5. In one place, ext didn't fire the same way in Lean 3 versus Lean 4; I just copied the output of ext? from Lean 3, but we should understand what went wrong.