Sqrt of 2 is irrational

Stream: maths

[Sayantan Majumdar]

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]

has anyone done this proof in a better way?

[Sayantan Majumdar]

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

[Patrick Massot]

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]

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

[Sayantan Majumdar]

thanks, will try to continue from there

[Patrick Massot]

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

[Patrick Massot]

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

[Sayantan Majumdar]

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