Commit 2023-12-11 11:08 9f2bb70b
View on Github →fix: correct bad handling of rat literals in ring_nf
(#8836)
Reported on Zulip:
import Mathlib.Data.Real.Basic local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4[#2220](https://github.com/leanprover-community/mathlib4/pull/2220) example {n : ℝ} : (n + 1 / 2) ^ 2 * (n + 1 + 1 / 3) ≤ (n + 1 / 3) * (n + 1) ^ 2 := by ring_nf
After the
ring_nf
call, the goal looks like:↑(Int.ofNat 1) / ↑3 + n * (↑(Int.ofNat 19) / ↑12) + n ^ 2 * (↑(Int.ofNat 7) / ↑3) + n ^ 3 ≤ ↑(Int.ofNat 1) / ↑3 + n * (↑(Int.ofNat 5) / ↑3) + n ^ 2 * (↑(Int.ofNat 7) / ↑3) + n ^ 3
This removes the unwanted Int.ofNat
and coercions.
The docstring was apparently incorrect on Rat.rawCast
(according to @digama0).
With that in mind, it's just a case of fixing the local lemmas used to clean up, to reflect the actual invariant instead of the previously-documented one.
This also fixes a hang when using mode = .raw
, by using only a single pass to prevent 1
recursively expanding to Nat.rawCast 1 + 0
.