# PR contents

This is the supremum of

- #8284
- #8056
- #8023
- #8332
- #8226 (already approved)
- #7834 (already approved)

along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it.

Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380.

I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime.

# Lean PRs involved in this bump

In particular this includes adjustments for the Lean PRs

* leanprover/lean4#2778 
* leanprover/lean4#2790
* leanprover/lean4#2783
* leanprover/lean4#2825
* leanprover/lean4#2722

## leanprover/lean4#2778

We can get rid of all the 
```
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
```
macros across Mathlib (and in any projects that want to write natural number powers of reals).

## leanprover/lean4#2722

Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. 

## leanprover/lean4#2783

This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes:
* switching to using explicit lemmas that have the intended level of application
* `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour
* Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`.

This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes!



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mauricio Collares <mauricio@collares.org>

# PR contents

This is the supremum of

- #8284
- #8056
- #8023
- #8332
- #8226 (already approved)
- #7834 (already approved)

along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it.

Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380.

I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime.

# Lean PRs involved in this bump

In particular this includes adjustments for the Lean PRs

* leanprover/lean4#2778 
* leanprover/lean4#2790
* leanprover/lean4#2783
* leanprover/lean4#2825
* leanprover/lean4#2722

## leanprover/lean4#2778

We can get rid of all the 
```
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
```
macros across Mathlib (and in any projects that want to write natural number powers of reals).

## leanprover/lean4#2722

Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. 

## leanprover/lean4#2783

This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes:
* switching to using explicit lemmas that have the intended level of application
* `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour
* Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`.

This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes!



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mauricio Collares <mauricio@collares.org>

These are split from #8226 (and subsequent changes in #8366), and arise from the fact the latest Lean is better at detecting these due to better abstraction.

I can't comment on whether any of these should be concerning, but putting them in a small commit makes it easier for someone to find and review them later.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

# PR contents

This is the supremum of

- #8284
- #8056
- #8023
- #8332
- #8226 (already approved)
- #7834 (already approved)

along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it.

Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380.

I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime.

# Lean PRs involved in this bump

In particular this includes adjustments for the Lean PRs

* leanprover/lean4#2778 
* leanprover/lean4#2790
* leanprover/lean4#2783
* leanprover/lean4#2825
* leanprover/lean4#2722

## leanprover/lean4#2778

We can get rid of all the 
```
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
```
macros across Mathlib (and in any projects that want to write natural number powers of reals).

## leanprover/lean4#2722

Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. 

## leanprover/lean4#2783

This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes:
* switching to using explicit lemmas that have the intended level of application
* `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour
* Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`.

This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes!



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mauricio Collares <mauricio@collares.org>

These are split from #8226 (and subsequent changes in #8366), and arise from the fact the latest Lean is better at detecting these due to better abstraction.

I can't comment on whether any of these should be concerning, but putting them in a small commit makes it easier for someone to find and review them later.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

This is the supremum of

- #8284
- #8056
- #8023
- #8332
- #8226 (already approved)
- #7834 (already approved)

along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it.

Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380.

I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime.

In particular this includes adjustments for the Lean PRs

* leanprover/lean4#2778
* leanprover/lean4#2790
* leanprover/lean4#2783
* leanprover/lean4#2825
* leanprover/lean4#2722

