@**Yaël Dillies**'s recent proof at #8164 uses `aesop` in a way that relies on `simp` using `decide := true` by default, which we have now disabled, and hence this breaks on `nightly-testing`.

I propose we add `@[aesop safe destruct]` to `Nat.not_prime_one` (and `Nat.not_prime_zero` while we're there).

Co-authored-by: Scott Morrison <scott.morrison@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>

# 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>

@**Yaël Dillies**'s recent proof at #8164 uses `aesop` in a way that relies on `simp` using `decide := true` by default, which we have now disabled, and hence this breaks on `nightly-testing`.

I propose we add `@[aesop safe destruct]` to `Nat.not_prime_one` (and `Nat.not_prime_zero` while we're there).

Co-authored-by: Scott Morrison <scott.morrison@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>

@**Yaël Dillies**'s recent proof at #8164 uses `aesop` in a way that relies on `simp` using `decide := true` by default, which we have now disabled, and hence this breaks on `nightly-testing`.

I propose we add `@[aesop safe destruct]` to `Nat.not_prime_one` (and `Nat.not_prime_zero` while we're there).

Co-authored-by: Scott Morrison <scott.morrison@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>

@**Yaël Dillies**'s recent proof at #8164 uses `aesop` in a way that relies on `simp` using `decide := true` by default, which we have now disabled, and hence this breaks on `nightly-testing`.

I propose we add `@[aesop safe destruct]` to `Nat.not_prime_one` (and `Nat.not_prime_zero` while we're there).

Co-authored-by: Scott Morrison <scott.morrison@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>