English
If gcd x y = 1 and y is odd, and z > 0, then h is primitive-classified.
Русский
Если gcd(x,y)=1 и y нечетно, и z>0, то h является примитивно классифицированной.
LaTeX
$$$\gcd x y = 1 \land y \equiv 1 \pmod{2} \land z > 0 \Rightarrow h.IsPrimitiveClassified$$$
Lean4
theorem isPrimitiveClassified_of_coprime_of_odd_of_pos (hc : Int.gcd x y = 1) (hyo : y % 2 = 1) (hzpos : 0 < z) :
h.IsPrimitiveClassified := by
by_cases h0 : x = 0
· exact h.isPrimitiveClassified_of_coprime_of_zero_left hc h0
let v := (x : ℚ) / z
let w := (y : ℚ) / z
have hq : v ^ 2 + w ^ 2 = 1 := by
simp [field, v, w]
simp only [sq]
norm_cast
have hvz : v ≠ 0 := by simp [field, v, -mul_eq_zero, -div_eq_zero_iff, h0]
have hw1 : w ≠ -1 := by
contrapose! hvz with hw1
rw [hw1, neg_sq, one_pow, add_eq_right] at hq
exact pow_eq_zero hq
have hQ : ∀ x : ℚ, 1 + x ^ 2 ≠ 0 := by
intro q
apply ne_of_gt
exact lt_add_of_pos_of_le zero_lt_one (sq_nonneg q)
have hp : (⟨v, w⟩ : ℚ × ℚ) ∈ {p : ℚ × ℚ | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1} := ⟨hq, hw1⟩
let q := (circleEquivGen hQ).symm ⟨⟨v, w⟩, hp⟩
have ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2) :=
by
apply Prod.mk.inj
exact congr_arg Subtype.val ((circleEquivGen hQ).apply_symm_apply ⟨⟨v, w⟩, hp⟩).symm
let m := (q.den : ℤ)
let n := q.num
have hm0 : m ≠ 0 := by
-- Added to adapt to https://github.com/leanprover/lean4/pull/2734.
-- Without `unfold`, `norm_cast` can't see the coercion.
-- One might try `zeta := true` in `Tactic.NormCast.derive`,
-- but that seems to break many other things.
unfold m
norm_cast
apply Rat.den_nz q
have hq2 : q = n / m := (Rat.num_div_den q).symm
have hm2n2 : 0 < m ^ 2 + n ^ 2 := by positivity
have hm2n20 : (m ^ 2 + n ^ 2 : ℚ) ≠ 0 := by positivity
have hx1 {j k : ℚ} (h₁ : k ≠ 0) (h₂ : k ^ 2 + j ^ 2 ≠ 0) :
(1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2) := by field_simp
have hw2 : w = ((m : ℚ) ^ 2 - (n : ℚ) ^ 2) / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2) := by
calc
w = (1 - q ^ 2) / (1 + q ^ 2) := by apply ht4.2
_ = (1 - (↑n / ↑m) ^ 2) / (1 + (↑n / ↑m) ^ 2) := by rw [hq2]
_ = _ := by exact hx1 (Int.cast_ne_zero.mpr hm0) hm2n20
have hx2 {j k : ℚ} (h₁ : k ≠ 0) (h₂ : k ^ 2 + j ^ 2 ≠ 0) :
2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2) :=
have h₃ : k * (k ^ 2 + j ^ 2) ≠ 0 := mul_ne_zero h₁ h₂
by field_simp
have hv2 : v = 2 * m * n / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2) := by
calc
v = 2 * q / (1 + q ^ 2) := by apply ht4.1
_ = 2 * (n / m) / (1 + (↑n / ↑m) ^ 2) := by rw [hq2]
_ = _ := by exact hx2 (Int.cast_ne_zero.mpr hm0) hm2n20
have hnmcp : Int.gcd n m = 1 := q.reduced
have hmncp : Int.gcd m n = 1 := by
rw [Int.gcd_comm]
exact hnmcp
rcases Int.emod_two_eq_zero_or_one m with hm2 | hm2 <;> rcases Int.emod_two_eq_zero_or_one n with hn2 | hn2
· -- m even, n even
exfalso
have h1 : 2 ∣ (Int.gcd n m : ℤ) := Int.dvd_coe_gcd (Int.dvd_of_emod_eq_zero hn2) (Int.dvd_of_emod_eq_zero hm2)
cutsat
· -- m even, n odd
apply h.isPrimitiveClassified_aux hc hzpos hm2n2 hv2 hw2 _ hmncp
· apply Or.intro_left
exact And.intro hm2 hn2
· apply coprime_sq_sub_sq_add_of_even_odd hmncp hm2 hn2
· -- m odd, n even
apply h.isPrimitiveClassified_aux hc hzpos hm2n2 hv2 hw2 _ hmncp
· apply Or.intro_right
exact And.intro hm2 hn2
apply coprime_sq_sub_sq_add_of_odd_even hmncp hm2 hn2
· -- m odd, n odd
exfalso
have h1 :
2 ∣ m ^ 2 + n ^ 2 ∧
2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1 :=
coprime_sq_sub_sq_sum_of_odd_odd hmncp hm2 hn2
have h2 : y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2 :=
by
apply Rat.div_int_inj hzpos _ (h.coprime_of_coprime hc) h1.2.2.2
· change w = _
rw [← Rat.divInt_eq_div, ← Rat.divInt_mul_right (by simp : (2 : ℤ) ≠ 0)]
rw [Int.ediv_mul_cancel h1.1, Int.ediv_mul_cancel h1.2.1, hw2, Rat.divInt_eq_div]
norm_cast
· cutsat
norm_num [h2.1, h1.2.2.1] at hyo
