Per the style guidelines, `λ` is disallowed in mathlib.
This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon.

Notes
- In lines I was modifying anyway, I also converted `=>` to `↦`.
- Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`.
- Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced.

<!-- The text above the `

- lambda by fun (and "=>" by "\mapsto", while I was it)
- remove commas after fields (there are seemingly allowed, but not necessary)
- indent code per the style guide

I did not consistently switch to `where` syntax; I was not sure if this has side effects (e.g. on performance). If desired, I can make that change also.

I did not test the code samples; they might be broken (but at least their syntax works).

Follow-up to #11301.

Includes some doc comments and real code: this is exhaustive, with two exceptions:
- some files are handled in #11409 instead
- I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std.

Follow-up to #11301, much shorter this time.

Fully update the module docstrings (in particular, the examples given therein) after #8386.

This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301.

Co-authored-by: @Vierkantor



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib.
This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon.

Notes
- In lines I was modifying anyway, I also converted `=>` to `↦`.
- Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`.
- Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced.

<!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions:
- some files are handled in #11409 instead
- I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std.

Follow-up to #11301, much shorter this time.

Fully update the module docstrings (in particular, the examples given therein) after #8386.

This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301.

Co-authored-by: @Vierkantor



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib.
This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon.

Notes
- In lines I was modifying anyway, I also converted `=>` to `↦`.
- Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`.
- Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced.

<!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions:
- some files are handled in #11409 instead
- I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std.

Follow-up to #11301, much shorter this time.

Fully update the module docstrings (in particular, the examples given therein) after #8386.

This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301.

Co-authored-by: @Vierkantor



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib.
This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon.

Notes
- In lines I was modifying anyway, I also converted `=>` to `↦`.
- Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`.
- Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced.

<!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions:
- some files are handled in #11409 instead
- I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std.

Follow-up to #11301, much shorter this time.

Fully update the module docstrings (in particular, the examples given therein) after #8386.

This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301.

Co-authored-by: @Vierkantor



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Includes some doc comments and real code: this is exhaustive, with two exceptions:
- some files are handled in #11409 instead
- I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std.

Follow-up to #11301, much shorter this time.

Fully update the module docstrings (in particular, the examples given therein) after #8386.

This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301.

Co-authored-by: @Vierkantor



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib.
This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon.

Notes
- In lines I was modifying anyway, I also converted `=>` to `↦`.
- Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`.
- Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced.

<!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions:
- some files are handled in #11409 instead
- I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std.

Follow-up to #11301, much shorter this time.

Fully update the module docstrings (in particular, the examples given therein) after #8386.

This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301.

Co-authored-by: @Vierkantor



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib.
This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon.

Notes
- In lines I was modifying anyway, I also converted `=>` to `↦`.
- Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`.
- Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced.

<!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions:
- some files are handled in #11409 instead
- I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std.

Follow-up to #11301, much shorter this time.

Fully update the module docstrings (in particular, the examples given therein) after #8386.

This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301.

Co-authored-by: @Vierkantor



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>