awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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) : ℚ)
⊢ y = (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 ∧ z = (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2
have apply₁ : 0 < (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
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ w =
    HDiv.hDiv (α := ℚ) (↑((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2) : ℚ)
      (↑((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) : ℚ)
have rw : 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 [← Rat.divInt_eq_div, ← Rat.divInt_mul_right (by simp : (2 : ℤ) ≠ 0)]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ w =
    Rat.divInt ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 * 2)
      ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2 * 2)
have 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) : ℚ)
Tactic: rw [Int.ediv_mul_cancel h1.1, Int.ediv_mul_cancel h1.2.1, hw2, Rat.divInt_eq_div]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ (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) : ℚ)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ False
have h2 : 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
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
⊢ h.IsPrimitiveClassified
have inl : ∀ (h1 : x % 2 = 0 ∧ y % 2 = 1), h.IsPrimitiveClassified
Tactic: rcases h.even_odd_of_coprime hc with h1 | h2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ h.IsPrimitiveClassified
have inr : ∀ (h2 : x % 2 = 1 ∧ y % 2 = 0), h.IsPrimitiveClassified
Tactic: rcases h.even_odd_of_coprime hc with h1 | h2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified
have hc₁ : y.gcd x = 1
Tactic: rw [Int.gcd_comm] at hc
Cleared hypotheses: hc, hzpos, h2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified
have 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
Tactic: obtain ⟨m, n, H⟩ := h.symm.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h2.left hzpos
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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.IsPrimitiveClassified
have 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)
Tactic: use m, n
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ (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)
have h₁ : x % 2 = 1 →
  y % 2 = 0 →
    m.gcd n = 1 →
      y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
        x = 2 * m * n →
          m % 2 = 0 →
            n % 2 = 1 →
              (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)
Tactic: tauto
Cleared hypotheses: h2, H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 0 →
              n % 2 = 1 →
                (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)
⊢ (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)
have h₂ : x % 2 = 1 →
  y % 2 = 0 →
    m.gcd n = 1 →
      y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
        x = 2 * m * n →
          m % 2 = 1 →
            n % 2 = 0 →
              (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)
Tactic: tauto
Cleared hypotheses: h2, H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 0 →
              n % 2 = 1 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 1 →
              n % 2 = 0 →
                (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)
⊢ (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)
have h₃ : x % 2 = 1 →
  y % 2 = 0 →
    m.gcd n = 1 →
      y = 2 * m * n →
        x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          m % 2 = 0 →
            n % 2 = 1 →
              (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)
Tactic: tauto
Cleared hypotheses: h2, H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 0 →
              n % 2 = 1 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 1 →
              n % 2 = 0 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 →
              n % 2 = 1 →
                (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)
⊢ (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)
have h₄ : x % 2 = 1 →
  y % 2 = 0 →
    m.gcd n = 1 →
      y = 2 * m * n →
        x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          m % 2 = 1 →
            n % 2 = 0 →
              (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)
Tactic: tauto
Cleared hypotheses: h2, H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ h.IsPrimitiveClassified
have pos : ∀ (hz : 0 < z), h.IsPrimitiveClassified
Tactic: by_cases! hz : 0 < z
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
pos : ∀ (hz : 0 < z), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified
have neg : ∀ (hz : z ≤ 0), h.IsPrimitiveClassified
Tactic: by_cases! hz : 0 < z
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
⊢ h.IsPrimitiveClassified
have h' : PythagoreanTriple x y (-z)
Tactic: have h' : PythagoreanTriple x y (-z) := by simpa [PythagoreanTriple, neg_mul_neg] using h.eq
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
h' : PythagoreanTriple x y (-z)
⊢ h.IsPrimitiveClassified
have neg : 0 < -z
Tactic: apply h'.isPrimitiveClassified_of_coprime_of_pos hc
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
h' : PythagoreanTriple x y (-z)
⊢ 0 < -z
have apply : 0 ≤ -z
Tactic: apply lt_of_le_of_ne _ (h'.ne_zero_of_coprime hc).symm
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
⊢ h.IsClassified
have pos : ∀ (h0 : x.gcd y = 0), h.IsClassified
Tactic: by_cases h0 : Int.gcd x y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
pos : ∀ (h0 : x.gcd y = 0), h.IsClassified
⊢ h.IsClassified
have neg : ∀ (h0 : ¬x.gcd y = 0), h.IsClassified
Tactic: by_cases h0 : Int.gcd x y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ h.IsClassified
have hx : x = 0
Tactic: obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ h.IsClassified
have hy : y = 0
Tactic: obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ h.IsClassified
have 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
Tactic: use 0, 1, 0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ h.IsClassified
have neg : sorry.IsPrimitiveClassified
Tactic: apply h.isClassified_of_normalize_isPrimitiveClassified
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ⋯.IsPrimitiveClassified
have neg : (x / (↑(x.gcd y) : ℤ)).gcd (y / (↑(x.gcd y) : ℤ)) = 1
Tactic: apply h.normalize.isPrimitiveClassified_of_coprime