awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1

Tactic:
apply coprime_sq_sub_sq_add_of_even_odd hmncp hm2 hn2

Premises used: _private.0.coprime_sq_sub_sq_add_of_even_odd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
neg : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
apply : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
⊢ h.IsPrimitiveClassified

Tactic:
apply h.isPrimitiveClassified_aux hc hzpos hm2n2 hv2 hw2 _ hmncp

Premises used: PythagoreanTriple.isPrimitiveClassified_aux
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
neg : m % 2 = 1 ∧ n % 2 = 0
⊢ m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0

Tactic:
apply Or.intro_right

Premises used: Or.intro_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ m % 2 = 1 ∧ n % 2 = 0

Tactic:
And.intro hm2 hn2

Premises used: And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ m % 2 = 1 ∧ n % 2 = 0

Tactic:
exact And.intro hm2 hn2

Premises used: And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1

Tactic:
apply coprime_sq_sub_sq_add_of_odd_even hmncp hm2 hn2

Premises used: _private.0.coprime_sq_sub_sq_add_of_odd_even
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
neg : False
⊢ h.IsPrimitiveClassified

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
⊢ 2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1

Tactic:
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
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1
apply :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    HDiv.hDiv (α := ℚ) (↑((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2) : ℚ)
      (↑((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) : ℚ)
apply₁ : 0 < (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2
⊢ y = (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 ∧ z = (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2

Tactic:
apply Rat.div_int_inj hzpos _ (h.coprime_of_coprime hc) h1.2.2.2

Premises used: Rat.div_int_inj, And.right, PythagoreanTriple.coprime_of_coprime
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1
change :
  w =
    HDiv.hDiv (α := ℚ) (↑((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2) : ℚ)
      (↑((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    HDiv.hDiv (α := ℚ) (↑((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2) : ℚ)
      (↑((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) : ℚ)

Tactic:
change w = _
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1
⊢ Ne (α := ℤ) 2 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
hp :
  Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
    (v, w)
q : ℚ :=
  ((circleEquivGen hQ).symm : (a : { p : ℚ × ℚ // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → ℚ)
    (Subtype.mk (p := fun (p : ℚ × ℚ) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (v, w) hp)
ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
m : ℤ := (↑q.den : ℤ)
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
hw2 :
  w =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hv2 :
  v =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1
rw :
  w =
    Rat.divInt ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 * 2)
      ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2 * 2)
⊢ w =
    HDiv.hDiv (α := ℚ) (↑((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2) : ℚ)
      (↑((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) : ℚ)

Tactic:
rw [← Rat.divInt_eq_div, ← Rat.divInt_mul_right (by simp : (2 : ℤ) ≠ 0)]

Premises used: Rat.divInt_eq_div, Rat.divInt_mul_right