awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -(↑y.natAbs : ℤ)
h₁ :
  (0 = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2 ∧ y = HMul.hMul (α := ℤ) 2 0 * 1 ∨
      0 = HMul.hMul (α := ℤ) 2 0 * 1 ∧ y = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2) ∧
    Int.gcd 0 1 = 1 ∧
      (HMod.hMod (α := ℤ) 0 2 = 0 ∧ HMod.hMod (α := ℤ) 1 2 = 1 ∨
        HMod.hMod (α := ℤ) 0 2 = 1 ∧ HMod.hMod (α := ℤ) 1 2 = 0)
⊢ h.IsPrimitiveClassified

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

Tactic:
rw [hy, hc, Int.gcd_zero_left]

Premises used: Int.gcd_zero_left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -(↑y.natAbs : ℤ)
⊢ (0 = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2 ∧ -(↑1 : ℤ) = HMul.hMul (α := ℤ) 2 0 * 1 ∨
      0 = HMul.hMul (α := ℤ) 2 0 * 1 ∧ -(↑1 : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2) ∧
    Int.natAbs 1 = 1 ∧
      (HMod.hMod (α := ℤ) 0 2 = 0 ∧ HMod.hMod (α := ℤ) 1 2 = 1 ∨
        HMod.hMod (α := ℤ) 0 2 = 1 ∧ HMod.hMod (α := ℤ) 1 2 = 0)

Tactic:
decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
by_contra : ∀ (H : ¬y.gcd z = 1), False
⊢ y.gcd z = 1

Tactic:
by_contra H
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
obtain : ∀ (p : ℕ) (hp : Nat.Prime p) (hpy : p ∣ y.natAbs) (hpz : p ∣ z.natAbs), False
⊢ False

Tactic:
obtain ⟨p, hp, hpy, hpz⟩ := Nat.Prime.not_coprime_iff_dvd.mp H

Premises used: Iff.mp, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
apply : p ∣ 1
⊢ False

Tactic:
apply hp.not_dvd_one

Premises used: Nat.Prime.not_dvd_one
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
rw : p ∣ x.gcd y
⊢ p ∣ 1

Tactic:
rw [← hc]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
apply : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) x 2
⊢ p ∣ x.gcd y

Tactic:
apply Nat.dvd_gcd (Int.Prime.dvd_natAbs_of_coe_dvd_sq hp _ _) hpy

Premises used: Int.Prime.dvd_natAbs_of_coe_dvd_sq, Nat.dvd_gcd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
rw : (↑p : ℤ) ∣ z * z - y * y
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) x 2

Tactic:
rw [sq, eq_sub_of_add_eq h]

Premises used: eq_sub_of_add_eq, sq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ (↑p : ℤ) ∣ y

Tactic:
rw [← Int.natCast_dvd] at hpy hpz

Premises used: Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
hpy₁ : (↑p : ℤ) ∣ y
⊢ (↑p : ℤ) ∣ z

Tactic:
rw [← Int.natCast_dvd] at hpy hpz

Premises used: Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : (↑p : ℤ) ∣ y
hpz : (↑p : ℤ) ∣ z
⊢ (↑p : ℤ) ∣ z * z - y * y

Tactic:
dvd_sub (hpz.mul_right _) (hpy.mul_right _)

Premises used: Dvd.dvd.mul_right, dvd_sub
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : (↑p : ℤ) ∣ y
hpz : (↑p : ℤ) ∣ z
⊢ (↑p : ℤ) ∣ z * z - y * y

Tactic:
exact dvd_sub (hpz.mul_right _) (hpy.mul_right _)

Premises used: Dvd.dvd.mul_right, dvd_sub
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
⊢ HPow.hPow (β := ℕ)
        (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)).1 2 +
      HPow.hPow (β := ℕ)
        (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)).2 2 =
    1

Tactic:
field [hk x]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
simp : ¬Eq.{u_1 + 1} (α := K) 1 (-1)
⊢ (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)).2 ≠ -1

Tactic:
simp only [Ne, div_eq_iff (hk x), neg_mul, one_mul, neg_add, sub_eq_add_neg, add_left_inj]

Premises used: sub_eq_add_neg, neg_add, Ne, add_left_inj, div_eq_iff, neg_mul, one_mul
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
⊢ ¬Eq.{u_1 + 1} (α := K) 1 (-1)

Tactic:
simpa only [eq_neg_iff_add_eq_zero, one_pow] using hk 1

Premises used: one_pow, eq_neg_iff_add_eq_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
⊢ HAdd.hAdd (α := K) 1 1 = 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
⊢ HAdd.hAdd (α := K) 1 1 = 2

