Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-21 01:39 80700498

View on Github →

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]

Estimated changes