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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2

Tactic:
have h2m : (p : ℤ) ∣ 2 * m ^ 2 := by
    convert! dvd_add hp2 hp1 using 1
    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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 - (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)

Tactic:
dvd_sub hp2 hp1

Premises used: dvd_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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h₁ :
  2 * HPow.hPow (β := ℕ) n 2 =
    HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 - (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)
⊢ (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2

Tactic:
convert! dvd_sub hp2 hp1 using 1

Premises used: dvd_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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
⊢ 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 : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
⊢ (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2

Tactic:
have h2n : (p : ℤ) ∣ 2 * n ^ 2 := by
    convert! dvd_sub hp2 hp1 using 1
    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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
have hmc : p = 2 ∨ p ∣ Int.natAbs m := prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2m
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
⊢ p = 2 ∨ p ∣ n.natAbs

Tactic:
have hnc : p = 2 ∨ p ∣ Int.natAbs n := prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2n
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
pos : ∀ (h2 : p = 2), False
neg : ∀ (h2 : ¬p = 2), False
⊢ False

Tactic:
by_cases h2 : p = 2
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
simp :
  (HMod.hMod (α := ℤ) 0 2 % 2 * (HMod.hMod (α := ℤ) 0 2 % 2) % 2 % 2 +
        HMod.hMod (α := ℤ) 1 2 % 2 * (HMod.hMod (α := ℤ) 1 2 % 2) % 2 % 2) %
      2 =
    1
⊢ (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 1

Tactic:
simp only [sq, Int.add_emod, Int.mul_emod, hm, hn, dvd_refl, Int.emod_emod_of_dvd]

Premises used: sq, Int.emod_emod_of_dvd, Int.mul_emod, Int.add_emod, dvd_refl
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
⊢ (HMod.hMod (α := ℤ) 0 2 % 2 * (HMod.hMod (α := ℤ) 0 2 % 2) % 2 % 2 +
        HMod.hMod (α := ℤ) 1 2 % 2 * (HMod.hMod (α := ℤ) 1 2 % 2) % 2 % 2) %
      2 =
    1

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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
⊢ (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 1

Tactic:
have h3 : (m ^ 2 + n ^ 2) % 2 = 1 := by
      simp only [sq, Int.add_emod, Int.mul_emod, hm, hn, dvd_refl, Int.emod_emod_of_dvd]
      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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
h3 : (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 1
a : 2 ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 0

Tactic:
apply Int.emod_eq_zero_of_dvd

Premises used: Int.emod_eq_zero_of_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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
h3 : (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 1
a a₁ a₂ a₃ :
  ∀ (hp2 : (↑2 : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) (h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2)
    (h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2) (hmc : p = 2 ∨ p ∣ m.natAbs) (hnc : p = 2 ∨ p ∣ n.natAbs) (h2 : p = 2)
    (h3 : (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

Tactic:
rwa [h2] at hp2
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
h3 : (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 1
⊢ (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 0

Tactic:
have h4 : (m ^ 2 + n ^ 2) % 2 = 0 := by
      apply Int.emod_eq_zero_of_dvd
      rwa [h2] at hp2
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
h3 : (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 1
h4 : (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 0
⊢ Eq (α := ℤ) 0 1

Tactic:
rw [h4] at h3
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
h3 : (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 1
h4 : (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 0
h3₁ : Eq (α := ℤ) 0 1
⊢ (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 0

Tactic:
rw [h4] at h3
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
h3 : Eq (α := ℤ) 0 1
h4 : (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 0
⊢ False

Tactic:
zero_ne_one h3

Premises used: zero_ne_one
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
h3 : Eq (α := ℤ) 0 1
h4 : (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) % 2 = 0
⊢ False

Tactic:
exact zero_ne_one h3

Premises used: zero_ne_one
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : ¬p = 2
neg : p ∣ 1
⊢ False

Tactic:
apply hp.not_dvd_one

Premises used: Nat.Prime.not_dvd_one
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : ¬p = 2
neg : p ∣ m.gcd n
⊢ p ∣ 1

Tactic:
rw [← h]
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : ¬p = 2
⊢ p ∣ m.gcd n

Tactic:
Nat.dvd_gcd (Or.resolve_left hmc h2) (Or.resolve_left hnc h2)

Premises used: Int.gcd, Or.resolve_left, Nat.dvd_gcd
-- 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 (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
hp2 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h2m : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
h2n : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) n 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : ¬p = 2
⊢ p ∣ m.gcd n

Tactic:
exact Nat.dvd_gcd (Or.resolve_left hmc h2) (Or.resolve_left hnc h2)

Premises used: Or.resolve_left, Nat.dvd_gcd
-- 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
      (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2).natAbs =
    1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 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
⊢ -(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) m 2

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
      (HPow.hPow (β := ℕ) n 2 + HPow.hPow (β := ℕ) m 2).natAbs =
    1
⊢ (-(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)).natAbs.gcd
      (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2).natAbs =
    1

Tactic:
rw [(by ring : -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2), add_comm]

Premises used: add_comm
-- 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
      (HPow.hPow (β := ℕ) n 2 + HPow.hPow (β := ℕ) m 2).natAbs =
    1

Tactic:
apply coprime_sq_sub_sq_add_of_even_odd _ hn hm

Premises used: _private.0.coprime_sq_sub_sq_add_of_even_odd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
rwa rwa₁ rwa₂ rwa₃ : m.gcd n = 1
⊢ n.gcd m = 1

Tactic:
rwa [Int.gcd_comm]

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
by_contra : ∀ (H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1), False
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1

Tactic:
by_contra H
-- 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
obtain :
  ∀ (p : ℕ) (hp : Nat.Prime p) (hp1 : p ∣ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).natAbs)
    (hp2 : p ∣ (2 * m * n).natAbs), False
⊢ False

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

Premises used: Iff.mp, Nat.Prime.not_coprime_iff_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).natAbs
hp2 : p ∣ (2 * m * n).natAbs
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2

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

Premises used: 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).natAbs
hp2 : p ∣ (2 * m * n).natAbs
hp1₁ : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
⊢ (↑p : ℤ) ∣ 2 * m * n

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

Premises used: 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
rw : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑1 : ℤ)
⊢ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)

Tactic:
rw [h]
-- 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
norm_cast : ¬p ∣ 1
⊢ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑1 : ℤ)

Tactic:
norm_cast
-- 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
⊢ ¬p ∣ 1

Tactic:
mt Nat.dvd_one.mp (Nat.Prime.ne_one hp)

Premises used: Nat.dvd_one, mt, Nat.Prime.ne_one, 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
⊢ ¬p ∣ 1

Tactic:
exact mt Nat.dvd_one.mp (Nat.Prime.ne_one hp)

Premises used: Nat.dvd_one, mt, Nat.Prime.ne_one, 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
⊢ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)

Tactic:
have hnp : ¬(p : ℤ) ∣ Int.gcd m n := by
    rw [h]
    norm_cast
    exact mt Nat.dvd_one.mp (Nat.Prime.ne_one hp)
-- 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) : ℤ)
inl : ∀ (hp2m : p ∣ (2 * m).natAbs), False
inr : ∀ (hpn : p ∣ n.natAbs), False
⊢ False

Tactic:
rcases Int.Prime.dvd_mul hp hp2 with hp2m | hpn

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 ∣ (2 * m).natAbs
⊢ p ∣ Int.natAbs 2 * m.natAbs

Tactic:
rw [Int.natAbs_mul] at hp2m

Premises used: Int.natAbs_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
inl : ∀ (hp2 : p ∣ Int.natAbs 2), False
inl₁ : ∀ (hpm : p ∣ m.natAbs), False
⊢ False

Tactic:
rcases (Nat.Prime.dvd_mul hp).mp hp2m with hp2 | hpm

Premises used: Iff.mp, Nat.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_1 : (↑p : ℤ) ∣ 2 * m * n
hnp : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(m.gcd n) : ℤ)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hp2 : p ∣ Int.natAbs 2
⊢ p = 2

Tactic:
have hp2' : p = 2 := (Nat.le_of_dvd zero_lt_two hp2).antisymm hp.two_le
-- 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_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 : ∀ (hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2), False
⊢ False

Tactic:
revert hp1
-- 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 : ∀ (hp1 : (↑2 : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2), False
⊢ ∀ (hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2), False

Tactic:
rw [hp2']
-- 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 : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) % (↑2 : ℤ) = 0
⊢ ∀ (hp1 : (↑2 : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2), False

Tactic:
apply mt Int.emod_eq_zero_of_dvd

Premises used: mt, Int.emod_eq_zero_of_dvd