## Stream: maths

### Topic: Sqrt of 2 is irrational

#### Sayantan Majumdar (May 05 2020 at 11:25):

I am trying to prove ¬(∃ p : ℚ, p * p = 2). I have reached to a somewhat good place but there is a coercion issue

example : ¬(∃ p : ℚ, p * p = 2) :=
begin
intro h,
apply exists.elim h,
assume p,
assume h₀,
have h₁, from @rat.eq_iff_mul_eq_mul (p * p) (2 : ℚ),
have h₂, from (iff.elim_left h₁),
have h₃, from eq.symm (h₂ h₀),
have h₄, from (rat.coe_nat_denom 2),
-- have h₅, from @eq.subst ℤ (λ x, (2 : ℚ).num * ↑((p * p).denom) = (p * p).num * x) ↑((2 : ℚ).denom) 1 h₄ h₃,
have h₅, from rat.coe_nat_num 2,
have h₆, from rat.coe_int_denom 2,
have h₇, from rat.coe_int_num 2,
have h₈, from rat.coe_int_eq_of_int 2,
sorry,
end


#### Sayantan Majumdar (May 05 2020 at 11:26):

has anyone done this proof in a better way?

#### Sayantan Majumdar (May 05 2020 at 11:26):

I am having trouble getting rid of the 2.denom part

#### Patrick Massot (May 05 2020 at 11:44):

I have zero experience using rational numbers in Lean but I would start with:

import tactic
example : ¬(∃ p : ℚ, p * p = 2) :=
begin
suffices : ¬ ∃ a b : ℤ, a*a = 2*b*b,
{ rintro ⟨p, h₀⟩,
apply this,
rw rat.eq_iff_mul_eq_mul at h₀,
use [p.num, p.denom],
norm_cast at h₀,
simpa [mul_assoc, rat.mul_self_num, rat.mul_self_denom] using h₀ },

sorry,
end


#### Patrick Massot (May 05 2020 at 11:45):

Of course you'll find much more by reading https://leanprover-community.github.io/mathlib_docs/data/real/irrational.html

#### Sayantan Majumdar (May 05 2020 at 11:57):

thanks, will try to continue from there

#### Patrick Massot (May 05 2020 at 12:03):

You should also study the use of rintros and rw here (and simpa). It will make your code much more efficient.

#### Patrick Massot (May 05 2020 at 12:04):

Your handling of negation also strongly suggests you would benefit from going through the tutorials project.

#### Sayantan Majumdar (May 05 2020 at 12:09):

thanks, will do. was trying to write everything out to understand where thing have gone wrong

Last updated: May 06 2021 at 18:20 UTC