awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ :
  y = 2 * m * n ∧
    z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
⊢ x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
    y = 2 * m * n ∧
      z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
        m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
apply And.intro h_odd.1

Premises used: And.left, And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ :
  z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
⊢ y = 2 * m * n ∧
    z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
apply And.intro h_odd.2

Premises used: And.right, And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ :
  ∀ (h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2),
    z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
h₂ :
  ∀ (h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)),
    z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
rcases ht2 with h_pos | h_neg
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
apply And.intro h_pos (And.intro ht3 (And.intro ht4 hm))

Premises used: And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
h₁ : False
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
h₁ : ∀ (h_pos : 0 < z), False
⊢ False

Tactic:
revert h_pos
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
h₁ : ∀ (h_pos : 0 < -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)), False
⊢ ∀ (h_pos : 0 < z), False

Tactic:
rw [h_neg]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ 0 ≤ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ ∀ (h_pos : 0 < -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)), False

Tactic:
exact imp_false.mpr (not_lt.mpr (neg_nonpos.mpr (by positivity)))

Premises used: Iff.mpr, imp_false, neg_nonpos, not_lt
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₁ : False
⊢ x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
    y = 2 * m * n ∧
      z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
        m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
⊢ PythagoreanTriple (2 * m * n) y z

Tactic:
rcases h_even with ⟨rfl, -⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₁ : PythagoreanTriple (2 * m * n) y z
⊢ (2 * m * n).gcd y = 1

Tactic:
rcases h_even with ⟨rfl, -⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₁ : PythagoreanTriple (2 * m * n) y z
h_coprime₁ : (2 * m * n).gcd y = 1
⊢ 2 * m * n % 2 = 1

Tactic:
rcases h_even with ⟨rfl, -⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h : PythagoreanTriple (2 * m * n) y z
h_coprime : (2 * m * n).gcd y = 1
h_parity : 2 * m * n % 2 = 1
⊢ Eq (α := ℤ) 0 1

Tactic:
rw [mul_assoc, Int.mul_emod_right] at h_parity

Premises used: mul_assoc, Int.mul_emod_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h : PythagoreanTriple (2 * m * n) y z
h_coprime : (2 * m * n).gcd y = 1
h_parity : Eq (α := ℤ) 0 1
⊢ False

Tactic:
zero_ne_one h_parity

Premises used: zero_ne_one
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h : PythagoreanTriple (2 * m * n) y z
h_coprime : (2 * m * n).gcd y = 1
h_parity : Eq (α := ℤ) 0 1
⊢ False

Tactic:
exact zero_ne_one h_parity

Premises used: zero_ne_one
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht1 :
  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
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h₁ :
  x = HPow.hPow (β := ℕ) (-m) 2 - HPow.hPow (β := ℕ) (-n) 2 ∧
    y = 2 * -m * -n ∧
      z = HPow.hPow (β := ℕ) (-m) 2 + HPow.hPow (β := ℕ) (-n) 2 ∧
        (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ ∃ (m : ℤ) (n : ℤ),
    x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      y = 2 * m * n ∧
        z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
          m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
use -m, -n
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht1 :
  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
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h₁ :
  ∀ (h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n),
    x = HPow.hPow (β := ℕ) (-m) 2 - HPow.hPow (β := ℕ) (-n) 2 ∧
      y = 2 * -m * -n ∧
        z = HPow.hPow (β := ℕ) (-m) 2 + HPow.hPow (β := ℕ) (-n) 2 ∧
          (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
h₂ :
  ∀ (h_even : 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 ∧
        z = HPow.hPow (β := ℕ) (-m) 2 + HPow.hPow (β := ℕ) (-n) 2 ∧
          (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ x = HPow.hPow (β := ℕ) (-m) 2 - HPow.hPow (β := ℕ) (-n) 2 ∧
    y = 2 * -m * -n ∧
      z = HPow.hPow (β := ℕ) (-m) 2 + HPow.hPow (β := ℕ) (-n) 2 ∧
        (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
rcases ht1 with h_odd | h_even
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ :
  x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) (-n) 2 ∧
    y = 2 * -m * -n ∧
      z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) (-n) 2 ∧
        (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ x = HPow.hPow (β := ℕ) (-m) 2 - HPow.hPow (β := ℕ) (-n) 2 ∧
    y = 2 * -m * -n ∧
      z = HPow.hPow (β := ℕ) (-m) 2 + HPow.hPow (β := ℕ) (-n) 2 ∧
        (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
rw [neg_sq m]

Premises used: neg_sq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ :
  x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
    y = 2 * -m * -n ∧
      z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
        (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) (-n) 2 ∧
    y = 2 * -m * -n ∧
      z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) (-n) 2 ∧
        (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
rw [neg_sq n]

Premises used: neg_sq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ :
  y = 2 * -m * -n ∧
    z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
    y = 2 * -m * -n ∧
      z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
        (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
apply And.intro h_odd.1

Premises used: And.left, And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ : y = 2 * -m * -n
h₂ :
  z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ y = 2 * -m * -n ∧
    z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ : 2 * m * n = 2 * -m * -n
⊢ y = 2 * -m * -n

Tactic:
rw [h_odd.2]

Premises used: And.right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
⊢ 2 * m * n = 2 * -m * -n

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ :
  ∀ (h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2),
    z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
h₂ :
  ∀ (h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)),
    z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
rcases ht2 with h_pos | h_neg
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h₁ : (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
apply And.intro h_pos

Premises used: And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h₁ : (-m).gcd (-n) = 1
h₂ : (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h₁ : m.natAbs.gcd n.natAbs = 1
⊢ (-m).natAbs.gcd (-n).natAbs = 1

Tactic:
rw [Int.natAbs_neg, Int.natAbs_neg]

Premises used: Int.natAbs_neg
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ m.natAbs.gcd n.natAbs = 1

Tactic:
ht3

Premises used: Int.gcd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ m.natAbs.gcd n.natAbs = 1

Tactic:
exact ht3
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h₁ : (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ -m
⊢ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
rw [Int.neg_emod_two, Int.neg_emod_two]

Premises used: Int.neg_emod_two
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h₁ : 0 ≤ -m
⊢ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ -m

Tactic:
apply And.intro ht4

Premises used: And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ 0 ≤ -m

Tactic:
lia
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
h₁ : False
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
h₁ : ∀ (h_pos : 0 < z), False
⊢ False

Tactic:
revert h_pos
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
h₁ : ∀ (h_pos : 0 < -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)), False
⊢ ∀ (h_pos : 0 < z), False

Tactic:
rw [h_neg]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ 0 ≤ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ ∀ (h_pos : 0 < -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)), False

Tactic:
exact imp_false.mpr (not_lt.mpr (neg_nonpos.mpr (by positivity)))

Premises used: Iff.mpr, imp_false, neg_nonpos, not_lt