awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z ∧ x.gcd y = 1
m n : ℤ
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₁ :
  ∀
    (h :
      PythagoreanTriple (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (2 * m * n) z ∧
        (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1)
    (co : m.gcd n = 1) (pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0),
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
          2 * m * n = 2 * m * n ∨
        HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = 2 * m * n ∧
          2 * m * n = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
      (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)
h₂ :
  ∀
    (h :
      PythagoreanTriple (2 * m * n) (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) z ∧
        (2 * m * n).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),
    (2 * m * n = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
          HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = 2 * m * n ∨
        2 * m * n = 2 * m * n ∧
          HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
      (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)
⊢ (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) ∧
    (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)

Tactic:
rcases H with ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co, pp⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (2 * m * n) z ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
        2 * m * n = 2 * m * n ∨
      HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = 2 * m * n ∧
        2 * m * n = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    (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)

Tactic:
⟨Or.inl ⟨rfl, rfl⟩, ?_, co, pp⟩

Premises used: And.intro, Or.inl, rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (2 * m * n) z ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
h₁ : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
        2 * m * n = 2 * m * n ∨
      HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = 2 * m * n ∧
        2 * m * n = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    (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)

Tactic:
refine ⟨Or.inl ⟨rfl, rfl⟩, ?_, co, pp⟩
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (2 * m * n) z ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
rw :
  (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2

Tactic:
rw [sq, ← h.left.eq]

Premises used: sq, And.left, PythagoreanTriple.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (2 * m * n) z ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (2 * m * n) z ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2

Tactic:
have : z ^ 2 = (m ^ 2 + n ^ 2) ^ 2 := by
        rw [sq, ← h.left.eq]
        ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (2 * m * n) z ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
this : HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)

Tactic:
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this

Premises used: eq_or_eq_neg_of_sq_eq_sq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (2 * m * n) (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) z ∧
    (2 * m * n).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
⊢ (2 * m * n = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
        HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = 2 * m * n ∨
      2 * m * n = 2 * m * n ∧
        HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    (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)

Tactic:
⟨Or.inr ⟨rfl, rfl⟩, ?_, co, pp⟩

Premises used: And.intro, Or.inr, rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (2 * m * n) (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) z ∧
    (2 * m * n).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
h₁ : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ (2 * m * n = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
        HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = 2 * m * n ∨
      2 * m * n = 2 * m * n ∧
        HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    (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)

Tactic:
refine ⟨Or.inr ⟨rfl, rfl⟩, ?_, co, pp⟩
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (2 * m * n) (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) z ∧
    (2 * m * n).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
rw :
  2 * m * n * (2 * m * n) +
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2

Tactic:
rw [sq, ← h.left.eq]

Premises used: sq, And.left, PythagoreanTriple.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (2 * m * n) (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) z ∧
    (2 * m * n).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
⊢ 2 * m * n * (2 * m * n) +
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (2 * m * n) (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) z ∧
    (2 * m * n).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
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2

Tactic:
have : z ^ 2 = (m ^ 2 + n ^ 2) ^ 2 := by
        rw [sq, ← h.left.eq]
        ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z m n : ℤ
h :
  PythagoreanTriple (2 * m * n) (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) z ∧
    (2 * m * n).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
this : HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) 2
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)

Tactic:
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this

Premises used: eq_or_eq_neg_of_sq_eq_sq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
mpr :
  (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
mpr₁ : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
        2 * m * n * (2 * m * n) =
      (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
coprime_sq_sub_mul co pp

Premises used: _private.0.coprime_sq_sub_mul
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
exact coprime_sq_sub_mul co pp

Premises used: _private.0.coprime_sq_sub_mul
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
mpr :
  (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
mpr₁ : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
mpr₂ :
  (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
mpr₃ mpr₄ mpr₅ : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
        2 * m * n * (2 * m * n) =
      (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
first
      | constructor; ring; exact coprime_sq_sub_mul co pp
      | constructor; ring; rw [Int.gcd_comm]; exact coprime_sq_sub_mul co pp

Premises used: _private.0.coprime_sq_sub_mul, Int.gcd_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
mpr :
  (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
mpr₁ : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
        2 * m * n * (2 * m * n) =
      -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
mpr :
  (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
mpr₁ : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
mpr₂ :
  (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
      2 * m * n * (2 * m * n) =
    -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
mpr₃ mpr₄ mpr₅ : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) +
        2 * m * n * (2 * m * n) =
      -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
first
      | constructor; ring; exact coprime_sq_sub_mul co pp
      | constructor; ring; rw [Int.gcd_comm]; exact coprime_sq_sub_mul co pp

Premises used: _private.0.coprime_sq_sub_mul, Int.gcd_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
mpr :
  2 * m * n * (2 * m * n) +
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
    (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
mpr₁ : (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1
⊢ 2 * m * n * (2 * m * n) +
        (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
      (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∧
    (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) +
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
    (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
mpr : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
⊢ (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1

Tactic:
rw [Int.gcd_comm]

Premises used: Int.gcd_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
mpr :
  2 * m * n * (2 * m * n) +
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
    -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
mpr₁ : (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1
⊢ 2 * m * n * (2 * m * n) +
        (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
      -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∧
    (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) +
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
    -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)

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
obtain :
  ∀ (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),
    ∃ (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
⊢ ∃ (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:
obtain ⟨m, n, ht1, ht2, ht3, ht4⟩ :=
    PythagoreanTriple.coprime_classification.mp (And.intro h h_coprime)

Premises used: PythagoreanTriple.coprime_classification, And.intro, Iff.mp
-- 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
inl :
  ∀ (hm : 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
inr :
  ∀ (hm : m < 0),
    ∃ (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
⊢ ∃ (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:
rcases le_or_gt 0 m with hm | hm

Premises used: le_or_gt, OfNat.ofNat
-- 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 : 0 ≤ m
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 : 0 ≤ m
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