We can get rid of all the
```
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
```
macros across Mathlib (and in any projects that want to write natural number powers of reals).

Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`.

This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes:
* switching to using explicit lemmas that have the intended level of application
* `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour
* Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`.

This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes!

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mauricio Collares <mauricio@collares.org>

These are split from #8226 (and subsequent changes in #8366), and arise from the fact the latest Lean is better at detecting these due to better abstraction.

I can't comment on whether any of these should be concerning, but putting them in a small commit makes it easier for someone to find and review them later.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

# PR contents

This is the supremum of

- #8284
- #8056
- #8023
- #8332
- #8226 (already approved)
- #7834 (already approved)

along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it.

Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380.

I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime.

# Lean PRs involved in this bump

In particular this includes adjustments for the Lean PRs

* leanprover/lean4#2778 
* leanprover/lean4#2790
* leanprover/lean4#2783
* leanprover/lean4#2825
* leanprover/lean4#2722

## leanprover/lean4#2778

We can get rid of all the 
```
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
```
macros across Mathlib (and in any projects that want to write natural number powers of reals).

## leanprover/lean4#2722

Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. 

## leanprover/lean4#2783

This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes:
* switching to using explicit lemmas that have the intended level of application
* `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour
* Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`.

This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes!



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mauricio Collares <mauricio@collares.org>

`norm_num` now successfully reduces `Nat.digits` calls that have concrete arguments, so we can clean up some old workarounds.

This all works because Lean 4.6.0 introduced "simprocs", including the default-enabled `reduceLE`, `reduceMod`, `reduceDiv`, etc. which `norm_num` can invoke to discharge the side-goals required by applications of `digits_of_two_le_of_pos`.

Another crucial aspect is that `{ decide := false }` is the default for `simp` (and `norm_num`) after #8366.  Otherwise,
the `Acc`-based recursion in `digitsAux` would bog down kernel reduction.

`norm_num` now successfully reduces `Nat.digits` calls that have concrete arguments, so we can clean up some old workarounds.

This all works because Lean 4.6.0 introduced "simprocs", including the default-enabled `reduceLE`, `reduceMod`, `reduceDiv`, etc. which `norm_num` can invoke to discharge the side-goals required by applications of `digits_of_two_le_of_pos`.

Another crucial aspect is that `{ decide := false }` is the default for `simp` (and `norm_num`) after #8366.  Otherwise,
the `Acc`-based recursion in `digitsAux` would bog down kernel reduction.

`norm_num` now successfully reduces `Nat.digits` calls that have concrete arguments, so we can clean up some old workarounds.

This all works because Lean 4.6.0 introduced "simprocs", including the default-enabled `reduceLE`, `reduceMod`, `reduceDiv`, etc. which `norm_num` can invoke to discharge the side-goals required by applications of `digits_of_two_le_of_pos`.

Another crucial aspect is that `{ decide := false }` is the default for `simp` (and `norm_num`) after #8366.  Otherwise,
the `Acc`-based recursion in `digitsAux` would bog down kernel reduction.

`norm_num` now successfully reduces `Nat.digits` calls that have concrete arguments, so we can clean up some old workarounds.

This all works because Lean 4.6.0 introduced "simprocs", including the default-enabled `reduceLE`, `reduceMod`, `reduceDiv`, etc. which `norm_num` can invoke to discharge the side-goals required by applications of `digits_of_two_le_of_pos`.

Another crucial aspect is that `{ decide := false }` is the default for `simp` (and `norm_num`) after #8366.  Otherwise,
the `Acc`-based recursion in `digitsAux` would bog down kernel reduction.

`norm_num` now successfully reduces `Nat.digits` calls that have concrete arguments, so we can clean up some old workarounds.

This all works because Lean 4.6.0 introduced "simprocs", including the default-enabled `reduceLE`, `reduceMod`, `reduceDiv`, etc. which `norm_num` can invoke to discharge the side-goals required by applications of `digits_of_two_le_of_pos`.

Another crucial aspect is that `{ decide := false }` is the default for `simp` (and `norm_num`) after #8366.  Otherwise,
the `Acc`-based recursion in `digitsAux` would bog down kernel reduction.

`norm_num` now successfully reduces `Nat.digits` calls that have concrete arguments, so we can clean up some old workarounds.

This all works because Lean 4.6.0 introduced "simprocs", including the default-enabled `reduceLE`, `reduceMod`, `reduceDiv`, etc. which `norm_num` can invoke to discharge the side-goals required by applications of `digits_of_two_le_of_pos`.

Another crucial aspect is that `{ decide := false }` is the default for `simp` (and `norm_num`) after #8366.  Otherwise,
the `Acc`-based recursion in `digitsAux` would bog down kernel reduction.