awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2_1 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
inl : ¬-HMod.hMod (α := ℤ) 1 2 % 2 = 0
⊢ ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) % (↑2 : ℤ) = 0

Tactic:
simp only [sq, Nat.cast_ofNat, Int.sub_emod, Int.mul_emod, hm, hn,
        mul_zero, EuclideanDomain.zero_mod, mul_one, zero_sub]

Premises used: Nat.cast_ofNat, EuclideanDomain.zero_mod, sq, MulZeroClass.mul_zero, Int.mul_emod, mul_one, Int.sub_emod, zero_sub
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2_1 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ ¬-HMod.hMod (α := ℤ) 1 2 % 2 = 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
inl : (↑p : ℤ) ∣ n
⊢ False

Tactic:
apply mt (Int.dvd_coe_gcd (Int.natCast_dvd.mpr hpm)) hnp

Premises used: Iff.mpr, Int.dvd_coe_gcd, mt, Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
inl : (↑p : ℤ) ∣ n ∨ (↑p : ℤ) ∣ n
⊢ (↑p : ℤ) ∣ n

Tactic:
apply or_self_iff.mp

Premises used: or_self_iff, Iff.mp
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
inl : (↑p : ℤ) ∣ n * n
⊢ (↑p : ℤ) ∣ n ∨ (↑p : ℤ) ∣ n

Tactic:
apply Int.Prime.dvd_mul' hp

Premises used: Int.Prime.dvd_mul'
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
⊢ n * n = -(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) + m * m

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
inl : (↑p : ℤ) ∣ -(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) + m * m
⊢ (↑p : ℤ) ∣ n * n

Tactic:
rw [(by ring : n * n = -(m ^ 2 - n ^ 2) + m * m)]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
⊢ (↑p : ℤ) ∣ -(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) + m * m

Tactic:
hp1.neg_right.add ((Int.natCast_dvd.2 hpm).mul_right _)

Premises used: Iff.mpr, Dvd.dvd.mul_right, Dvd.dvd.add, Dvd.dvd.neg_right, Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
⊢ (↑p : ℤ) ∣ -(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) + m * m

Tactic:
exact hp1.neg_right.add ((Int.natCast_dvd.2 hpm).mul_right _)

Premises used: Iff.mpr, Dvd.dvd.mul_right, Dvd.dvd.add, Dvd.dvd.neg_right, Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hpn : p ∣ n.natAbs
⊢ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(n.gcd m) : ℤ)

Tactic:
rw [Int.gcd_comm] at hnp

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

Tactic:
rw [Int.gcd_comm] at hnp

Premises used: Int.gcd_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(n.gcd m) : ℤ)
hpn : p ∣ n.natAbs
inr : (↑p : ℤ) ∣ m
⊢ False

Tactic:
apply mt (Int.dvd_coe_gcd (Int.natCast_dvd.mpr hpn)) hnp

Premises used: Iff.mpr, Int.dvd_coe_gcd, mt, Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(n.gcd m) : ℤ)
hpn : p ∣ n.natAbs
inr : (↑p : ℤ) ∣ m ∨ (↑p : ℤ) ∣ m
⊢ (↑p : ℤ) ∣ m

Tactic:
apply or_self_iff.mp

Premises used: or_self_iff, Iff.mp
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(n.gcd m) : ℤ)
hpn : p ∣ n.natAbs
inr : (↑p : ℤ) ∣ m * m
⊢ (↑p : ℤ) ∣ m ∨ (↑p : ℤ) ∣ m

Tactic:
apply Int.Prime.dvd_mul' hp

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

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(n.gcd m) : ℤ)
hpn : p ∣ n.natAbs
inr : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 + n * n
⊢ (↑p : ℤ) ∣ m * m

Tactic:
rw [(by ring : m * m = m ^ 2 - n ^ 2 + n * n)]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(n.gcd m) : ℤ)
hpn : p ∣ n.natAbs
inr : (↑p : ℤ) ∣ n * n
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 + n * n

Tactic:
apply dvd_add hp1

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

Tactic:
(Int.natCast_dvd.mpr hpn).mul_right n

Premises used: Iff.mpr, Dvd.dvd.mul_right, Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(n.gcd m) : ℤ)
hpn : p ∣ n.natAbs
⊢ (↑p : ℤ) ∣ n * n

Tactic:
exact (Int.natCast_dvd.mpr hpn).mul_right n

Premises used: Iff.mpr, Dvd.dvd.mul_right, Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
rw : (-(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)).natAbs.gcd (2 * m * n).natAbs = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
rw [Int.gcd, ← Int.natAbs_neg (m ^ 2 - n ^ 2)]

Premises used: Int.gcd, HSub.hSub, HPow.hPow, OfNat.ofNat, Int.natAbs_neg
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ 2 * m * n = 2 * n * m

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
rw : (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) m 2).natAbs.gcd (2 * n * m).natAbs = 1
⊢ (-(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)).natAbs.gcd (2 * m * n).natAbs = 1

