Help me prove sqrt(6) is irrational?

Stream: new members

[Mr Proof]

My proof so far:

import Mathlib

theorem irrationalSqrt6 : Irrational (√6) := by
  have h:(√6)^2 = 6 := by norm_num
  have q: 2 < √6 := by rw [Real.lt_sqrt];norm_num;simp
  have p: √6 < 3 :=by rw [Real.sqrt_lt];norm_num;simp;simp
  have g:Not (exists y:Int, √6 = y) :=by apply sorry
  simpa using irrational_nrt_of_notint_nrt 2 6 h g

I'm using irrational_nrt_of_notint_nrt but it needs to know that √6 is not an integer. So I've proved it lies between 2 and 3. But there I'm stuck.

I think I really need to find a better way of searching for tactics. What are the best strategies for looking for tactics? There's so many!

[Kyle Miller]

We're working on getting a list of tactics into the mathlib docs, but for now you can use the #help tactic command.

There's a 9-month-old copy of that output here: https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md

[Kyle Miller]

Here are some tricks:

theorem irrationalSqrt6 : Irrational (√6) := by
  have h:(√6)^2 = 6 := by simp
  have q: 2 < √6 := by convert_to √4 < √6; simp; gcongr; norm_num
  have p: √6 < 3 :=by convert_to √6 < √9; simp; gcongr; norm_num
  have g:¬ ∃ y:Int, √6 = y := by
    push_neg
    intro y h
    rw [h] at p q
    norm_cast at p q
    omega
  simpa using irrational_nrt_of_notint_nrt 2 6 h g

[Mr Proof]

Thanks. The convert_to didn't seem to work on the web version (maybe it's not up to date yet) so I just used my original definitions of p and q and the rest seemed to work.

So omega I guess just basically solves integer equations, and in this case it found that there was no solution.

[Kyle Miller]

convert_to does exactly what it's supposed to do in the web version. Instead, it's that I forgot I had my simproc from the other thread still defined, so simp was able to prove the 2 = √4 goal.

[Mr Proof]

Ah :grinning_face_with_smiling_eyes:. Yeah that simproc is very useful. Hope you will add it to Lean even as just an extra tactic. Could call it sqrt_norm perhaps?

[Asei Inoue]

I’m maintaining the list of all tactics

https://github.com/Seasawher/mathlib4-tactics