Hopefully this one is not controversial. :-)

Co-authored-by: madvorak <dvorakmartinbridge@seznam.cz>

… sigma filter. (#10856)

add a general construction of a measurable space consisting of sets measurable with respect to some underlying sigma algebra modulo a given sigma filter. Refactor basic definitions and lemmas in `MeasureTheory/Measure/NullMeasurable.lean` to be an instance of this general construction.

The reason is that in the immediate future I would like to define Baire measurability in mathlib, and want to avoid repetition. 

*TODO*: Similarly generalize things about `AEMeasurable`, where appropriate. 



Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Golf and move `Prod.instNeBotNhdsWithinIio` etc.

…#11478)

I won't have a lot of time to work on this PR until April, so please feel free to take it over before then.

I initially wanted to use `synthInstance` rather than `findLocalDeclWithType?` but because `n` is not an outParam in `CharP R n`, the typeclass system won't work unless we know the value of `n` already.

Perhaps `findLocalDeclWithType?` is cheap enough to make this part of standard `reduce_mod_char` behaviour. I'd like to profile our usecases to find out if indeed this holds when expressions become much more complicated.

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/reduce_mod_char.20doesn't.20work




Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/missing.20doc.20of.20.60.23check_failure.60/near/434466058), the `#help` command is out of date with respect to the parsers that can be obscuring the search for the "first token", used to power the search-by-token-prefix form of the command `#help tactic "measur"`. The list below has been tested against everything in lean, and the only things that fail to find a first token now are those that actually don't have a token like the ident parser.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Without this change, the infoview gives
```
Error updating: Error fetching goals: Rpc error: InternalError: unknown free variable '_fvar.231'
```
when you hover over the variable name

Extend the style linter with two tiny features:
- lint on "isolated where": all occurrences were already fixed in #12991 and #13202.
- lint on "leading by": if one line starts with `by ` but the previous line ends with `:=`, according to the style guide the `by` should move to the previous line. For now, we only lint if the `by` fits on the previous line (fixed in #13618 and predecessors): there about other 28 cases in mathlib which don't have an obvious fix.

…use (#13784)

This is a few isolated lemmas split out of
#10853.

1. AnalyticAt.comp_of_eq
2. FormalMultilinearSeries.zero_radius
3. constFormalMultilinearSeries_zero

... as was discussed on zulip the other day; I cannot find the link quickly.
After this PR, a handful of uses remain which are harder to remove: [this branch](https://github.com/leanprover-community/mathlib4/compare/MR-mono-gcongr) comments them all

Inspired by #12661: let's start with some easy instances, so we can focus on the difficult ones.

In particular, this PR does not depend on any in-progress bugfixes, not tries to change a default value `by continuity` to `by fun_prop`.

I am not at all confident about the tagging of lemmas with fun_prop: I remember this being subtle, but can't find any documentation on this. @lecopivo Can you advise on these lemmas (or simply link to the right documentation if I just overlooked it)?

... and similar results for lipschitzness.

From LeanCamCombi

Unnecessary, and unhelpful.

…IsLocalization` (#13933)

If `x` is a point in the basic open set `D(f)` where `f` is a homogeneous element of positive
degree, then the homogeneously localized ring `A⁰ₓ` has the universal property of the localization
of `A⁰_f` at `φ(x)` where `φ : Proj|D(f) ⟶ Spec A⁰_f` is the morphism of locally ringed space
constructed as above.


Co-authored-by: Andrew Yang <the.erd.one@gmail.com>




Co-authored-by: zjj <j.jj@j.jj>

This is the first part of the refactor of `CompHaus` and friends (adding the new API which will eventually be used to redefine  the categories of compact Hausdorff spaces, see #12930)

…ile. (#13942)

…ive functors (#13948)

These are not actionable anymore (if they ever were).

Fixes #10756.

This is a proposal to rename what was in mathlib `Group` and in mathlib4 `GroupCat` to its literature name `Grp`. This has the advantage not to conflict with `group` that has been capitalised to `Group` and to be shorter.

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

… sets (#13638)

We add a lemma showing that if `P` is a downwards-closed predicate on sets, then `s` is maximal w.r.t. `P` 
iff `s` has property `P` but no proper insertion of `s` has property `P`. We also add the dual lemma for single removals and upwards-closed predicates.

Put materials about (Mv)Polynomial into Kaehler/Polynomial and the others into Kaehler/Basic