Rewrite rational as a/b

Stream: new members

[Matthew Khoriaty]

I completed the Lean Game Server Natural Number Game, Set Theory Game, and Logic Game, and I'm trying to write my first real proof. I'm going for "root 2 is irrational".

From  rootTwo ^ 2 = 2, how can I rewrite it to (a/b) ^2 = 2? More generally, how do you find the theorems you need in your proofs?

root2irrational.jpeg

So far I have:

import Mathlib.Algebra.Algebra.Rat
import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Init.Data.Nat.Lemmas
example (rootTwo : ℚ): ¬(rootTwo ^ 2 = 2) :=
by
  by_contra s2

[Kalle Kytölä]

Moogle and Loogle are good general search tools (both useful, very complementary use cases) for Lean and Mathlib content.

Another useful strategy in VS Code is to guess the name and use autocomplete, for example let b := Rat.de and then Ctrl+space autocompletion finds Rat.den. This is even more useful with lemmas with longer names (e.g. Rat.num_div_den, which is pretty directly what you seem to be looking for).

Finally, if you have a pretty clean statement of something that you believe should be in that form (or strictly more general) in Mathlib, you can write that statement in a have my_statement := ... or example : ... and then try by exact?. That finds if a single lemma in Mathlib implies your statement with the current hypothesis in their literal form.

So you can make progress by

import Mathlib.Algebra.Algebra.Rat
import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Init.Data.Nat.Lemmas
example (rootTwo : ℚ): ¬(rootTwo ^ 2 = 2) := by
  by_contra s2
  rw [← Rat.num_div_den rootTwo] at s2
  sorry

[Kalle Kytölä]

Btw, should we have linkifiers to Moogle and Loogle on this Zulip? I think search questions are sufficiently common to make the linkifiers useful.