Linarith for real number

Stream: Is there code for X?

[Casavaca]

How to prove this?

example (i : ℕ) (h : i < 90) : (i : ℝ) * 2 < 180 := by ???

Edit:

example (i : ℕ) (k : ℤ) (hi : i < 90) (hk : 0 < k) : (i : ℝ) * 2 < k * 180 := by ???

[Vincent Beffara]

import Mathlib

example (i : ℕ) (h : i < 90) : (i : ℝ) * 2 < 180 := by
  norm_cast ; omega

[Casavaca]

You are right. I updated the example.

[Vincent Beffara]

import Mathlib

example (i : ℕ) (k : ℤ) (hi : i < 90) (hk : 0 < k) : (i : ℝ) * 2 < k * 180 := by
  norm_cast ; omega

:grinning_face_with_smiling_eyes:

[Casavaca]

You are right. I tried linarith which doesn't work, but omega does. Thank you.

[Kim Morrison]

I wonder why linarith fails. It seems like it should be in scope.

[Kim Morrison]

Ah:

import Mathlib

example (i : ℕ) (k : ℤ) (hi : i < 90) (hk : 0 < k) : (i : ℝ) * 2 < k * 180 := by
  norm_cast
  zify at *
  linarith