Tactic:
have h2 : (1 + 1 : K) = 2 := by norm_num
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
h2 : HAdd.hAdd (α := K) 1 1 = 2
⊢ 1 + HPow.hPow (α := K) (β := ℕ) 1 2 ≠ 0

Tactic:
hk 1

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
h2 : HAdd.hAdd (α := K) 1 1 = 2
h : 2 = 1 + HPow.hPow (α := K) (β := ℕ) 1 2
⊢ Ne.{u_1 + 1} (α := K) 2 0

Tactic:
convert! hk 1

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
h2 : HAdd.hAdd (α := K) 1 1 = 2
h : 2 = HAdd.hAdd (α := K) 1 1
h₁ h₂ : Eq.{u_1 + 1} (α := K) 2 2
⊢ 2 = 1 + HPow.hPow (α := K) (β := ℕ) 1 2

Tactic:
rw [one_pow 2, h2]

Premises used: one_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
h2 : HAdd.hAdd (α := K) 1 1 = 2
⊢ Ne.{u_1 + 1} (α := K) 2 0

Tactic:
have h3 : (2 : K) ≠ 0 := by
      convert! hk 1
      rw [one_pow 2, h2]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
h2 : HAdd.hAdd (α := K) 1 1 = 2
h3 : Ne.{u_1 + 1} (α := K) 2 0
⊢ (fun (p : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }) ↦
        (↑p : K × K).1 / ((↑p : K × K).2 + 1))
      ((fun (x : K) ↦
          (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1)
              (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)) ⋯ :
            { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }))
        x) =
    x

Tactic:
simp [field, hk x, h2, add_assoc, add_comm, add_sub_cancel, mul_comm]

Premises used: add_assoc, add_comm, add_sub_cancel, mul_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hxy : HPow.hPow (β := ℕ) (x, y).1 2 + HPow.hPow (β := ℕ) (x, y).2 2 = 1
hy : (x, y).2 ≠ -1
change :
  ∀ (hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1),
    Eq (α := { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 })
      ((fun (x : K) ↦
          (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1)
              (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)) ⋯ :
            { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }))
        ((fun (p : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }) ↦
            (↑p : K × K).1 / ((↑p : K × K).2 + 1))
          (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (x, y)
            ⋯)))
      (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (x, y) ⋯)
⊢ Eq (α := { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 })
    ((fun (x : K) ↦
        (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1)
            (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)) ⋯ :
          { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }))
      ((fun (p : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }) ↦
          (↑p : K × K).1 / ((↑p : K × K).2 + 1))
        (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (x, y)
          ⋯)))
    (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (x, y) ⋯)

Tactic:
change x ^ 2 + y ^ 2 = 1 at hxy
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
⊢ y + 1 ≠ 0

Tactic:
have h2 : y + 1 ≠ 0 := mt eq_neg_of_add_eq_zero_left hy
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
rw : HPow.hPow (β := ℕ) (y + 1) 2 + (1 + -HPow.hPow (β := ℕ) y 2) = 2 * (y + 1)
⊢ HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)

Tactic:
rw [(add_neg_eq_iff_eq_add.mpr hxy.symm).symm]

Premises used: Iff.mpr, Eq.symm, add_neg_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
⊢ HPow.hPow (β := ℕ) (y + 1) 2 + (1 + -HPow.hPow (β := ℕ) y 2) = 2 * (y + 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
⊢ HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)

Tactic:
have h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1) := by
      rw [(add_neg_eq_iff_eq_add.mpr hxy.symm).symm]
      ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
⊢ 1 + HPow.hPow (α := K) (β := ℕ) 1 2 ≠ 0

Tactic:
hk 1

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
h : 2 = 1 + HPow.hPow (α := K) (β := ℕ) 1 2
⊢ Ne.{u_1 + 1} (α := K) 2 0

Tactic:
convert! hk 1

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
h : 2 = HAdd.hAdd (α := K) 1 1
⊢ 2 = 1 + HPow.hPow (α := K) (β := ℕ) 1 2

Tactic:
rw [one_pow 2]

Premises used: one_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
⊢ 2 = HAdd.hAdd (α := K) 1 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
⊢ Ne.{u_1 + 1} (α := K) 2 0

Tactic:
have h4 : (2 : K) ≠ 0 := by
      convert! hk 1
      rw [one_pow 2]
      ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
