The minploy of √p + √q is X^4 - 2 (p + q)X^2 + (p - q)^2

Stream: Is there code for X?

[张守信(Shouxin Zhang)]

How to solve the following example with one line of code?

example (p q : ℕ) :
  (√↑p + √↑q) ^ 4 - 2 * (↑p + ↑q) * (√↑p + √↑q) ^ 2 + (↑p - ↑q) ^ 2 = 0 := by

  sorry

I know that through some simple ring_nf and simp, show ... by ... operations, I can eventually prove this example. But this is not what I want. I think there should be a tactic similar to ring_nf that can solve it.

[Ruben Van de Velde]

There seems to be a recent flurry of interest in single-tactic proofs, and I don't understand where it comes from. It might be possible to create a tactic for this case, but it's not obvious to me why it should be a priority

[Ruben Van de Velde]

This might be interesting

import Mathlib

@[simp]
lemma aux (p n : ℕ) [n.AtLeastTwo] : (√p) ^ n = p * (√p) ^ (n - 2) := by
  have : 2 ≤ n := by exact Nat.AtLeastTwo.prop
  have : n = n - 2 + 2 := by exact (Nat.sub_eq_iff_eq_add this).mp rfl
  conv_lhs => rw [this]
  simp [pow_add, mul_comm]

example (p q : ℕ) :
  (√↑p + √↑q) ^ 4 - 2 * (↑p + ↑q) * (√↑p + √↑q) ^ 2 + (↑p - ↑q) ^ 2 = 0 := by
  ring_nf
  simp
  ring_nf

[张守信(Shouxin Zhang)]

Ruben Van de Velde said:

There seems to be a recent flurry of interest in single-tactic proofs, and I don't understand where it comes from. It might be possible to create a tactic for this case, but it's not obvious to me why it should be a priority

"It might be possible to create a tactic for this case", that's true.

[Kevin Buzzard]

Do you have some specific scope in mind for your tactic? It's not reasonable to want a tactic that "proves all obvious things", that's not really how it works

[Johan Commelin]

import Mathlib

