[Merged by Bors] - feat: Checking ae on a countable type

[YaelDillies]

and other simple measure lemmas

From PFR and LeanCamCombi

---

[urkud]

I have some minor edits I want to suggest but I need to grade an exam first. If I don't comment again in the next 14h, then ignore this comment.

[YaelDillies]

I'm not in a hurry! Will wait for your suggestions :)

[urkud]

Changes I pushed to this branch:

• Rename NullMeasurableSet.measure_compl to measure_compl₀ to match lemmas like map_apply₀, reorder, golf.
• Move measure_preimage_eq_zero_iff_of_countable right after tsum_measure_preimage_singleton, golf.
• Add measure_null_iff_singleton, generalize and golf ae_iff_of_countable, drop ae_of_countable.
• Move AEMeasurable.nullMeasurable close to your AEMeasurable.nullMeasurableSet. If you don't need your lemma very early, we can move both of them to where AEMeasurable.nullMeasurable was.
• Golf map_eq_zero_iff and mapₗ_eq_zero_iff using measure_univ_eq_zero.

[YaelDillies]

Happy with the changes!

I don't need AEMeasurable.nullMeasurableSet very early, but I was expecting it very early! This is one of the first lemmas my brain goes to when thinking about null-measurability, and I would have expected it be very basic.

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Canceled.

[YaelDillies]

Whoops, messed up mod_cast. Should be good now.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported