Commit 2022-06-27 16:25 2558b3b3

feat(*): Upgrade to lean 3.44.1c (#14984) The changes are:

• reflected a is now spelt reflected _ a, as the argument was made explicit to resolve type resolution issues. We need to add new instances for with_top and with_bot as these are no longer found via the option instance. These new instances are an improvement, as they can now use bot and top instead of none.
• Some nat order lemmas in core have been renamed or had their argument explicitness adjusted.
• dsimp now applies iff lemmas, which means it can end up making more progress than it used to. This appears to impact split_ifs too.
• opposite.op_inj_iff shouldn't be proved until after opposite is irreducible (where iff.rfl no longer works as a proof), otherwise dsimp is tricked into unfolding the irreducibility which puts the goal state in a form where no further lemmas can apply. We skip Lean 3.44.0c because the support in that version for iff lemmas in dsimp had some unintended consequences which required many undesirable changes.