How to prove that the real number 2 < 3?

Stream: new members

[Martin C. Martin]

import Mathlib.Data.Real.Basic

example : (2 : ℝ) < 3 := sorry

simp doesn't make any progress, and I'm not sure what else to try.

[Shreyas Srinivas]

norm_num?

[Martin C. Martin]

Ah thanks!

[Kevin Buzzard]

There should maybe be a better answer to the general question of "I don't know the 40 or so standard mathlib tactics so don't know how to make progress on this math-simple goal". I mean, a better answer than "go and read Mathematics In Lean and learn what all the tactics do" or "in your case this tactic works". Does hint solve this one or does it just melt your machine?

[Martin C. Martin]

Thanks Kevin. My Mathlib checkout doesn't have Mathlib.Tactic.Hint. Is it new?

[Martin C. Martin]

I have 4.3.0-rc1. I'll try upgrading to rc2.

[Riccardo Brasca]

It's probably not imported by Mathlib.Data.Real.Basic.

[Riccardo Brasca]

Try

import Mathlib.Tactic

[Shreyas Srinivas]

Kevin Buzzard said:

There should maybe be a better answer to the general question of "I don't know the 40 or so standard mathlib tactics so don't know how to make progress on this math-simple goal". I mean, a better answer than "go and read Mathematics In Lean and learn what all the tactics do" or "in your case this tactic works". Does hint solve this one or does it just melt your machine?

@Martin Dvořák 's Cheatsheet? EDIT: it would be cool to have in the docview

[Riccardo Brasca]

hint is instantaneous on my machine, and it says that linarith does the job.

[Riccardo Brasca]

BTW show_term linarith produces a huge term (that doesn't work), why show_term norm_num is much shorter.

[Martin Dvořák]

Shreyas Srinivas said:

Martin Dvořák 's Cheatsheet? EDIT: it would be cool to have in the docview

Which one did you want?
https://github.com/madvorak/lean4-tactics
Or the printable one?

[Damiano Testa]

Riccardo Brasca said:

BTW show_term linarith produces a huge term (that doesn't work), why show_term norm_num is much shorter.

There is also the shorter proof Nat.cast_lt.mpr (Nat.lt.base 2).

[Shreyas Srinivas]

Martin Dvořák said:

Shreyas Srinivas said:

Martin Dvořák 's Cheatsheet? EDIT: it would be cool to have in the docview

Which one did you want?
https://github.com/madvorak/lean4-tactics
Or the printable one?

The link version should do