Commit 2023-12-04 15:55 31d8db6f

View on Github →

feat: rify tactic (#7990)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

added theorem Rat.cast_ofNat

Modified Mathlib/Data/Rat/Floor.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Attr/Register.lean

Created Mathlib/Tactic/Rify.lean

added theorem Mathlib.Tactic.Rify.ofNat_rat_real

added theorem Mathlib.Tactic.Rify.rat_cast_eq

added theorem Mathlib.Tactic.Rify.rat_cast_le

added theorem Mathlib.Tactic.Rify.rat_cast_lt

added theorem Mathlib.Tactic.Rify.rat_cast_ne

Modified Mathlib/Tactic/Zify.lean

added theorem Mathlib.Tactic.Zify.Nat.cast_sub_of_add_le

added theorem Mathlib.Tactic.Zify.Nat.cast_sub_of_lt

Created test/Rify.lean