I have a simple identity in the reals:
section
variable {P R q: ℝ}
theorem rq : R ^ 3 + q ^ 3 + P * R * q - R ^ 3 = q * (q ^ 2 + P * R) := by ring
end
Now I want to use it to prove exactly the same identity for the naturals. Actually I can prove it directly by rewriting with the corresponding theorems (but is a bit painful.)
This is not quite as straightforward as you might think, because it's not true in general that if x and y are naturals, then x-y (computed in naturals) coerced to reals, equals (x coerced to reals) - (y coerced to reals). The issue is that if y>x then x-y cannot be mathematically correctly done in the naturals, so e.g. 2-3 in naturals is 0, but 2-3 in reals is -1. So you'll have to convince Lean that the subtraction is not pathological, which is not difficult in your case (e.g. rearrange the brackets on LHS and use Nat.add_sub_self_left), but this will then make the application of theorem rq much harder. Here's some sample code but because of this issue I'm not sure I understand the question, in some sense.
import Mathlib.Tactic
section
variable {P R q: ℝ}
theorem rq : R ^ 3 + q ^ 3 + P * R * q - R ^ 3 = q * (q ^ 2 + P * R) := by ring
end
example (P R q : ℕ) : R ^ 3 + q ^ 3 + P * R * q - R ^ 3 = q * (q ^ 2 + P * R) := by
rw [← Nat.cast_inj (R := ℝ)] -- coerce to reals
push_cast -- push coercions in as far as possible
rw [← rq] -- RHS is now in correct form so can use your lemma
-- problem now is that we have ↑(a - b) on LHS and ↑a - ↑b on RHS
rw [add_assoc, Nat.add_sub_self_left] -- do the subtraction manually by proving it's mathematically valid
push_cast
-- goal now has R^3 + ... - R^3 on RHS but not on LHS
ring