awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
⊢ PythagoreanTriple x y z ∧ x.gcd y = 1 ↔
    ∃ (m : ℤ) (n : ℤ),
      (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)
have mp : PythagoreanTriple x y z ∧ x.gcd y = 1 →
  ∃ (m : ℤ) (n : ℤ),
    (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: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
mp :
  PythagoreanTriple x y z ∧ x.gcd y = 1 →
    ∃ (m : ℤ) (n : ℤ),
      (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)
⊢ PythagoreanTriple x y z ∧ x.gcd y = 1 ↔
    ∃ (m : ℤ) (n : ℤ),
      (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)
have mpr : (∃ (m : ℤ) (n : ℤ),
    (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)) →
  PythagoreanTriple x y z ∧ x.gcd y = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z ∧ x.gcd y = 1
⊢ ∃ (m : ℤ) (n : ℤ),
    (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)
have mp : ∀ (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)),
  ∃ (m : ℤ) (n : ℤ),
    (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: obtain ⟨m, n, H⟩ := h.left.isPrimitiveClassified_of_coprime h.right
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ ∃ (m : ℤ) (n : ℤ),
    (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)
have h₁ : (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
    x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
  (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: use m, n
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ (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)
have 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)
Tactic: rcases H with ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co, pp⟩
Cleared hypotheses: x, y, h, H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ (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)
have 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)
Tactic: rcases H with ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co, pp⟩
Cleared hypotheses: x, y, h, H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
have h₁ : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
Tactic: refine ⟨Or.inl ⟨rfl, rfl⟩, ?_, co, pp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
have 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
Tactic: rw [sq, ← h.left.eq]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
have h₁ : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
Tactic: refine ⟨Or.inr ⟨rfl, rfl⟩, ?_, co, pp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
have 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
Tactic: rw [sq, ← h.left.eq]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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) ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ (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
have mpr₁ : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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) ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
have 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)
Tactic: first
      | constructor; ring; exact coprime_sq_sub_mul co pp
      | constructor; ring; rw [Int.gcd_comm]; exact coprime_sq_sub_mul co pp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ (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
have mpr₁ : (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
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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) ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ (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
have mpr₁ : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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) ∧
    (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
have 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)
Tactic: first
      | constructor; ring; exact coprime_sq_sub_mul co pp
      | constructor; ring; rw [Int.gcd_comm]; exact coprime_sq_sub_mul co pp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ (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
have mpr₁ : (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
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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) ∧
    (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ 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
have mpr₁ : (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1
have mpr : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
Tactic: rw [Int.gcd_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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) ∧
    (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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)
⊢ 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
have mpr₁ : (2 * m * n).gcd (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ),
    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
have 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
Tactic: obtain ⟨m, n, ht1, ht2, ht3, ht4⟩ :=
    PythagoreanTriple.coprime_classification.mp (And.intro h h_coprime)