awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
⊢ Ne (α := ℤ) 2 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
⊢ Ne (α := ℤ) 2 0

Tactic:
have h20 : (2 : ℤ) ≠ 0 := by decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
rw :
  (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
      (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
    1
⊢ ((HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2).gcd
      ((HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2) =
    1

Tactic:
rw [h1, h2, Int.mul_ediv_cancel_left _ h20, Int.mul_ediv_cancel_left _ h20]

Premises used: Int.mul_ediv_cancel_left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
by_contra :
  ∀
    (h4 :
      ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
            (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
          1),
    False
⊢ (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
      (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
    1

Tactic:
by_contra h4
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
obtain :
  ∀ (p : ℕ) (hp : Nat.Prime p) (hp1 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).natAbs)
    (hp2 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1).natAbs), False
⊢ False

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

Premises used: Iff.mp, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).natAbs
hp2 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1).natAbs
apply : p ∣ 1
⊢ False

Tactic:
apply hp.not_dvd_one

Premises used: Nat.Prime.not_dvd_one
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).natAbs
hp2 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1).natAbs
rw : p ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
⊢ p ∣ 1

Tactic:
rw [← h]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).natAbs
hp2 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1).natAbs
⊢ (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)

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

Premises used: Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).natAbs
hp2 : p ∣ (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1).natAbs
hp1₁ : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
⊢ (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1

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

Premises used: Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
hp2 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
a : p ∣ (m0 * 2 + 1).natAbs
a₁ : p ∣ (n0 * 2 + 1).natAbs
⊢ p ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)

Tactic:
apply Nat.dvd_gcd

Premises used: Nat.dvd_gcd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
hp2 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
a : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2
⊢ p ∣ (m0 * 2 + 1).natAbs

Tactic:
apply Int.Prime.dvd_natAbs_of_coe_dvd_sq hp

Premises used: Int.Prime.dvd_natAbs_of_coe_dvd_sq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
hp2 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
⊢ (↑p : ℤ) ∣
    2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0) +
      (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)

Tactic:
dvd_add hp1 hp2

Premises used: dvd_add
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
hp2 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
h₁ :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 =
    2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0) +
      (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2

Tactic:
convert! dvd_add hp1 hp2

Premises used: dvd_add
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
hp2 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
⊢ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 =
    2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0) +
      (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
hp2 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
a : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) (n0 * 2 + 1) 2
⊢ p ∣ (n0 * 2 + 1).natAbs

Tactic:
apply Int.Prime.dvd_natAbs_of_coe_dvd_sq hp

Premises used: Int.Prime.dvd_natAbs_of_coe_dvd_sq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
hp2 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
⊢ (↑p : ℤ) ∣
    2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1 -
      2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)

Tactic:
dvd_sub hp2 hp1

Premises used: dvd_sub
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
hp2 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
h₁ :
  HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1 -
      2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) (n0 * 2 + 1) 2

Tactic:
convert! dvd_sub hp2 hp1

Premises used: dvd_sub
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1)
h2 :
  HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))
h3 : (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0
h20 : Ne (α := ℤ) 2 0
h4 :
  ¬(2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)).gcd
        (2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1) =
      1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
hp2 : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
⊢ HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1 -
      2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ z ≠ 0

Tactic:
have hz : z ≠ 0 := ne_of_gt hzpos
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
apply :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) : ℚ)
      (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)
⊢ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2

Tactic:
apply Rat.div_int_inj hzpos hm2n2 (h.coprime_of_coprime hc) H

Premises used: Rat.div_int_inj, PythagoreanTriple.coprime_of_coprime
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
rw :
  (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) =
    HDiv.hDiv (α := ℚ) (↑(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) : ℚ)
      (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) : ℚ)
      (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)

Tactic:
rw [hw2]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
hv2 :
  HDiv.hDiv (α := ℚ) (↑x : ℚ) (↑z : ℚ) =
    HMul.hMul (α := ℚ) 2 (↑m : ℚ) * (↑n : ℚ) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
hw2 :
  HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 - HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2) /
      (HPow.hPow (α := ℚ) (β := ℕ) (↑m : ℚ) 2 + HPow.hPow (α := ℚ) (β := ℕ) (↑n : ℚ) 2)
H : (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Rat.divInt (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) =
    Rat.divInt (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) =
    HDiv.hDiv (α := ℚ) (↑(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) : ℚ)
      (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)

Tactic:
norm_cast