Real to Int

Stream: general

[Eric Chen]

Hey all,

Is there a way to apply a theorem for real numbers to integers? As integers are contained in the reals, this should theoretically be possible.

For instance, consider the very simple example:

import Mathlib.Tactic.Ring
import Mathlib.Data.Int.Basic
import Mathlib.Data.Real.Basic
theorem fact
  (a b : Real):
  (a+b)^2 = a^2 + 2*a*b + b^2:= by ring

theorem factWithInt
  (a b : Int):
  (a + b)^2 = a^2 + 2*a*b + b^2 := by
    --How do I use "fact" to deduce "factWithInt"?

[Mario Carneiro]

theorem factWithInt
    (a b : Int) :
    (a + b)^2 = a^2 + 2*a*b + b^2 := by
  exact_mod_cast fact a b

[Mario Carneiro]

what this actually does is first assert fact a b (which is really fact ↑a ↑b), which produces a statement about real numbers with lots of cast expressions in it, then bubbles all the casts out to get a statement about integers