mathlib

80700498 - feat(tactic/lift): add lift tactic (#1315)

feat(tactic/lift): add lift tactic (#1315) * start on lift_to tactic * finish lift tactic * add instance to lift rat to int this required me to move some lemmas from rat/order to rat/basic which had nothing to do with the order on rat * move test to test/tactic.lean * add header and documentation * add more/better documentation * typo * more documentation * rewrite, minor * move import * remove can_lift attribute now we automatically construct the simp set used to simplify Thanks to @cipher1024 for the idea and writing the main part of this code * remove occurrence of [can_lift]