mathlib3

801c013f - refactor(tactic/lift): remove attribute/simp-set and swap side goal (#16565)

refactor(tactic/lift): remove attribute/simp-set and swap side goal (#16565) This PR accomplishes two things: * It simplifies the design of the `lift` tactic (while keeping roughly the same user interface, see below). Specifically, it does not need an attribute set to simplify expressions coming from `can_lift` instances. - This will make the tactic easier to port to Lean 4. - It accomplishes this by moving two fields of `can_lift` into `out_param`s. So writing the instances is slightly different from before. * If the `using h` clause is left out, then `lift` produces a subgoal. This subgoal used to come after the main goal. But I think it is natural to make it the first goal. So that you can write ``` lift n to nat with k, { linarith }, ``` instead of ``` lift n to nat using by { linarith } with k, ```