awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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 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))
Tactic: have h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)) := by ring
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
have H : Ne (α := ℤ) 2 0
Tactic: rw [h2, Int.mul_ediv_cancel_left, Int.mul_emod_right]
-- 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
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))
⊢ 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 h3 : (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
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
have 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
Tactic: refine ⟨⟨_, h1⟩, ⟨_, h2⟩, h3, ?_⟩
-- 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
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
⊢ ((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 h20 : Ne (α := ℤ) 2 0
Tactic: have h20 : (2 : ℤ) ≠ 0 := by decide
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ ((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 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
Tactic: rw [h1, h2, Int.mul_ediv_cancel_left _ h20, Int.mul_ediv_cancel_left _ h20]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ (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
have 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
Tactic: by_contra h4
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have 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
Tactic: obtain ⟨p, hp, hp1, hp2⟩ := Nat.Prime.not_coprime_iff_dvd.mp h4
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ False
have apply : p ∣ 1
Tactic: apply hp.not_dvd_one
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 ∣ 1
have rw : p ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
Tactic: rw [← 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
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 ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
have hp1₁ : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 - HPow.hPow (β := ℕ) n0 2 + m0 - n0)
Tactic: rw [← Int.natCast_dvd] at hp1 hp2
Cleared hypotheses: hp1, hp2
-- 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
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 ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
have hp2₁ : (↑p : ℤ) ∣ 2 * (HPow.hPow (β := ℕ) m0 2 + HPow.hPow (β := ℕ) n0 2 + m0 + n0) + 1
Tactic: rw [← Int.natCast_dvd] at hp1 hp2
Cleared hypotheses: hp1, hp2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
have a : p ∣ (m0 * 2 + 1).natAbs
Tactic: apply Nat.dvd_gcd
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ p ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
have a₁ : p ∣ (n0 * 2 + 1).natAbs
Tactic: apply Nat.dvd_gcd
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 ∣ (m0 * 2 + 1).natAbs
have a : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2
Tactic: apply Int.Prime.dvd_natAbs_of_coe_dvd_sq hp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) ∣ HPow.hPow (β := ℕ) (m0 * 2 + 1) 2
have 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)
Tactic: convert! dvd_add hp1 hp2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 ∣ (n0 * 2 + 1).natAbs
have a : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) (n0 * 2 + 1) 2
Tactic: apply Int.Prime.dvd_natAbs_of_coe_dvd_sq hp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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 : ℤ) ∣ HPow.hPow (β := ℕ) (n0 * 2 + 1) 2
have 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)
Tactic: convert! dvd_sub hp2 hp1
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
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
⊢ h.IsPrimitiveClassified
have hz : z ≠ 0
Tactic: have hz : z ≠ 0 := ne_of_gt hzpos
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
have apply : HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
  HDiv.hDiv (α := ℚ) (↑(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) : ℚ)
    (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)
Tactic: apply Rat.div_int_inj hzpos hm2n2 (h.coprime_of_coprime hc) H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ HDiv.hDiv (α := ℚ) (↑y : ℚ) (↑z : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) : ℚ)
      (↑(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) : ℚ)
have 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) : ℚ)
Tactic: rw [hw2]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
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
⊢ (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) : ℚ)
have 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)
Tactic: norm_cast