A wrong proof, kept up on purpose: \sqrt{4} is irrational

Left here deliberately so you can see what a rejection looks like. The claim is false and the kernel says so — and what it hands back is the goal it still had open, which is the part worth reading.

import Mathlib
theorem sqrt_four_irrational : Irrational (Real.sqrt 4) := by
  norm_num

/work/Submission.lean:2:59: error: unsolved goals
⊢ False