a proof of irrationality of sqrt(2) following https://lawrencecpaulson.github.io/2023/01/18/Sqrt2_irrational.html

sqrt2.lean

import data.real.irrational
import tactic

open real

example : irrational (sqrt 2) :=
begin
  rintro ⟨q, hq⟩,
  have hqnum : 0 ≤ q.num,
  { rw rat.num_nonneg_iff_zero_le,
    have := sqrt_nonneg 2,
    rw ← hq at this,
    assumption_mod_cast, },
  let R := {n : ℕ | n ≠ 0 ∧ ∃ m : ℕ, sqrt 2 * n = m},
  have hR : ∃ n, n ∈ R,
  { refine ⟨q.denom, q.denom_ne_zero, _⟩,
    use q.num.nat_abs,
    rw [← hq],
    norm_cast,
    nth_rewrite 0 [← q.num_div_denom],
    field_simp [q.denom_ne_zero],
    nth_rewrite 0 int.eq_nat_abs_of_zero_le hqnum,
    simp [-int.coe_nat_abs], },
  classical,
  let k := nat.find hR,
  have hk : k ∈ R := nat.find_spec hR,
  have hk2 : 0 < k := nat.pos_of_ne_zero hk.1,
  cases hk.2 with m hm,
  set x' := (sqrt 2 - 1) * k with hkx',
  have foo : (1 : ℝ) < sqrt 2,
  { nth_rewrite 0 ← sqrt_one, apply sqrt_lt_sqrt; norm_num },
  have hx' : 0 < x' := mul_pos (by norm_num [foo]) (by assumption_mod_cast),
  have hk₀ : ∃ k₀ : ℤ, x' = k₀,
  { use m - k, change _ * _ = _, rw [sub_mul, hm], push_cast, ring, },
  cases hk₀ with k₀ hk₀,
  obtain ⟨k', hk'⟩ : ∃ k' : ℕ, x' = k',
  { use k₀.nat_abs, rw hk₀, rw hk₀ at hx', norm_cast at hx',
    nth_rewrite 0 int.eq_nat_abs_of_zero_le hx'.le, refl, },
  have hk'2 : 0 < k',
  { rw hk' at hx', exact_mod_cast hx', },
  have foo' : sqrt 2 < 2,
  { nth_rewrite 1 ← (show sqrt 4 = 2, by {rw sqrt_eq_iff_sq_eq; norm_num } ),
    apply sqrt_lt_sqrt; norm_num, },
  have hk'k : k' < k,
  { suffices : (sqrt 2 - 1) * k < k, change x' < k at this, rw hk' at this, assumption_mod_cast,
    have : (0 : ℝ) < k, assumption_mod_cast,
    nlinarith,
  },
  apply nat.find_min hR hk'k ⟨hk'2.ne', _⟩,
  rw ← hk',
  use 2 * k - m,
  rw [hkx', ← mul_assoc, mul_sub, ← sqrt_mul, sqrt_mul_self, mul_one, sub_mul, hm, nat.cast_sub];
  try {norm_num},
  suffices : (m : ℝ) ≤ 2 * k,
  { assumption_mod_cast, },
  rw ← hm,
  have hk3 : (0 : ℝ) < k, assumption_mod_cast,
  nlinarith,
end