# Commit 2020-05-03 08:34 a223bbb6

View on Github →chore(*): switch to lean 3.10.0 (#2587) There have been two changes in Lean 3.10 that have a significant effect on mathlib:

`rename'`

has been moved to core. Therefore`rename'`

has been removed.- Given a term
`⇑f x`

, the simplifier can now rewrite in both`f`

and`x`

. In many cases we had both`⇑f = ⇑f'`

and`⇑f x = ⇑f' x`

as simp lemmas; the latter is redundant now and has been removed (or just not marked simp anymore). The new and improved congruence lemmas are also used by`convert`

and`congr`

, these tactics have become more powerful as well. I've also sneaked in two related changes that I noticed while fixing the proofs affected by the changes above: `@[to_additive, simp]`

has been replaced by`@[simp, to_additive]`

in the monoid localization file. The difference is that`@[to_additive, simp]`

only marks the multiplicative lemma as simp.`def prod_comm : α × β ≃ β × α`

(etc.) is no longer marked`@[simp]`

. Marking this kind of lemmas as simp causes the simplifier to unfold the definition of`prod_comm`

(instead of just rewriting`α × β`

to`β × α`

in the`≃`

simp relation). This has become a bigger issue now since the simplifier can rewrite the`f`

in`⇑f x`

.