Leverage theorem in the reals for the natural numbers

Question

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.)

Answer 1

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

Answer 2

Kevin explained why subtraction of natural numbers can't be automatically casted to reals. Here is a shorter version of Kevin's proof:

example (P R q : ℕ) : R ^ 3 + q ^ 3 + P * R * q - R ^ 3 = q * (q ^ 2 + P * R) := by
  rw [add_assoc, Nat.add_sub_self_left] -- get rid of subtraction
  zify -- cast to integers
  ring