How to manipulate rational numbers algebraically

Stream: new members

[Will Bradley]

I've been trying to do a proof that sqrt 2 is irrational, but I'm stuck on manipulating the numerator and denominator algebraically. Specifically, how do I go from (p / q)^2 = 2 to p^2 = 2q^2? And is there a more idiomatic way to get from p / q = sqrt 2 to (p / q)^2 = 2, without invoking cast_inj?

import Mathlib

example : Irrational (Real.sqrt 2) := by
  intro ⟨x, hx⟩
  let p := x.num
  let q := x.den
  have: x^2 = 2 := by
    have := Real.sq_sqrt (show 0 ≤ 2 by norm_num)
    simp [(Rat.cast_inj (α := ℝ) (m := x^2) (n := 2)).mp, this, hx]
  have: p^2 = 2*q^2 := by sorry
  sorry

[Riccardo Brasca]

You can probably formalize any math proof you have. My suggestion is to write down an extremely precise math proof, and try to formalize each step.

[Ruben Van de Velde]

import Mathlib

example : Irrational (Real.sqrt 2) := by
  intro ⟨x, hx⟩
  let p := x.num
  let q := x.den
  have: x^2 = 2 := by
    have := Real.sq_sqrt (show 0 ≤ 2 by norm_num)
    simp [(Rat.cast_inj (α := ℝ) (m := x^2) (n := 2)).mp, this, hx]
  have: p^2 = 2*q^2 := by
    simp [p, q]
    rw [← Rat.num_div_den x] at this
    rw [@div_pow] at this -- rw? at this
    rw [eq_comm] at this -- guess
    rw [eq_div_iff_mul_eq] at this
    · rw [eq_comm] at this
      norm_cast at this
    · have := Rat.den_nz x
      positivity
  sorry

[Jon Bannon]

Is there an encyclopedic list of Lean 4 tactics? I can't find such a thing in the API documentation, so I figure I'm looking in the wrong places.

[Kevin Buzzard]

(asked again here https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean.204.20tactics.20list/near/439268892). Please don't double-post -- you can move posts.