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
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
⊢ 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
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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₁ :
  (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
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
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
⊢ (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:
apply And.intro _ (And.intro co pp)

Premises used: And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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₁ : x = 2 * m * n ∧ y = 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

Tactic:
right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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

Tactic:
⟨?_, h2.left⟩

Premises used: And.left, And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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₁ : x = 2 * m * n
⊢ x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2

Tactic:
refine ⟨?_, h2.left⟩
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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₁ :
  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) : ℚ)
⊢ x = 2 * m * n

Tactic:
rw [← Rat.coe_int_inj _ _, ← div_left_inj' ((mt (Rat.coe_int_inj z 0).mp) hz), hv2, h2.right]

Premises used: Rat.coe_int_inj, mt, And.right, Iff.mp, div_left_inj', OfNat.ofNat
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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₁ h₂ h₃ 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)
⊢ 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:
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
pos : ∀ (h0 : x = 0), h.IsPrimitiveClassified
neg : ∀ (h0 : ¬x = 0), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified

Tactic:
by_cases h0 : x = 0
-- 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
⊢ h.IsPrimitiveClassified

Tactic:
h.isPrimitiveClassified_of_coprime_of_zero_left hc h0

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime_of_zero_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
⊢ h.IsPrimitiveClassified

Tactic:
exact h.isPrimitiveClassified_of_coprime_of_zero_left hc h0

Premises used: PythagoreanTriple.isPrimitiveClassified_of_coprime_of_zero_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 : ℚ)
simp :
  HPow.hPow (α := ℚ) (β := ℕ) (↑x : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑y : ℚ) 2 =
    HPow.hPow (α := ℚ) (β := ℕ) (↑z : ℚ) 2
⊢ HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1

Tactic:
simp [field, v, w]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
simp :
  HMul.hMul (α := ℚ) (↑x : ℚ) (↑x : ℚ) + HMul.hMul (α := ℚ) (↑y : ℚ) (↑y : ℚ) = HMul.hMul (α := ℚ) (↑z : ℚ) (↑z : ℚ)
⊢ HPow.hPow (α := ℚ) (β := ℕ) (↑x : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑y : ℚ) 2 =
    HPow.hPow (α := ℚ) (β := ℕ) (↑z : ℚ) 2

Tactic:
simp only [sq]

Premises used: sq
-- 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 : ℚ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : x * x + y * y = z * z
⊢ HMul.hMul (α := ℚ) (↑x : ℚ) (↑x : ℚ) + HMul.hMul (α := ℚ) (↑y : ℚ) (↑y : ℚ) = HMul.hMul (α := ℚ) (↑z : ℚ) (↑z : ℚ)

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 : ℚ)
⊢ 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
-- 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
⊢ v ≠ 0

Tactic:
simp [field, v, -mul_eq_zero, -div_eq_zero_iff, h0]

Premises used: mul_eq_zero, div_eq_zero_iff
-- 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
⊢ v ≠ 0

Tactic:
have hvz : v ≠ 0 := by simp [field, v, -mul_eq_zero, -div_eq_zero_iff, h0]
-- 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
contrapose : ∀ (hw1 : w = -1), v = 0
⊢ w ≠ -1

Tactic:
contrapose hvz with hw1
-- 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
hw1 : w = -1
⊢ HPow.hPow (β := ℕ) v 2 = 0

Tactic:
rw [hw1, neg_sq, one_pow, add_eq_right] at hq

Premises used: one_pow, neg_sq, add_eq_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 + HPow.hPow (β := ℕ) w 2 = 1
hw1 : w = -1
hq₁ : HPow.hPow (β := ℕ) v 2 = 0
⊢ w = -1

Tactic:
rw [hw1, neg_sq, one_pow, add_eq_right] at hq

Premises used: one_pow, neg_sq, add_eq_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ)
w : ℚ := HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ)
hq : HPow.hPow (β := ℕ) v 2 = 0
hw1 : w = -1
⊢ v = 0

Tactic:
eq_zero_of_pow_eq_zero hq

Premises used: eq_zero_of_pow_eq_zero
-- 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 = 0
hw1 : w = -1
⊢ v = 0

Tactic:
exact eq_zero_of_pow_eq_zero hq

Premises used: eq_zero_of_pow_eq_zero
-- 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
⊢ 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
-- 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
q : ℚ
h₁ : 0 < 1 + HPow.hPow (β := ℕ) q 2
⊢ 1 + HPow.hPow (β := ℕ) q 2 ≠ 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- 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
q : ℚ
⊢ 0 < 1 + HPow.hPow (β := ℕ) q 2

Tactic:
lt_add_of_pos_of_le zero_lt_one (sq_nonneg q)

Premises used: zero_lt_one, lt_add_of_pos_of_le, sq_nonneg
-- 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
q : ℚ
⊢ 0 < 1 + HPow.hPow (β := ℕ) q 2

Tactic:
exact lt_add_of_pos_of_le zero_lt_one (sq_nonneg q)

Premises used: zero_lt_one, lt_add_of_pos_of_le, sq_nonneg
-- 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
⊢ ∀ (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)
-- 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
⊢ 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⟩
-- 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)
x₁ : (v, w) = (2 * q / (1 + HPow.hPow (β := ℕ) q 2), (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2))
⊢ v = 2 * q / (1 + HPow.hPow (β := ℕ) q 2) ∧ w = (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2)

Tactic:
apply Prod.mk.inj

Premises used: Prod.mk.inj
-- 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)
⊢ (v, w) = (2 * q / (1 + HPow.hPow (β := ℕ) q 2), (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2))

Tactic:
congr_arg Subtype.val ((circleEquivGen hQ).apply_symm_apply ⟨⟨v, w⟩, hp⟩).symm

Premises used: Equiv.apply_symm_apply, circleEquivGen, Prod.mk, Subtype.mk, congr_arg, Eq.symm, Subtype.val
-- 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)
⊢ (v, w) = (2 * q / (1 + HPow.hPow (β := ℕ) q 2), (1 - HPow.hPow (β := ℕ) q 2) / (1 + HPow.hPow (β := ℕ) q 2))

Tactic:
exact congr_arg Subtype.val ((circleEquivGen hQ).apply_symm_apply ⟨⟨v, w⟩, hp⟩).symm

Premises used: Equiv.apply_symm_apply, circleEquivGen, Prod.mk, Subtype.mk, congr_arg, Eq.symm, Subtype.val
-- 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)
⊢ 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
-- 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
unfold : Ne (α := ℤ) (↑q.den : ℤ) 0
⊢ m ≠ 0

Tactic:
unfold m
-- 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
norm_cast : ¬q.den = 0
⊢ Ne (α := ℤ) (↑q.den : ℤ) 0

Tactic:
norm_cast