Commit 2023-11-17 05:53 40b64f79

View on Github →

chore: bump to v4.3.0-rc2 (#8366)

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


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!

Estimated changes

modified theorem fish_pipe
modified theorem fish_pure
deleted def List.dropRight
deleted def List.dropRightWhile
deleted theorem List.dropRightWhile_nil
deleted theorem List.dropRight_nil
deleted theorem List.dropRight_zero
modified theorem List.dropWhile_eq_self_iff
added def List.rdrop
added def List.rdropWhile
added theorem List.rdropWhile_concat
added theorem List.rdropWhile_nil
added theorem List.rdropWhile_prefix
added theorem List.rdrop_concat_succ
added theorem List.rdrop_nil
added theorem List.rdrop_zero
added def List.rtake
added def List.rtakeWhile
added theorem List.rtakeWhile_concat
added theorem List.rtakeWhile_nil
added theorem List.rtakeWhile_suffix
added theorem List.rtake_concat_succ
added theorem List.rtake_nil
added theorem List.rtake_zero
deleted def List.takeRight
deleted def List.takeRightWhile
deleted theorem List.takeRightWhile_nil
deleted theorem List.takeRight_nil
deleted theorem List.takeRight_zero
modified theorem Function.graph_id
modified theorem Rel.inv_bot
modified theorem Rel.inv_top
modified theorem Cardinal.le_powerlt
modified theorem Cardinal.natCast_pow
modified theorem Cardinal.one_power
modified theorem Cardinal.power_def
modified theorem Cardinal.power_one
modified theorem Cardinal.power_zero
modified theorem Cardinal.zero_power
modified theorem Ordinal.log_nonempty
modified theorem Ordinal.nat_cast_opow
modified theorem Ordinal.one_opow
modified theorem Ordinal.opow_one
modified theorem Ordinal.opow_zero
modified theorem Ordinal.sup_opow_nat
modified theorem Ordinal.zero_opow