awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have neg : p ∣ 1
Tactic: apply hp.not_dvd_one
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 ∣ 1
have neg : p ∣ m.gcd n
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) = 1
have rw : (-(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)).natAbs.gcd
    (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2).natAbs =
  1
Tactic: rw [Int.gcd, ← Int.natAbs_neg (m ^ 2 - n ^ 2)]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (-(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)).natAbs.gcd
      (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2).natAbs =
    1
have rw : (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) m 2).natAbs.gcd (HPow.hPow (β := ℕ) n 2 + HPow.hPow (β := ℕ) m 2).natAbs =
  1
Tactic: rw [(by ring : -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2), add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) m 2).natAbs.gcd
      (HPow.hPow (β := ℕ) n 2 + HPow.hPow (β := ℕ) m 2).natAbs =
    1
have apply : n.gcd m = 1
Tactic: apply coprime_sq_sub_sq_add_of_even_odd _ hn hm
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
have by_contra : ∀ (H : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have obtain : ∀ (p : ℕ) (hp : Nat.Prime p) (hp1 : p ∣ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).natAbs)
  (hp2 : p ∣ (2 * m * n).natAbs), False
Tactic: obtain ⟨p, hp, hp1, hp2⟩ := Nat.Prime.not_coprime_iff_dvd.mp H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ False
have hp1₁ : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
Tactic: rw [← Int.natCast_dvd] at hp1 hp2
Cleared hypotheses: hp1, hp2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ False
have hp2₁ : (↑p : ℤ) ∣ 2 * m * n
Tactic: rw [← Int.natCast_dvd] at hp1 hp2
Cleared hypotheses: hp1, hp2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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) : ℤ)
have rw : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑1 : ℤ)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) (↑1 : ℤ)
have norm_cast : ¬p ∣ 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ False
have hnp : ¬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)
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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) : ℤ)
⊢ False
have inl : ∀ (hp2m : p ∣ (2 * m).natAbs), False
Tactic: rcases Int.Prime.dvd_mul hp hp2 with hp2m | hpn
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have inr : ∀ (hpn : p ∣ n.natAbs), False
Tactic: rcases Int.Prime.dvd_mul hp hp2 with hp2m | hpn
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ False
have hp2m₁ : p ∣ Int.natAbs 2 * m.natAbs
Tactic: rw [Int.natAbs_mul] at hp2m
Cleared hypotheses: hp2m
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have inl : ∀ (hp2 : p ∣ Int.natAbs 2), False
Tactic: rcases (Nat.Prime.dvd_mul hp).mp hp2m with hp2 | hpm
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have inl₁ : ∀ (hpm : p ∣ m.natAbs), False
Tactic: rcases (Nat.Prime.dvd_mul hp).mp hp2m with hp2 | hpm
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ False
have hp2' : p = 2
Tactic: have hp2' : p = 2 := (Nat.le_of_dvd zero_lt_two hp2).antisymm hp.two_le
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have inl : ∀ (hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2), False
Tactic: revert hp1
Cleared hypotheses: hp1
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ ∀ (hp1 : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2), False
have inl : ∀ (hp1 : (↑2 : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2), False
Tactic: rw [hp2']
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ ∀ (hp1 : (↑2 : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2), False
have inl : ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) % (↑2 : ℤ) = 0
Tactic: apply mt Int.emod_eq_zero_of_dvd
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ ¬(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) % (↑2 : ℤ) = 0
have inl : ¬-HMod.hMod (α := ℤ) 1 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]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have inl : (↑p : ℤ) ∣ n
Tactic: apply mt (Int.dvd_coe_gcd (Int.natCast_dvd.mpr hpm)) hnp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) ∣ n
have inl : (↑p : ℤ) ∣ n ∨ (↑p : ℤ) ∣ n
Tactic: apply or_self_iff.mp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) ∣ n ∨ (↑p : ℤ) ∣ n
have inl : (↑p : ℤ) ∣ n * n
Tactic: apply Int.Prime.dvd_mul' hp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) ∣ n * n
have inl : (↑p : ℤ) ∣ -(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) + m * m
Tactic: rw [(by ring : n * n = -(m ^ 2 - n ^ 2) + m * m)]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ False
have hnp₁ : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(n.gcd m) : ℤ)
Tactic: rw [Int.gcd_comm] at hnp
Cleared hypotheses: hnp, hpn
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have inr : (↑p : ℤ) ∣ m
Tactic: apply mt (Int.dvd_coe_gcd (Int.natCast_dvd.mpr hpn)) hnp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) ∣ m
have inr : (↑p : ℤ) ∣ m ∨ (↑p : ℤ) ∣ m
Tactic: apply or_self_iff.mp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) ∣ m ∨ (↑p : ℤ) ∣ m
have inr : (↑p : ℤ) ∣ m * m
Tactic: apply Int.Prime.dvd_mul' hp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) ∣ m * m
have inr : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 + n * n
Tactic: rw [(by ring : m * m = m ^ 2 - n ^ 2 + n * n)]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) ∣ HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 + n * n
have inr : (↑p : ℤ) ∣ n * n
Tactic: apply dvd_add hp1
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
have rw : (-(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)).natAbs.gcd (2 * m * n).natAbs = 1
Tactic: rw [Int.gcd, ← Int.natAbs_neg (m ^ 2 - n ^ 2)]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (-(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)).natAbs.gcd (2 * m * n).natAbs = 1
have rw : (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) m 2).natAbs.gcd (2 * n * m).natAbs = 1
Tactic: rw [(by ring : 2 * m * n = 2 * n * m), (by ring : -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2)]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (HPow.hPow (β := ℕ) n 2 - HPow.hPow (β := ℕ) m 2).natAbs.gcd (2 * n * m).natAbs = 1
have apply : n.gcd m = 1
Tactic: apply coprime_sq_sub_mul_of_even_odd _ hn hm
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hmn : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
have inl : ∀ (h1 : m % 2 = 0 ∧ n % 2 = 1), (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
Tactic: rcases hmn with h1 | h2
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
have inr : ∀ (h2 : m % 2 = 1 ∧ n % 2 = 0), (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2).gcd (2 * m * n) = 1
Tactic: rcases hmn with h1 | h2
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 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
have 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
Tactic: obtain ⟨m0, hm2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hm)
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 1
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
have 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
Tactic: obtain ⟨n0, hn2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hn)
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ 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
have 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
Tactic: rw [sub_eq_iff_eq_add] at hm2 hn2
Cleared hypotheses: hm2, n0, hn2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ 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
have 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
Tactic: subst m
Cleared hypotheses: m, h, hm, hm2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ 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
have 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
Tactic: subst n
Cleared hypotheses: n, hn, hn2, h
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
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
have 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)
Tactic: have h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) := by
    ring