awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
⊢ h.IsPrimitiveClassified
have h2 : y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
Tactic: have h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2 := by
    apply Rat.div_int_inj hzpos hm2n2 (h.coprime_of_coprime hc) H
    rw [hw2]
    norm_cast
-- 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
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ 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 : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ (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 apply : 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
Tactic: apply And.intro _ (And.intro co pp)
-- 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
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ 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
have h₁ : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
Tactic: right
-- 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
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
have h₁ : x = 2 * m * n
Tactic: refine ⟨?_, h2.left⟩
-- 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
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ x = 2 * m * n
have h₁ : HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) =
  HDiv.hDiv (α := ℚ) (↑(2 * m * n) : ℚ) (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)
Tactic: rw [← Rat.coe_int_inj _ _, ← div_left_inj' ((mt (Rat.coe_int_inj z 0).mp) hz), hv2, h2.right]
-- 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
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) =
    HDiv.hDiv (α := ℚ) (↑(2 * m * n) : ℚ) (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)
have h₁ : Rat.divInt (2 * m * n) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) =
  Rat.divInt (2 * m * n) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
Tactic: norm_cast
-- 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
⊢ h.IsPrimitiveClassified
have pos : ∀ (h0 : x = 0), h.IsPrimitiveClassified
Tactic: by_cases h0 : x = 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
pos : ∀ (h0 : x = 0), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified
have neg : ∀ (h0 : ¬x = 0), h.IsPrimitiveClassified
Tactic: by_cases h0 : x = 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 : ℚ)
⊢ HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
have simp : HPow.hPow (α := ℚ) (β := ℕ) (↑x : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑y : ℚ) 2 = HPow.hPow (α := ℚ) (β := ℕ) (↑z : ℚ) 2
Tactic: simp [field, v, w]
-- 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 : ℚ)
⊢ HPow.hPow (α := ℚ) (β := ℕ) (↑x : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑y : ℚ) 2 =
    HPow.hPow (α := ℚ) (β := ℕ) (↑z : ℚ) 2
have simp : HMul.hMul (α := ℚ) (↑x : ℚ) (↑x : ℚ) + HMul.hMul (α := ℚ) (↑y : ℚ) (↑y : ℚ) = HMul.hMul (α := ℚ) (↑z : ℚ) (↑z : ℚ)
Tactic: simp only [sq]
-- 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 : ℚ)
⊢ HMul.hMul (α := ℚ) (↑x : ℚ) (↑x : ℚ) + HMul.hMul (α := ℚ) (↑y : ℚ) (↑y : ℚ) = HMul.hMul (α := ℚ) (↑z : ℚ) (↑z : ℚ)
have norm_cast : x * x + y * y = z * z
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 : ℚ)
⊢ h.IsPrimitiveClassified
have hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
Tactic: have hq : v ^ 2 + w ^ 2 = 1 := by
    simp [field, v, w]
    simp only [sq]
    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
⊢ h.IsPrimitiveClassified
have hvz : v ≠ 0
Tactic: have hvz : v ≠ 0 := by simp [field, v, -mul_eq_zero, -div_eq_zero_iff, h0]
-- 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
⊢ w ≠ -1
have contrapose : ∀ (hw1 : w = -1), v = 0
Tactic: contrapose hvz with hw1
Cleared hypotheses: hvz
-- 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
hw1 : w = -1
⊢ v = 0
have hq₁ : HPow.hPow (β := ℕ) v 2 = 0
Tactic: rw [hw1, neg_sq, one_pow, add_eq_right] at hq
Cleared hypotheses: hq, hw1
-- 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
⊢ h.IsPrimitiveClassified
have hw1 : w ≠ -1
Tactic: have hw1 : w ≠ -1 := by
    contrapose hvz with hw1
    rw [hw1, neg_sq, one_pow, add_eq_right] at hq
    exact eq_zero_of_pow_eq_zero hq
-- 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
q : ℚ
⊢ 1 + HPow.hPow (β := ℕ) q 2 ≠ 0
have h₁ : 0 < 1 + HPow.hPow (β := ℕ) q 2
Tactic: apply ne_of_gt
-- 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
⊢ h.IsPrimitiveClassified
have hQ : ∀ (x : ℚ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
Tactic: have hQ : ∀ x : ℚ, 1 + x ^ 2 ≠ 0 := by
    intro q
    apply ne_of_gt
    exact lt_add_of_pos_of_le zero_lt_one (sq_nonneg q)
-- 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
⊢ h.IsPrimitiveClassified
have hp : Membership.mem (γ := Set (ℚ × ℚ)) {p : ℚ × ℚ | HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1}
  (v, w)
Tactic: have hp : (⟨v, w⟩ : ℚ × ℚ) ∈ { p : ℚ × ℚ | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 } := ⟨hq, hw1⟩
-- 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)
⊢ v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
have x₁ : (v, w) = (2 * q / (1 + HPow.hPow (β := ℕ) q 2), (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2))
Tactic: apply Prod.mk.inj
-- 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)
⊢ h.IsPrimitiveClassified
have ht4 : v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)
Tactic: have ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2) := by
    apply Prod.mk.inj
    exact congr_arg Subtype.val ((circleEquivGen hQ).apply_symm_apply ⟨⟨v, w⟩, hp⟩).symm
-- 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
⊢ Ne (α := ℤ) (↑q.den : ℤ) 0
have norm_cast : ¬q.den = 0
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
⊢ h.IsPrimitiveClassified
have hm0 : m ≠ 0
Tactic: have hm0 : m ≠ 0 := by
    -- Added to adapt to https://github.com/leanprover/lean4/pull/2734.
    -- Without `unfold`, `norm_cast` can't see the coercion.
    -- One might try `zeta := true` in `Tactic.NormCast.derive`,
    -- but that seems to break many other things.
    unfold m
    norm_cast
    apply Rat.den_nz q
-- 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
⊢ h.IsPrimitiveClassified
have hq2 : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)
Tactic: have hq2 : q = n / m := (Rat.num_div_den q).symm
-- 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 : ℚ)
⊢ h.IsPrimitiveClassified
have hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
Tactic: have hm2n2 : 0 < m ^ 2 + n ^ 2 := by positivity
-- 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
⊢ h.IsPrimitiveClassified
have hm2n20 : HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2 ≠ 0
Tactic: have hm2n20 : (m ^ 2 + n ^ 2 : ℚ) ≠ 0 := by positivity
-- 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
⊢ (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2) =
    (1 - HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)) 2) /
      (1 + HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)) 2)
have rw : (1 - HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)) 2) /
    (1 + HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)) 2) =
  (1 - HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)) 2) /
    (1 + HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑m : ℚ)) 2)
Tactic: rw [hq2]