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)
⊢ n.gcd m = 1

Tactic:
have hnmcp : Int.gcd n m = 1 := q.reduced
-- 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 rw : n.gcd m = 1
⊢ m.gcd n = 1

Tactic:
rw [Int.gcd_comm]

Premises used: Int.gcd_comm
-- 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
⊢ n.gcd m = 1

Tactic:
hnmcp
-- 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
⊢ n.gcd m = 1

Tactic:
exact hnmcp
-- 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
⊢ m.gcd n = 1

Tactic:
have hmncp : Int.gcd m n = 1 := by
    rw [Int.gcd_comm]
    exact hnmcp
-- 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
neg : ∀ (hm2 : m % 2 = 0), h.IsPrimitiveClassified
neg₁ : ∀ (hm2 : m % 2 = 1), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified

Tactic:
rcases Int.emod_two_eq_zero_or_one m with hm2 | hm2

Premises used: Int.emod_two_eq_zero_or_one
-- 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
neg : ∀ (hn2 : n % 2 = 0), h.IsPrimitiveClassified
neg₁ : ∀ (hn2 : n % 2 = 1), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified

Tactic:
rcases Int.emod_two_eq_zero_or_one n with hn2 | hn2

Premises used: Int.emod_two_eq_zero_or_one
-- 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
neg : ∀ (hn2 : n % 2 = 0), h.IsPrimitiveClassified
neg₁ : ∀ (hn2 : n % 2 = 1), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified

Tactic:
rcases Int.emod_two_eq_zero_or_one n with hn2 | hn2

Premises used: Int.emod_two_eq_zero_or_one
-- 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 = 0
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 = 0
hn2 : n % 2 = 0
⊢ Dvd.dvd (α := ℤ) 2 (↑(n.gcd m) : ℤ)

Tactic:
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)
-- 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 = 0
h1 : Dvd.dvd (α := ℤ) 2 (↑(n.gcd m) : ℤ)
⊢ False

Tactic:
lia
-- 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
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 = 0
hn2 : n % 2 = 1
neg : m % 2 = 0 ∧ n % 2 = 1
⊢ m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0

Tactic:
apply Or.intro_left

Premises used: Or.intro_left
-- 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
⊢ m % 2 = 0 ∧ n % 2 = 1

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 = 0
hn2 : n % 2 = 1
⊢ m % 2 = 0 ∧ n % 2 = 1

Tactic:
exact And.intro hm2 hn2

Premises used: And.intro