Tactic:
rw [(by ring : 2 * m * n = 2 * n * m), (by ring : -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2)]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
apply : n.gcd m = 1
⊢ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) m 2).natAbs.gcd (2 * n * m).natAbs = 1

Tactic:
apply coprime_sq_sub_mul_of_even_odd _ hn hm

Premises used: _private.0.coprime_sq_sub_mul_of_even_odd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hmn : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
inl : ∀ (h1 : m % 2 = 0 ∧ n % 2 = 1), (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
inr : ∀ (h2 : m % 2 = 1 ∧ n % 2 = 0), (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
rcases hmn with h1 | h2
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
h1 : m % 2 = 0 ∧ n % 2 = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
coprime_sq_sub_mul_of_even_odd h h1.left h1.right

Premises used: And.right, And.left, _private.0.coprime_sq_sub_mul_of_even_odd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
h1 : m % 2 = 0 ∧ n % 2 = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
exact coprime_sq_sub_mul_of_even_odd h h1.left h1.right

Premises used: And.right, And.left, _private.0.coprime_sq_sub_mul_of_even_odd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
h2 : m % 2 = 1 ∧ n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
coprime_sq_sub_mul_of_odd_even h h2.left h2.right

Premises used: _private.0.coprime_sq_sub_mul_of_odd_even, And.right, And.left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
h2 : 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_of_odd_even h h2.left h2.right

Premises used: _private.0.coprime_sq_sub_mul_of_odd_even, And.right, And.left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 1
obtain :
  ∀ (m0 : ℤ) (hm2 : m - 1 = m0 * 2),
    2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
        (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
          ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
              ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
            1
⊢ 2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1

Tactic:
obtain ⟨m0, hm2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hm)

Premises used: Int.dvd_self_sub_of_emod_eq, exists_eq_mul_left_of_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 1
m0 : ℤ
hm2 : m - 1 = m0 * 2
obtain :
  ∀ (n0 : ℤ) (hn2 : n - 1 = n0 * 2),
    2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
        (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
          ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
              ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
            1
⊢ 2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1

Tactic:
obtain ⟨n0, hn2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hn)

Premises used: Int.dvd_self_sub_of_emod_eq, exists_eq_mul_left_of_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 1
m0 : ℤ
hm2 : m - 1 = m0 * 2
n0 : ℤ
hn2 : n - 1 = n0 * 2
rw :
  ∀ (hm2 : m = m0 * 2 + 1) (n0 : ℤ) (hn2 : n = n0 * 2 + 1),
    2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
        (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
          ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
              ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
            1
⊢ 2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1

Tactic:
rw [sub_eq_iff_eq_add] at hm2 hn2

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 1
m0 : ℤ
hm2 : m = m0 * 2 + 1
n0 : ℤ
hn2 : n = n0 * 2 + 1
subst :
  ∀ (h : (m0 * 2 + 1).gcd n = 1) (hm : (m0 * 2 + 1) % 2 = 1),
    2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) n 2 ∧
      2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) n 2 ∧
        (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
          ((HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
              ((HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) n 2) / 2) =
            1
⊢ 2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1

Tactic:
subst m
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
n : ℤ
hn : n % 2 = 1
m0 n0 : ℤ
hn2 : n = n0 * 2 + 1
h : (m0 * 2 + 1).gcd n = 1
hm : (m0 * 2 + 1) % 2 = 1
subst :
  ∀ (hn : (n0 * 2 + 1) % 2 = 1) (h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1),
    2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 ∧
      2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 ∧
        (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0 ∧
          ((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
⊢ 2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) n 2 ∧
    2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) n 2 ∧
      (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) n 2) / 2 % 2 = 0 ∧
        ((HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) n 2) / 2).gcd
            ((HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) n 2) / 2) =
          1

Tactic:
subst n
-- 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
⊢ 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)

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
⊢ 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)

Tactic:
have h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) := by
    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)
⊢ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))

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)
⊢ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 =
    2 * (2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0))

Tactic:
have h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)) := by 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))
H : Ne (α := ℤ) 2 0
⊢ (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0

Tactic:
rw [h2, Int.mul_ediv_cancel_left, Int.mul_emod_right]

Premises used: Int.mul_emod_right, 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))
⊢ 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))
⊢ (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0

Tactic:
have h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0 := by
    rw [h2, Int.mul_ediv_cancel_left, Int.mul_emod_right]
    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
⊢ 2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 ∧
    2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 ∧
      (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0 ∧
        ((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:
⟨⟨_, h1⟩, ⟨_, h2⟩, h3, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
refine :
  ((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
⊢ 2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 + HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 ∧
    2 ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2 ∧
      (HPow.hPow (β := ℕ) (m0 * 2 + 1) 2 - HPow.hPow (β := ℕ) (n0 * 2 + 1) 2) / 2 % 2 = 0 ∧
        ((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:
refine ⟨⟨_, h1⟩, ⟨_, h2⟩, h3, ?_⟩