This is a reasonable approach. You prove this by "relaxing" a to be a real number, namely proving 2 <= (a : Real) <= 3 and then using that to deduce 2 <= (a : Int) <= 3. I'll let you handle how to prove 2 <= (a : Real) <= 3, but let's talk about converting between Int and Real, and more generally casting from one type to another.
Coercion basics
If a has type Int and you write a : Real, what you are telling Lean to do is coerce a from Int to Real. So a is replaced with ↑a. This uparrow symbol (written \u or \uparrow in the Lean vs code plugin) is shorthand for @Int.cast ℝ Real.instIntCast a. You can find this out by hovering over ↑a in the infoview. It also gives this helpful message:
↑x represents a coercion, which converts x of type α to type β, using typeclasses to resolve a suitable conversion function. You can often leave the ↑ off entirely, since coercion is triggered implicitly whenever there is a type error, but in ambiguous cases it can be useful to use ↑ to disambiguate between e.g. ↑x + ↑y and ↑(x + y).
As this message suggests, if Lean is expecting a real number, as in a < Real.pi, then a, ↑a, and (a : ℝ) are all the same.
#check ∀ a : ℤ, a < Real.pi -- ∀ (a : ℤ), ↑a < Real.pi
#check ∀ a : ℤ, ↑a < Real.pi -- ∀ (a : ℤ), ↑a < Real.pi
#check ∀ a : ℤ, (a : ℝ) < Real.pi -- ∀ (a : ℤ), ↑a < Real.pi
One case where a alone wouldn't work is when the expression is valid as either an Int or a Real. In that case, you have to specify the coercion using (a : ℝ) in at least one place.
#check ∀ a : ℤ, ((a : ℝ) / 2) * 2 = a -- ((a : ℝ) / 2) * 2 = a
It is not enough here to just use ↑a since Lean doesn't know what to coerce to. For example, this doesn't coerce at all:
#check ∀ a : ℤ, ↑a / 2 * 2 = a -- ∀ (a : ℤ), a / 2 * 2 = a
Conversely, Lean seems to apply ↑a as far inside as possible. So sometimes one needs to explicitly use ↑ to specify where the conversion should be.
#check ∀ a : ℤ, ((a + a) : ℝ) = (a : ℝ) + (a : ℝ)
-- ∀ (a : ℤ), ↑a + ↑a = ↑a + ↑a
#check ∀ a : ℤ, (↑(a + a) : ℝ) = a + a
-- ∀ (a : ℤ), ↑(a + a) = ↑a + ↑a
Coersion can change the truth value of a theorem
The reason that
have ha : a ^ 2 - 5 * a + 5 = (a - 5/2) ^ 2 - 5/4 := by ring
failed, is that the theorem is false (and ring tells you this), because for the integers, 5/4 = 1 and 5/2 = 2.
#eval (5: ℤ ) / 4 -- 1
#eval (5: ℤ ) / 2 -- 2
(This is similar to say 5 // 4 and 5 // 2 in python if you are familiar with integer division in typical programming languages.)
So this brings us to an important point. Just because you prove a theorem for (a : ℝ) doesn't mean it still holds for a.
How to go back and forth between coercions?
It shouldn't be hard for you to prove 2 <= (a : Real) and (a : Real) <= 3, but that isn't your goal. You want 2 <= a and a <= 3 (which since a is an integer implies that a = 2 or a = 3).
This is a common case in coercions. While it isn't true in general that any theorem of (a : Real) is a theorem of a, it is true that many functions and relations are ↑-invariant (meaning R_ℤ a b ↔ R_ℝ ↑a ↑b) and other functions are ↑-equivariant (meaning ↑(f_ℤ a b) = f_ℝ ↑a ↑b).
These theorems should be readily available in Mathlib, but instead of looking them up, there are tactics to help.
norm_cast normalizes coercions (removing them if possible).
example (a : ℤ) (h : a < 9) : (a : ℝ) < 10 := by
norm_cast -- normalizes coercions (removing them if possible) in goal
/-
a : ℤ
h : a < 9
⊢ a < 10
-/
linarith [h]
example (a : ℤ) (h : (a : ℝ) < 9) : a < 10 := by
norm_cast at h -- normalizes coersions (removing them if possible) in the hypotheses `h`
/-
a : ℤ
h : a < 9
⊢ a < 10
-/
linarith [h]
push_cast pushes coercions inward (again removing them if possible).
example (a b : ℤ) (h : a + b < 9) : ↑ (a + b) < 10 := by
push_cast -- pushes coercions inward (removing them if possible) in the goal
/-
a b : ℤ
h : a + b < 9
⊢ a + b < 10
-/
linarith [h]
example (a b : ℤ) (h : ↑ (a + b) < 9) : a + b < 10 := by
push_cast at h -- pushes coercions inward (removing them if possible) in the hypothesis
/-
a b : ℤ
h : a + b < 9
⊢ a + b < 10
-/
linarith [h]
exact_mod_cast and apply_mod_cast are versions of exact and apply which also normalizes coercions.
example (a : ℤ) (h : a < 10) : (a : ℝ) < 10 := by
exact_mod_cast h -- like `exact` but normalizes coercions first
example (a : ℤ) (h : (a : ℝ) < 10) : a < 10 := by
exact_mod_cast h -- like `exact` but normalizes coercions first
example (a : ℤ) (h : (a : ℝ) < 10) : a < 10 := by
apply_mod_cast h -- like `apply` but normalizes coercions first
rify converts goals on ℕ, ℤ, ℚ, etc. to ℝ. There is also qify for rationals and zify for integers. The zify, qify, rify tactics require Mathlib, while the other ..._cast tactics are available in base Lean.
example (a : ℤ) (h : (a : ℝ) < 9) : a < 10 := by
rify -- converts goal to reals (use `zify` for ℤ and `qify` for ℚ)
/-
a : ℤ
h : ↑a < 9
⊢ ↑a < 10
-/
linarith [h]
example (a : ℤ) (h : (a : ℝ) < 10) : a < 10 := by
rify [h] -- `rify` using `h` as a simp lemma
Other coercions
There are a lot of coercions in Lean. They come up in natural settings where one wants to interpret one type as another because of some canonical embedding (usually a homomorphism).
There are coercions from ℕ to ℚ to ℝ to ℂ; coercions to and from Nat and Fin n; coercions from fields to rings to groups (the forgetful functor); coercions from ℕ to rings, and many more.
New coercions have to be registered so Lean knows about them. For more information see Coercions using Type Classes in Theorem Proving in Lean 4.