example (p q : ℕ) :
  (√↑p + √↑q) ^ 4 - 2 * (↑p + ↑q) * (√↑p + √↑q) ^ 2 + (↑p - ↑q) ^ 2 = 0 := by
  have : (√p + √q) ^ 4 - 2 * (√p ^ 2 + √q ^ 2) * (√p + √q) ^ 2 + (√p ^ 2 - √q ^ 2) ^ 2 = 0 := by ring
  simpa [(Real.sq_sqrt (Nat.cast_nonneg' _))]

[张守信(Shouxin Zhang)]

The remaining question is how to prove Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℚ[X]). I saw a proof on ℤ[X] on the zulip, but unlike there, I don't know how to construct a prime ideal on ℚ. Mathematically, I know that picking a natural number 2 and then using eisenstein_criterion makes everything very simple. But how to implement it in Lean4?

[Jz Pan]

It's enough to prove it irreducible on ℤ[X]. Then use docs#Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast

[Jz Pan]

Eisenstein criterion: docs#Polynomial.irreducible_of_eisenstein_criterion and docs#Polynomial.IsEisensteinAt.irreducible (same API duplicated twice)

[Riccardo Brasca]

Note that the main point of Mathlib.RingTheory.Polynomial.Eisenstein.Basic is to develop the theory of Polynomial.IsWeaklyEisensteinAt, that is needed for dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt.

To prove irreducibility of an explicit polynomial Polynomial.irreducible_of_eisenstein_criterion is perfectly fine.

[张守信(Shouxin Zhang)]

Ruben Van de Velde said:

There seems to be a recent flurry of interest in single-tactic proofs, and I don't understand where it comes from. It might be possible to create a tactic for this case, but it's not obvious to me why it should be a priority

Learned something new! :+1:

[张守信(Shouxin Zhang)]

After working on this for a while, I've found that it seems impossible to directly prove this polynomial's irreducibility using Polynomial.Eisenstein.

Furthermore, after some basic case analysis, it appears that even using the Rational Root Theorem to prove the polynomial has no rational roots isn't feasible.

Everything points to one approach: using the quadratic formula. Mathematically, this makes everything much simpler.

$$\begin{aligned} & x^4 - 2(p + q)x^2 + (p - q)^2 = 0 \iff x^2 = (p + q) \pm 2\sqrt{pq} \\ & x \in \Z \to x^2 \in \Z \to \sqrt{pq} \in \Z \to {\rm contradiction} \\ & {\rm and} (x^2 + bx + a)(x^2 + dx +c) = x^4 - 2(p + q)x^2 + (p - q)^2 = 0 \\ & \to a,c = (p + q) \pm 2\sqrt{pq} \to {\rm contradiction} \end{aligned}$$

But does lib have a formula for finding the roots of quadratic equations?
(... Sorry. A few times ago, I found it quadratic_eq_zero_iff. Continue working...)
My code is follow:

lemma ex1 (p q : ℤ) (h : Prime p) :
  4*p = q^2 → False := by
  intro hq
  cases' Int.even_or_odd q with hq_even hq_odd
  . obtain ⟨k, rfl⟩ := hq_even
    ring_nf at hq
    simp at hq
    contrapose! h
    refine IsSquare.not_prime ?_
    rw [hq]
    exact IsSquare.sq k
  . obtain ⟨k, rfl⟩ := hq_odd
    ring_nf at hq
    have : 4*(p - k^2 - k) = 1 := by linarith
    have : (4 : ℤ)∣1 := ⟨p - k^2 - k, this.symm⟩
    norm_num at this

open Polynomial in
example (p q : ℤ)
  (hp : 0 < p) (hq : 0 < q)
  (hp₁ : Prime p) (hq₁ : Prime q):
  Irreducible (X ^ 4 - 2 * (C (p : ℤ) + C (q : ℤ)) * X ^ 2 + C ((p : ℤ) - (q : ℤ))^2 : ℤ[X]) := by
  set h := (X ^ 4 - 2 * (C (p : ℤ) + C (q : ℤ)) * X ^ 2 + C ((p : ℤ) - (q : ℤ))^2 : ℤ[X]) with hh
  have hh₁ : h.natDegree = 4 := by unfold h; compute_degree!
  have hh₂ : h.Monic := by unfold h; monicity!
  rw [Monic.irreducible_iff_natDegree ‹_›]
  constructor
  . rw [← Monic.natDegree_pos ‹_›, hh₁]; simp
  . intro f g hf hg hfg
    have : f.natDegree ≤ 4 := by
      rw [← hh₁, ← hfg]
      simp [Monic.natDegree_mul hf hg, le_add_iff_nonneg_right]
    set n := f.natDegree with hn
    have mul_def := Monic.natDegree_mul hf hg
    rw [hfg, hh₁] at mul_def
    interval_cases n
    . simp
    . right
      sorry
    . exfalso
      have f_form := as_sum_range_C_mul_X_pow f
      simp [← hn, Finset.range_succ] at f_form
      simp [← hn, ← (Nat.sub_eq_iff_eq_add' this)] at mul_def
      have g_form := as_sum_range_C_mul_X_pow g
      simp [← mul_def, Finset.range_succ] at g_form
      have tempf : f.coeff 2 = 1 :=
        Mathlib.Tactic.ComputeDegree.coeff_congr_lhs hf hn.symm
      have tempg : g.coeff 2 = 1 :=
        Mathlib.Tactic.ComputeDegree.coeff_congr_lhs hg mul_def.symm
      simp [tempf] at f_form; clear tempf
      simp [tempg] at g_form; clear tempg
      have fg_form : f * g = X^4 + C (f.coeff 1 + g.coeff 1) * X^3 +
        C (f.coeff 0 + g.coeff 0 + f.coeff 1 * g.coeff 1) * X^2 +
        C (f.coeff 0 * g.coeff 1 + g.coeff 0 * f.coeff 1) * X +
        C (f.coeff 0 * g.coeff 0) := by
        nth_rw 1 [f_form, g_form]; simp; ring_nf
      set a := f.coeff 0
      set b := f.coeff 1
      set c := g.coeff 0
      set d := g.coeff 1
      simp [-eq_intCast, hfg, hh] at fg_form
      have coeff3 : b + d = 0 := by
        have := congrFun (congrArg coeff fg_form) 3
        simp [-eq_intCast, ← map_sub, ← map_pow, coeff_mul_X_pow'] at this
        exact this.symm
      conv_rhs at fg_form => rw [← map_add, coeff3, map_zero, zero_mul, add_zero]
      rw [add_eq_zero_iff_eq_neg'] at coeff3
      rw [coeff3] at fg_form
      have coeff2 := congrFun (congrArg coeff fg_form) 2
      simp [-eq_intCast, ← map_sub, ← map_pow, coeff_mul_X_pow'] at coeff2
      have coeff1 := congrFun (congrArg coeff fg_form) 1
      simp [-eq_intCast, ← map_sub, ← map_pow, coeff_mul_X_pow'] at coeff1
      have coeff0 := congrFun (congrArg coeff fg_form) 0
      simp [-eq_intCast, ← map_sub, ← map_pow, coeff_mul_X_pow'] at coeff0
      simp [eq_neg_add_iff_add_eq] at coeff1
      rcases coeff1 with coeff1 | coeff1
      . simp [← coeff1] at coeff2 coeff0
        rw [← pow_two] at coeff0
        rw [sq_eq_sq_iff_eq_or_eq_neg] at coeff0
        rcases coeff0 with coeff0 | coeff0
        . simp [← coeff0] at coeff2
          rw [neg_eq_iff_add_eq_zero] at coeff2
          ring_nf at coeff2
          rw [Int.sub_eq_zero] at coeff2
          apply ex1 p b ‹_›; linarith
        . simp [@Int.eq_neg_comm] at coeff0
          simp [coeff0, neg_eq_iff_add_eq_zero] at coeff2
          ring_nf at coeff2
          apply ex1 q b ‹_›; linarith
      . simp [coeff1] at coeff2

        sorry
    . right
      sorry
    . right; simp_all

[Jz Pan]

张守信(Shouxin Zhang) said:

example (p q : ℤ)
  (hp : 0 < p) (hq : 0 < q)
  (hp₁ : Prime p) (hq₁ : Prime q):
  Irreducible ...

Unfortunately, this result is incorrect for p = q case.

[Riccardo Brasca]

Can you write down a very precise mathematical proof that the polynomial is irreducible?

[Riccardo Brasca]

For example, if p=45 and q=5 the your polynomial is not irreducible.

[Riccardo Brasca]

The minimal polynomial is x^2-80.

[Riccardo Brasca]

This is just to say that you should first of all have a precise proof, otherwise formalization will be basically impossible.

[张守信(Shouxin Zhang)]

Done it.

open Polynomial in
theorem minploy_of_coprime_pq (p q : ℤ)
  (hp : 0 < p) (hq : 0 < q)
  (hp₁ : Prime p) (hq₁ : Prime q) (hpq : IsCoprime p q):
  Irreducible (X ^ 4 - 2 * (C (p : ℤ) + C (q : ℤ)) * X ^ 2 + C ((p : ℤ) - (q : ℤ))^2 : ℤ[X]) := by
  set h := (X ^ 4 - 2 * (C (p : ℤ) + C (q : ℤ)) * X ^ 2 + C ((p : ℤ) - (q : ℤ))^2 : ℤ[X]) with hh
  have hh₁ : h.natDegree = 4 := by unfold h; compute_degree!
  have hh₂ : h.Monic := by unfold h; monicity!
  rw [Monic.irreducible_iff_natDegree ‹_›]
  constructor
  . rw [← Monic.natDegree_pos ‹_›, hh₁]; simp
  . intro f g hf hg hfg
    have : f.natDegree ≤ 4 := by
      rw [← hh₁, ← hfg]
      simp [Monic.natDegree_mul hf hg, le_add_iff_nonneg_right]
    set n := f.natDegree with hn
    have mul_def := Monic.natDegree_mul hf hg
    rw [hfg, hh₁] at mul_def
    interval_cases n
    . simp
    . exfalso
      have f_form := as_sum_range_C_mul_X_pow f
      simp [← hn, Finset.range_succ] at f_form
      simp [Mathlib.Tactic.ComputeDegree.coeff_congr_lhs hf hn.symm] at f_form
      rw [← eq_intCast C, show C (f.coeff 0) = - C (-f.coeff 0) by simp] at f_form
      set a := -f.coeff 0
      rw [@Mathlib.Tactic.RingNF.add_neg] at f_form
      have := dvd_mul_right f g
      nth_rw 1 [f_form, hfg, dvd_iff_isRoot] at this
      set h' : ℤ[X] := X ^ 2 - 2 * (C p + C q) * X + C (p - q) ^ 2 with hh'
      have h'_expand : expand _ 2 h' = h := by
        rw [hh', hh]
        simp [← @npow_mul]
        left
        rw [coe_expand]; simp only [eval₂_ofNat]
      replace this : h'.IsRoot (a^2) := by
        rw [← h'_expand] at this
        rw [IsRoot.def] at this ⊢
        rwa [expand_eval] at this
      have discrim_eq : discrim (1 : ℝ) (-2 * (p + q)) ((p - q) ^ 2) = (4*Real.sqrt (p*q)) * (4*Real.sqrt (p*q)):= by
          unfold discrim
          rw [← pow_two]; ring_nf
          have : 0 ≤ p*q := by nlinarith
          rw [ex2 ((p : ℝ)*q) (by
            rify at this; rwa [])]
      set b := a^2
      replace discrim_eq := quadratic_eq_zero_iff (by norm_num : (1 : ℝ) ≠ 0) discrim_eq b
      simp [← pow_two] at discrim_eq; ring_nf at discrim_eq
      simp [IsRoot.def, h'] at this; rify at this; ring_nf at this
      rw [discrim_eq] at this
      have temp : ¬ Irrational (@Int.cast ℝ _ (b - p -q)) := by simp
      rcases this with this | this
      . replace : (@Int.cast ℝ _ (b - p -q)) = √(↑p * ↑q) * 2 := by
          simp [this]; ring_nf
        contrapose! temp
        rw [this, show (2 : ℝ) = @Rat.cast ℝ _ 2 by rfl]
        apply Irrational.mul_rat ?_ (by norm_num)
        exact ex3 p q hp hq hp₁ hq₁ hpq
      . replace : (@Int.cast ℝ _ (b - p -q)) = -√(↑p * ↑q) * 2 := by
          simp [this]
        contrapose! temp
        rw [this]; simp only [neg_mul, irrational_neg_iff, h']
        rw [show (2 : ℝ) = @Rat.cast ℝ _ 2 by rfl]
        apply Irrational.mul_rat ?_ (by norm_num)
        exact ex3 p q hp hq hp₁ hq₁ hpq
    . exfalso
      have f_form := as_sum_range_C_mul_X_pow f
      simp [← hn, Finset.range_succ] at f_form
      simp [← hn, ← (Nat.sub_eq_iff_eq_add' this)] at mul_def
      have g_form := as_sum_range_C_mul_X_pow g
      simp [← mul_def, Finset.range_succ] at g_form
      have tempf : f.coeff 2 = 1 :=
        Mathlib.Tactic.ComputeDegree.coeff_congr_lhs hf hn.symm
      have tempg : g.coeff 2 = 1 :=
        Mathlib.Tactic.ComputeDegree.coeff_congr_lhs hg mul_def.symm
      simp [tempf] at f_form; clear tempf
      simp [tempg] at g_form; clear tempg
      have fg_form : f * g = X^4 + C (f.coeff 1 + g.coeff 1) * X^3 +
        C (f.coeff 0 + g.coeff 0 + f.coeff 1 * g.coeff 1) * X^2 +
        C (f.coeff 0 * g.coeff 1 + g.coeff 0 * f.coeff 1) * X +
        C (f.coeff 0 * g.coeff 0) := by
        nth_rw 1 [f_form, g_form]; simp; ring_nf
      set a := f.coeff 0
      set b := f.coeff 1
      set c := g.coeff 0
      set d := g.coeff 1
      simp [-eq_intCast, hfg, hh] at fg_form
      have coeff3 : b + d = 0 := by
        have := congrFun (congrArg coeff fg_form) 3
        simp [-eq_intCast, ← map_sub, ← map_pow, coeff_mul_X_pow'] at this
        exact this.symm
      conv_rhs at fg_form => rw [← map_add, coeff3, map_zero, zero_mul, add_zero]
      rw [add_eq_zero_iff_eq_neg'] at coeff3
      rw [coeff3] at fg_form
      have coeff2 := congrFun (congrArg coeff fg_form) 2
      simp [-eq_intCast, ← map_sub, ← map_pow, coeff_mul_X_pow'] at coeff2
      have coeff1 := congrFun (congrArg coeff fg_form) 1
      simp [-eq_intCast, ← map_sub, ← map_pow, coeff_mul_X_pow'] at coeff1
      have coeff0 := congrFun (congrArg coeff fg_form) 0
      simp [-eq_intCast, ← map_sub, ← map_pow, coeff_mul_X_pow'] at coeff0
      simp [eq_neg_add_iff_add_eq] at coeff1
      rcases coeff1 with coeff1 | coeff1
      . simp [← coeff1] at coeff2 coeff0
        rw [← pow_two] at coeff0
        rw [sq_eq_sq_iff_eq_or_eq_neg] at coeff0
        rcases coeff0 with coeff0 | coeff0
        . simp [← coeff0] at coeff2
          rw [neg_eq_iff_add_eq_zero] at coeff2
          ring_nf at coeff2
          rw [Int.sub_eq_zero] at coeff2
          apply ex1 p b ‹_›; linarith
        . simp [@Int.eq_neg_comm] at coeff0
          simp [coeff0, neg_eq_iff_add_eq_zero] at coeff2
          ring_nf at coeff2
          apply ex1 q b ‹_›; linarith
      . simp [coeff1] at coeff2
        clear coeff3 coeff1
        rw [neg_eq_iff_eq_neg, show -(_) = -1 * (a + c) by ring] at coeff2
        rw [show a * c = 1 * a * c by ring] at coeff0
        have temp := (roots_quadratic_eq_pair_iff_of_ne_zero (by norm_num : (1 : ℤ) ≠ 0)).2 (And.intro coeff2 coeff0)
        have : (C 1 * X ^ 2 + C (2 * (p + q)) * X + C ((p - q) ^ 2) : ℤ[X]).IsRoot a := by
          rw [← mem_roots (by
            simp
            refine Monic.ne_zero_of_ne ?_ ?_
            . simp
            . monicity!)]
          rw [temp]; simp
        rw [IsRoot.def] at this
        simp at this
        have discrim_eq : discrim (1 : ℝ) (2 * (p + q)) ((p - q) ^ 2) = (4*Real.sqrt (p*q)) * (4*Real.sqrt (p*q)):= by
          unfold discrim
          rw [← pow_two]; ring_nf
          have : 0 ≤ p*q := by nlinarith
          rw [ex2 ((p : ℝ)*q) (by
            rify at this; rwa [])]
        replace discrim_eq := quadratic_eq_zero_iff (by norm_num : (1 : ℝ) ≠ 0) discrim_eq
        specialize discrim_eq a
        simp [← pow_two] at discrim_eq
        rify at this
        rw [discrim_eq] at this
        ring_nf at this
        rw [@neg_sub_left, @eq_neg_add_iff_add_eq, eq_neg_add_iff_add_eq, neg_sub_comm, @eq_sub_iff_add_eq] at this
        ring_nf at this
        rcases this with this | this
        . simp only [← Int.cast_add] at this
          have temp : @Int.cast ℝ _ (q + p + a ) ∈ Set.range ((↑) : ℤ → ℝ) := by
            rw [Set.mem_range]
            use q + p + a
          rw [this] at temp
          simp only [Set.mem_range] at temp
          obtain ⟨y, hy⟩ := temp
          have temp : ¬ Irrational (y : ℝ) := by simp
          contrapose! temp
          rw [hy, show (2 : ℝ) = @Rat.cast ℝ _ 2 by rfl]
          apply Irrational.mul_rat ?_ (by norm_num)
          exact ex3 q p hq hp hq₁ hp₁ (id (IsCoprime.symm hpq))
        . simp only [← Int.cast_add] at this
          have temp : ¬ Irrational (@Int.cast ℝ _ (q + p + a )) := by simp
          contrapose! temp
          rw [this, irrational_neg_iff, show (2 : ℝ) = @Rat.cast ℝ _ 2 by rfl]
          apply Irrational.mul_rat ?_ (by norm_num)
          exact ex3 q p hq hp hq₁ hp₁ (id (IsCoprime.symm hpq))
    . exfalso
      have g_form := as_sum_range_C_mul_X_pow g
      rw [← hn] at mul_def
      simp [← propext (Nat.sub_eq_iff_eq_add' this)] at mul_def
      simp [← mul_def, Finset.range_succ] at g_form
      simp [Mathlib.Tactic.ComputeDegree.coeff_congr_lhs hg mul_def.symm] at g_form
      rw [← eq_intCast C, show C (g.coeff 0) = - C (-g.coeff 0) by simp] at g_form
      set a := -g.coeff 0
      rw [@Mathlib.Tactic.RingNF.add_neg] at g_form
      have := dvd_mul_left g f
      nth_rw 1 [g_form, hfg, dvd_iff_isRoot] at this
      set h' : ℤ[X] := X ^ 2 - 2 * (C p + C q) * X + C (p - q) ^ 2 with hh'
      have h'_expand : expand _ 2 h' = h := by
        rw [hh', hh]
        simp [← @npow_mul]
        left
        rw [coe_expand]; simp only [eval₂_ofNat]
      replace this : h'.IsRoot (a^2) := by
        rw [← h'_expand] at this
        rw [IsRoot.def] at this ⊢
        rwa [expand_eval] at this
      have discrim_eq : discrim (1 : ℝ) (-2 * (p + q)) ((p - q) ^ 2) = (4*Real.sqrt (p*q)) * (4*Real.sqrt (p*q)):= by
          unfold discrim
          rw [← pow_two]; ring_nf
          have : 0 ≤ p*q := by nlinarith
          rw [ex2 ((p : ℝ)*q) (by
            rify at this; rwa [])]
      set b := a^2
      replace discrim_eq := quadratic_eq_zero_iff (by norm_num : (1 : ℝ) ≠ 0) discrim_eq b
      simp [← pow_two] at discrim_eq; ring_nf at discrim_eq
      simp [IsRoot.def, h'] at this; rify at this; ring_nf at this
      rw [discrim_eq] at this
      have temp : ¬ Irrational (@Int.cast ℝ _ (b - p -q)) := by simp
      rcases this with this | this
      . replace : (@Int.cast ℝ _ (b - p -q)) = √(↑p * ↑q) * 2 := by
          simp [this]; ring_nf
        contrapose! temp
        rw [this, show (2 : ℝ) = @Rat.cast ℝ _ 2 by rfl]
        apply Irrational.mul_rat ?_ (by norm_num)
        exact ex3 p q hp hq hp₁ hq₁ hpq
      . replace : (@Int.cast ℝ _ (b - p -q)) = -√(↑p * ↑q) * 2 := by
          simp [this]
        contrapose! temp
        rw [this]; simp only [neg_mul, irrational_neg_iff, h']
        rw [show (2 : ℝ) = @Rat.cast ℝ _ 2 by rfl]
        apply Irrational.mul_rat ?_ (by norm_num)
        exact ex3 p q hp hq hp₁ hq₁ hpq
    . right; simp_all

[张守信(Shouxin Zhang)]

Jz Pan said:

张守信(Shouxin Zhang) said:

example (p q : ℤ)
  (hp : 0 < p) (hq : 0 < q)
  (hp₁ : Prime p) (hq₁ : Prime q):
  Irreducible ...

Unfortunately, this result is incorrect for p = q case.

Really. I just didn't remember the IsCoprime api for a while because leansearch crashed. It's sorry >_<

[张守信(Shouxin Zhang)]

And the lemma part:

lemma ex1 (p q : ℤ) (h : Prime p) :
  4*p = q^2 → False := by
  intro hq
  cases' Int.even_or_odd q with hq_even hq_odd
  . obtain ⟨k, rfl⟩ := hq_even
    ring_nf at hq
    simp at hq
    contrapose! h
    refine IsSquare.not_prime ?_
    rw [hq]
    exact IsSquare.sq k
  . obtain ⟨k, rfl⟩ := hq_odd
    ring_nf at hq
    have : 4*(p - k^2 - k) = 1 := by linarith
    have : (4 : ℤ)∣1 := ⟨p - k^2 - k, this.symm⟩
    norm_num at this

lemma ex2 (a : ℝ) (ha : 0 ≤ a): Real.sqrt (a)^2 = a := by
  symm; rw [← Real.sqrt_eq_iff_eq_sq] <;> simp_all

lemma ex3_begin (r : ℚ) (h : ∃ (n : ℤ), r^2 = n) : ∃ (m : ℤ), r = m := by
  let p := r.num
  set q := r.den with hq
  obtain ⟨n, h_eq⟩ := h
  have h_r_eq : r = p / q := by
    simp_rw [p, q, Rat.num_div_den]
  rw [h_r_eq] at h_eq
  simp [div_pow] at h_eq
  have : (r^2).den = 1 := by
    rw [Rat.den_eq_one_iff, h_r_eq]; simp [div_pow, h_eq]
  simp only [Rat.den_pow, Nat.pow_eq_one, OfNat.ofNat_ne_zero, or_false, q, p] at this
  use p; rw [h_r_eq, hq, this, Nat.cast_one, div_one]

lemma ex3 (p q : ℤ)
  (hp_pos : 0 < p) (hq_pos : 0 < q)
  (hp : Prime p) (hq : Prime q) (hpq : IsCoprime p q) : Irrational (Real.sqrt (p * q)) := by
  rw [show (p : ℝ) * q = @Rat.cast ℝ _ (@Int.cast ℚ _ (p * q)) by
    simp only [Int.cast_mul, Rat.cast_mul, Rat.cast_intCast]]
  rw [irrational_sqrt_ratCast_iff (q := (@Int.cast ℚ _ (p * q)))]
  constructor
  . intro h
    obtain ⟨r, hr⟩ := h
    obtain ⟨r, rfl⟩ : ∃ (r' : ℤ), r = ↑r' := by
      rw [← pow_two] at hr
      apply ex3_begin
      use (p * q); simp_all
    rw [← Int.cast_mul, ← Mathlib.Tactic.Qify.intCast_eq] at hr
    rw [← pow_two] at hr
    have p_dvd_r : p ∣ r := by
      apply hp.dvd_of_dvd_pow (n := 2)
      exact Dvd.intro q hr
    have q_dvd_r : q ∣ r := by
      apply hq.dvd_of_dvd_pow (n := 2)
      exact Dvd.intro_left p hr
    have pq_dvd_r : p * q ∣ r := by
      exact IsCoprime.mul_dvd hpq p_dvd_r q_dvd_r
    obtain ⟨k, rfl⟩ := pq_dvd_r
    have : p * q = (p * q * k)^2 := by
      nth_rw 1 [hr]
    have : 1 = p * q * k^2 := by
      have : (p * q) * 1 = (p * q) * (p * q * k^2) := by
        nth_rw 1 [this]; ring_nf
      rw [mul_eq_mul_left_iff] at this
      simp [hp_pos.ne.symm, hq_pos.ne.symm] at this
      exact this
    have hk_ge : 1 ≤ k^2 := by
      rw [Order.one_le_iff_pos, sq_pos_iff]
      contrapose! this; simp [this]
    have pq_gt_one : 1 < p * q := by
      have : 1 < p := by
        rw [ Int.lt_iff_le_and_ne]
        exact ⟨by exact hp_pos, by contrapose! hp; simp [← hp]⟩
      have : 1 < q := by
        rw [ Int.lt_iff_le_and_ne]
        exact ⟨by exact hq_pos, by contrapose! hq; simp [← hq]⟩
      nlinarith
    nlinarith
  . qify at *
    nlinarith

[张守信(Shouxin Zhang)]

Riccardo Brasca said:

Can you write down a very precise mathematical proof that the polynomial is irreducible?

Right. It's incredible that just recently there was an API for Vieta's theorem for quadratic equations in the library, otherwise my code wouldn't even be done.

[Riccardo Brasca]

You can probably suffer a little less doing the following: let $\alpha = \sqrt{p}+\sqrt{q}$ (with your assumptions on $p$ and $q$) and let $K =\mathbb{Q}(\alpha)$. Then:

• $\sqrt{pq}=\frac{(\sqrt{p}+\sqrt{q})^2 - p - q}{2} \in K$ and it has degree 2, so $[K : \mathbb{Q}] \geq 2$.
• $\alpha$ is a root of a polynomial of degree 4, so $[K : \mathbb{Q}] \leq 4$.
• $K$ contains an element (the one above) of degree 2, so $[K : \mathbb{Q}]$ cannot be 3.

The only remaining thing to prove is that the degree of $K$ cannot be 2. Here you have to make your hands dirty (proving that $\alpha$ is not a root a monic polynomial of degree 2.), as you did, but at least the rest seems less painful

[Riccardo Brasca]

Mathematically you can avoid all the suffering working in $L=\mathbb{Q}(\sqrt{p}, \sqrt{q})$ (that at the end is equal to $K$). It would be interesting to try in Lean

[Antoine Chambert-Loir]

For the initial polynomial $T^4-10T^2+1$, one can play with a variant of Eisenstein which involves an irreducible polynomial modulo $3$ instead of $T$. Then the fact is that $T^4-10T^2+1\equiv 12 \pmod {T^2+1}$, and $12$ is not divisible by $9$.

[Antoine Chambert-Loir]

The same trick works for the $p, q$ stuff if $q$ is not a square modulo $p$, but misses the case where $p$ and $q$ are both squares modulo the other one. (In that case, the polynomial is split modulo $p$ and $q$.)