Gaussian int

Stream: new members

[vxctyxeha]

hello i try to solve Determine all the representations of the integer 2130797=172⋅73⋅101  as a sum of two squares. and
i prove that  2130797=(4+i)2(4−i)2(8+3i)(8−3i)(10+i)(10−i) ，How should I express my current problem using lean to obtain all the numbers by combining these (4+i)²(4−i)²(8+3i)(8−3i)(10+i)(10−i)? Which tactic should I use?

import Mathlib
open Complex


  theorem my_favorite_theorem : (2130797 : ℂ) = (4 + I)^2 * (4 - I)^2 * (8 + 3*I) * (8 - 3*I) * (10 + I) * (10 - I) := by
  field_simp [pow_two, Complex.ext_iff, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im, Complex.I_re, Complex.I_im]
  norm_num

[vxctyxeha]

image.png

[Aaron Liu]

Well you need to state it first

import Mathlib

def solutions : Finset (Int × Int) where
  val := ({(851, 1186), (994, 1069), (334, 1421), (46, 1459), (646, 1309), (374, 1411)} : Multiset (Int × Int)).bind
      fun p => (({(1, 1), (1, -1), (-1, 1), (-1, -1)} : Multiset (Int × Int)).bind fun u => {u * p, u * p.swap})
  nodup := by decide

example (a b : Int) : a ^ 2 + b ^ 2 = 2130797 ↔ (a, b) ∈ solutions := by
  refine ⟨fun h => ?_, by revert a b; rw [← Prod.forall']; decide⟩
  -- good luck
  sorry

[vxctyxeha]

import Mathlib
/--找到所有满足x^2 + y^2 = 2130797的x和y-/
theorem  my_favorite_theorem1 : {(x, y) : ℤ × ℤ | x^2 + y^2 = 2130797}
  =
  (
    {(46, 1459), (46, -1459), (-46, 1459), (-46, -1459),
     (1459, 46), (1459, -46), (-1459, 46), (-1459, -46),
     (334, 1421), (334, -1421), (-334, 1421), (-334, -1421),
     (1421, 334), (1421, -334), (-1421, 334), (-1421, -334),
     (374, 1411), (374, -1411), (-374, 1411), (-374, -1411),
     (1411, 374), (1411, -374), (-1411, 374), (-1411, -374),
     (646, 1309), (646, -1309), (-646, 1309), (-646, -1309),
     (1309, 646), (1309, -646), (-1309, 646), (-1309, -646),
     (851, 1186), (851, -1186), (-851, 1186), (-851, -1186),
     (1186, 851), (1186, -851), (-1186, 851), (-1186, -851),
     (994, 1069), (994, -1069), (-994, 1069), (-994, -1069),
     (1069, 994), (1069, -994), (-1069, 994), (-1069, -994)} : Finset (ℤ × ℤ)
  ) := by

--我们把他的范围扩大到1460也就是比起根号2130797大-
have h1 : {(x, y) : ℤ × ℤ | x^2 + y^2 = 2130797} = Finset.filter (fun s : ℤ × ℤ => (s.1)^2 + (s.2)^2 = 2130797) (Finset.Icc (-1460 : ℤ) 1460 ×ˢ Finset.Icc (-1460 : ℤ) 1460) := by
    ext ⟨x, y⟩
    simp
    intro h
    have h2 : x ≤ 1460 := by nlinarith
    have h3 : x ≥ -1460 := by nlinarith
    have h4 : y ≤ 1460 := by nlinarith
    have h5 : y ≥ -1460 := by nlinarith
    tauto
--我们找到其所有在-1460到正1460的解
have all_48_integer_solutions_are_these_inlined :
  (
    Finset.filter (fun p : ℤ × ℤ ↦ p.1^2 + p.2^2 = (2130797 : ℤ))
      (Finset.Icc (-1460) 1460 ×ˢ Finset.Icc (-1460) 1460)
  )
  =
  ( --总共48对
    {(46, 1459), (46, -1459), (-46, 1459), (-46, -1459),
     (1459, 46), (1459, -46), (-1459, 46), (-1459, -46),
     (334, 1421), (334, -1421), (-334, 1421), (-334, -1421),
     (1421, 334), (1421, -334), (-1421, 334), (-1421, -334),
     (374, 1411), (374, -1411), (-374, 1411), (-374, -1411),
     (1411, 374), (1411, -374), (-1411, 374), (-1411, -374),
     (646, 1309), (646, -1309), (-646, 1309), (-646, -1309),
     (1309, 646), (1309, -646), (-1309, 646), (-1309, -646),
     (851, 1186), (851, -1186), (-851, 1186), (-851, -1186),
     (1186, 851), (1186, -851), (-1186, 851), (-1186, -851),
     (994, 1069), (994, -1069), (-994, 1069), (-994, -1069),
     (1069, 994), (1069, -994), (-1069, 994), (-1069, -994)} : Finset (ℤ × ℤ)
  ) := by


  native_decide
rw [h1]
rw [← all_48_integer_solutions_are_these_inlined]