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 = 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 :
  (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) =
    HDiv.hDiv (α := ℚ) (↑(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) : ℚ)
      (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)
⊢ w =
    Rat.divInt ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 * 2)
      ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2 * 2)

Tactic:
rw [Int.ediv_mul_cancel h1.1, Int.ediv_mul_cancel h1.2.1, hw2, Rat.divInt_eq_div]

Premises used: Int.ediv_mul_cancel, Rat.divInt_eq_div, And.right, And.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 = 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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Rat.divInt (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) =
    Rat.divInt (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) =
    HDiv.hDiv (α := ℚ) (↑(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) : ℚ)
      (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)

Tactic:
norm_cast
-- 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
⊢ 0 < (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2

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 = 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
⊢ y = (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 ∧ z = (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2

Tactic:
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
      · 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 = 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
h2 :
  y = (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 ∧ z = (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2
⊢ False

Tactic:
norm_num [h2.1, h1.2.2.1] at hyo

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
inl : ∀ (h1 : x % 2 = 0 ∧ y % 2 = 1), h.IsPrimitiveClassified
inr : ∀ (h2 : x % 2 = 1 ∧ y % 2 = 0), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified

Tactic:
rcases h.even_odd_of_coprime hc with h1 | h2

Premises used: PythagoreanTriple.even_odd_of_coprime
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h1 : x % 2 = 0 ∧ y % 2 = 1
⊢ h.IsPrimitiveClassified

Tactic:
h.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h1.right hzpos

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_pos, And.right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h1 : x % 2 = 0 ∧ y % 2 = 1
⊢ h.IsPrimitiveClassified

Tactic:
exact h.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h1.right hzpos

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_pos, And.right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ y.gcd x = 1

Tactic:
rw [Int.gcd_comm] at hc

Premises used: Int.gcd_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
hc₁ : y.gcd x = 1
⊢ 0 < z

Tactic:
rw [Int.gcd_comm] at hc

Premises used: Int.gcd_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
hc₁ : y.gcd x = 1
hzpos₁ : 0 < z
⊢ x % 2 = 1 ∧ y % 2 = 0

Tactic:
rw [Int.gcd_comm] at hc

Premises used: Int.gcd_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
inr :
  ∀ (m n : ℤ)
    (H :
      (y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ x = 2 * m * n ∨
          y = 2 * m * n ∧ x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)),
    h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified

Tactic:
obtain ⟨m, n, H⟩ := h.symm.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h2.left hzpos

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_pos, And.left, PythagoreanTriple.symm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ x = 2 * m * n ∨
      y = 2 * m * n ∧ x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
h₁ :
  (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
      x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ h.IsPrimitiveClassified

Tactic:
use m, n
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
pos : ∀ (hz : 0 < z), h.IsPrimitiveClassified
neg : ∀ (hz : z ≤ 0), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified

Tactic:
by_cases! hz : 0 < z
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : 0 < z
⊢ h.IsPrimitiveClassified

Tactic:
h.isPrimitiveClassified_of_coprime_of_pos hc hz

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime_of_pos
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : 0 < z
⊢ h.IsPrimitiveClassified

Tactic:
exact h.isPrimitiveClassified_of_coprime_of_pos hc hz

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime_of_pos
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
⊢ PythagoreanTriple x y (-z)

Tactic:
simpa [PythagoreanTriple, neg_mul_neg] using h.eq

Premises used: neg_mul_neg, PythagoreanTriple, PythagoreanTriple.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
⊢ PythagoreanTriple x y (-z)

Tactic:
have h' : PythagoreanTriple x y (-z) := by simpa [PythagoreanTriple, neg_mul_neg] using h.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
h' : PythagoreanTriple x y (-z)
neg : 0 < -z
⊢ h.IsPrimitiveClassified

Tactic:
apply h'.isPrimitiveClassified_of_coprime_of_pos hc

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime_of_pos
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
h' : PythagoreanTriple x y (-z)
apply : 0 ≤ -z
⊢ 0 < -z

Tactic:
apply lt_of_le_of_ne _ (h'.ne_zero_of_coprime hc).symm

Premises used: PythagoreanTriple.ne_zero_of_coprime, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
h' : PythagoreanTriple x y (-z)
⊢ 0 ≤ -z

Tactic:
le_neg.mp hz

Premises used: le_neg, Iff.mp
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
h' : PythagoreanTriple x y (-z)
⊢ 0 ≤ -z

Tactic:
exact le_neg.mp hz

Premises used: le_neg, Iff.mp
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
pos : ∀ (h0 : x.gcd y = 0), h.IsClassified
neg : ∀ (h0 : ¬x.gcd y = 0), h.IsClassified
⊢ h.IsClassified

Tactic:
by_cases h0 : Int.gcd x y = 0

Premises used: Int.gcd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
h₁ :
  (x = 0 * (HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2) ∧ y = 0 * (HMul.hMul (α := ℤ) 2 1 * 0) ∨
      x = 0 * (HMul.hMul (α := ℤ) 2 1 * 0) ∧
        y = 0 * (HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2)) ∧
    Int.gcd 1 0 = 1
⊢ h.IsClassified

Tactic:
use 0, 1, 0
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ (x = 0 * (HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2) ∧ y = 0 * (HMul.hMul (α := ℤ) 2 1 * 0) ∨
      x = 0 * (HMul.hMul (α := ℤ) 2 1 * 0) ∧
        y = 0 * (HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2)) ∧
    Int.gcd 1 0 = 1

Tactic:
simp [hx, hy]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
neg : ⋯.IsPrimitiveClassified
⊢ h.IsClassified

Tactic:
apply h.isClassified_of_normalize_isPrimitiveClassified

Premises used: PythagoreanTriple.isClassified_of_normalize_isPrimitiveClassified
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
neg : (x / (↑(x.gcd y) : ℤ)).gcd (y / (↑(x.gcd y) : ℤ)) = 1
⊢ ⋯.IsPrimitiveClassified

Tactic:
apply h.normalize.isPrimitiveClassified_of_coprime

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime, PythagoreanTriple.normalize
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ (x / (↑(x.gcd y) : ℤ)).gcd (y / (↑(x.gcd y) : ℤ)) = 1

Tactic:
apply Int.gcd_div_gcd_div_gcd (Nat.pos_of_ne_zero h0)

Premises used: Nat.pos_of_ne_zero, Int.gcd_div_gcd_div_gcd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
mp :
  PythagoreanTriple x y z ∧ x.gcd y = 1 →
    ∃ (m : ℤ) (n : ℤ),
      (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
          x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        (z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) ∧
          m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
mpr :
  (∃ (m : ℤ) (n : ℤ),
      (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
          x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        (z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) ∧
          m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)) →
    PythagoreanTriple x y z ∧ x.gcd y = 1
⊢ PythagoreanTriple x y z ∧ x.gcd y = 1 ↔
    ∃ (m : ℤ) (n : ℤ),
      (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
          x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        (z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) ∧
          m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z ∧ x.gcd y = 1
mp :
  ∀ (m n : ℤ)
    (H :
      (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
          x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)),
    ∃ (m : ℤ) (n : ℤ),
      (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
          x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        (z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) ∧
          m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ ∃ (m : ℤ) (n : ℤ),
    (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
        x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
      (z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) ∧
        m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

Tactic:
obtain ⟨m, n, H⟩ := h.left.isPrimitiveClassified_of_coprime h.right

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime, And.right, And.left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z ∧ x.gcd y = 1
m n : ℤ
H :
  (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
      x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
h₁ :
  (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
      x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    (z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) ∧
      m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ ∃ (m : ℤ) (n : ℤ),
    (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
        x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
      (z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) ∧
        m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

Tactic:
use m, n