Commit 2020-05-03 08:34 a223bbb6

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.