h4 : Ne.{u_1 + 1} (α := K) 2 0
simp :
  2 * (x / (y + 1)) / (1 + HPow.hPow (β := ℕ) (x / (y + 1)) 2) = x ∧
    (1 - HPow.hPow (β := ℕ) (x / (y + 1)) 2) / (1 + HPow.hPow (β := ℕ) (x / (y + 1)) 2) = y
⊢ Eq (α := { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 })
    ((fun (x : K) ↦
        (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1)
            (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)) ⋯ :
          { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }))
      ((fun (p : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }) ↦
          (↑p : K × K).1 / ((↑p : K × K).2 + 1))
        (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (x, y)
          ⋯)))
    (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1) (x, y) ⋯)

Tactic:
simp only [Prod.mk_inj, Subtype.mk_eq_mk]

Premises used: Prod.mk_inj, Subtype.mk_eq_mk
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
h4 : Ne.{u_1 + 1} (α := K) 2 0
left : 2 * (x / (y + 1)) / (1 + HPow.hPow (β := ℕ) (x / (y + 1)) 2) = x
right : (1 - HPow.hPow (β := ℕ) (x / (y + 1)) 2) / (1 + HPow.hPow (β := ℕ) (x / (y + 1)) 2) = y
⊢ 2 * (x / (y + 1)) / (1 + HPow.hPow (β := ℕ) (x / (y + 1)) 2) = x ∧
    (1 - HPow.hPow (β := ℕ) (x / (y + 1)) 2) / (1 + HPow.hPow (β := ℕ) (x / (y + 1)) 2) = y

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
h4 : Ne.{u_1 + 1} (α := K) 2 0
⊢ 2 * (x / (y + 1)) / (1 + HPow.hPow (β := ℕ) (x / (y + 1)) 2) = x

Tactic:
simp [field, h3]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
h4 : Ne.{u_1 + 1} (α := K) 2 0
right : HPow.hPow (β := ℕ) (y + 1) 2 - HPow.hPow (β := ℕ) x 2 = y * (y + 1) * 2
⊢ (1 - HPow.hPow (β := ℕ) (x / (y + 1)) 2) / (1 + HPow.hPow (β := ℕ) (x / (y + 1)) 2) = y

Tactic:
simp [field, h3]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
h4 : Ne.{u_1 + 1} (α := K) 2 0
right : HPow.hPow (β := ℕ) (y + 1) 2 - (1 + -HPow.hPow (β := ℕ) y 2) = y * (y + 1) * 2
⊢ HPow.hPow (β := ℕ) (y + 1) 2 - HPow.hPow (β := ℕ) x 2 = y * (y + 1) * 2

Tactic:
rw [← add_neg_eq_iff_eq_add.mpr hxy.symm]

Premises used: Iff.mpr, Eq.symm, add_neg_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x_1 : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = 1
h2 : y + 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (y + 1) 2 + HPow.hPow (β := ℕ) x 2 = 2 * (y + 1)
h4 : Ne.{u_1 + 1} (α := K) 2 0
⊢ HPow.hPow (β := ℕ) (y + 1) 2 - (1 + -HPow.hPow (β := ℕ) y 2) = y * (y + 1) * 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
⊢ (↑((circleEquivGen hk : (a : K) → { p : K × K // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) x) : K × K) =
    (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
v : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }
⊢ ((circleEquivGen hk).symm : (a : { p : K × K // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }) → K) v =
    (↑v : K × K).1 / ((↑v : K × K).2 + 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
by_contra :
  ∀ (H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1),
    False
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1

Tactic:
by_contra H
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
obtain :
  ∀ (p : ℕ) (hp : Nat.Prime p) (hp1 : p ∣ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).natAbs)
    (hp2 : p ∣ (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2).natAbs), False
⊢ False

Tactic:
obtain ⟨p, hp, hp1, hp2⟩ := Nat.Prime.not_coprime_iff_dvd.mp H

Premises used: Iff.mp, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).natAbs
hp2 : p ∣ (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2).natAbs
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2

Tactic:
rw [← Int.natCast_dvd] at hp1 hp2

Premises used: Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).natAbs
hp2 : p ∣ (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2).natAbs
hp1₁ : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2

Tactic:
rw [← Int.natCast_dvd] at hp1 hp2

Premises used: Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 + (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)

Tactic:
dvd_add hp2 hp1

Premises used: dvd_add
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h₁ :
  2 * HPow.hPow (β := ℕ) m 2 =
    HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 + (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)
⊢ (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2

Tactic:
convert! dvd_add hp2 hp1 using 1

Premises used: dvd_add
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ 2 * HPow.hPow (β := ℕ) m 2 =
    HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 + (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)

Tactic:
ring