tactics to calculate inequality

Stream: general

[ZHAO Jinxiang]

example (a b : ℝ) (h1 : a = 2017) (h2: b ≤ 1): b < a := by
  sorry

Is there any tactics to prove this?

[Kevin Buzzard]

linarith

[ZHAO Jinxiang]

Thanks. It works.
Also, how can I prove this?

example (a b : WithBot ℕ) (h1 : a = 2017) (h2: b ≤ 1): b < a := by
  sorry -- linarith seems not working here

[Kevin Buzzard]

import Mathlib

example (a b : WithBot ℕ) (h1 : a = 2017) (h2: b ≤ 1): b < a := by
  -- use the right lemma
  refine lt_of_le_of_lt h2 ?_
  -- now use a tactic
  simp_all

[ZHAO Jinxiang]

Why linarith not working here？

[Kevin Buzzard]

From the docstring:

In theory, linarith should prove any goal that is true in the theory of linear arithmetic over the rationals. While there is some special handling for non-dense orders like Nat and Int, this tactic is not complete for these theories and will not prove every true goal. It will solve goals over arbitrary types that instantiate LinearOrderedCommRing.

WithBot Nat is not covered by these examples.

[ZHAO Jinxiang]

Okay, I see.

[ZHAO Jinxiang]

Another question: Is there any tactics to auto prove this without using refine lt_of_le_of_lt h2 ?_ or apply h2.trans_lt？

[Kevin Buzzard]

import Mathlib

attribute [aesop unsafe apply 50%] lt_of_le_of_lt

example (a b : WithBot ℕ) (h1 : a = 2017) (h2: b ≤ 1): b < a := by
  aesop