awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z : ℤ
k : ℕ
x0 y0 : ℤ
left : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 ∣ x0 * (↑k : ℤ) * (x0 * (↑k : ℤ)) + y0 * (↑k : ℤ) * (y0 * (↑k : ℤ))
have neg : HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 ∣ HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 * (x0 * x0 + y0 * y0)
Tactic: rw [(by ring : x0 * k * (x0 * k) + y0 * k * (y0 * k) = (k : ℤ) ^ 2 * (x0 * x0 + y0 * y0))]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
have pos : ∀ (h0 : x.gcd y = 0), PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
Tactic: by_cases h0 : Int.gcd x y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
pos : ∀ (h0 : x.gcd y = 0), PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
have neg : ∀ (h0 : ¬x.gcd y = 0), PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
Tactic: by_cases h0 : Int.gcd x y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
have hx : x = 0
Tactic: obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
have hy : y = 0
Tactic: obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
have hz : z = 0
Tactic: have hz : z = 0 := by
      simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
        or_self_iff] using h
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
have neg : ∀ (z0 : ℤ) (h : PythagoreanTriple x y ((↑(x.gcd y) : ℤ) * z0)),
  PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) ((↑(x.gcd y) : ℤ) * z0 / (↑(x.gcd y) : ℤ))
Tactic: rcases h.gcd_dvd with ⟨z0, rfl⟩
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y : ℤ
h0 : ¬x.gcd y = 0
z0 : ℤ
h : PythagoreanTriple x y ((↑(x.gcd y) : ℤ) * z0)
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) ((↑(x.gcd y) : ℤ) * z0 / (↑(x.gcd y) : ℤ))
have neg : ∀ (k : ℕ) (x0 y0 : ℤ) (k0 : 0 < k) (h2 : x0.gcd y0 = 1) (h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0)
  (h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)),
  PythagoreanTriple (x0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
    (y0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
    ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0 / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
Tactic: obtain ⟨k, x0, y0, k0, h2, rfl, rfl⟩ :
    ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
    Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)
Cleared hypotheses: x, y, h0, h
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)
⊢ Ne (α := ℤ) (↑k : ℤ) 0
have norm_cast : ¬k = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)
⊢ ¬k = 0
have rwa : ∀ (k0 : k ≠ 0) (h2 : x0.gcd y0 = 1) (h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0)
  (h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)), ¬k = 0
Tactic: rwa [pos_iff_ne_zero] at k0
Cleared hypotheses: k0, h2, h0, h
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)
⊢ PythagoreanTriple (x0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
    (y0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
    ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0 / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
have hk : Ne (α := ℤ) (↑k : ℤ) 0
Tactic: have hk : (k : ℤ) ≠ 0 := by
    norm_cast
    rwa [pos_iff_ne_zero] at k0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)
hk : Ne (α := ℤ) (↑k : ℤ) 0
⊢ PythagoreanTriple (x0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
    (y0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
    ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0 / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
have neg : ∀ (h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑k : ℤ) * z0)) (hk : Ne (α := ℤ) (↑k : ℤ) 0),
  PythagoreanTriple (x0 * (↑k : ℤ) / (↑k : ℤ)) (y0 * (↑k : ℤ) / (↑k : ℤ)) ((↑k : ℤ) * z0 / (↑k : ℤ))
Tactic: rw [Int.gcd_mul_right, h2, Int.natAbs_natCast, one_mul] at h ⊢
Cleared hypotheses: h, hk
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑k : ℤ) * z0)
hk : Ne (α := ℤ) (↑k : ℤ) 0
⊢ PythagoreanTriple (x0 * (↑k : ℤ) / (↑k : ℤ)) (y0 * (↑k : ℤ) / (↑k : ℤ)) ((↑k : ℤ) * z0 / (↑k : ℤ))
have h₁ : PythagoreanTriple x0 y0 z0
Tactic: rw [mul_comm x0, mul_comm y0, mul_iff k hk] at h
Cleared hypotheses: h, hk
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple x0 y0 z0
hk : Ne (α := ℤ) (↑k : ℤ) 0
⊢ PythagoreanTriple (x0 * (↑k : ℤ) / (↑k : ℤ)) (y0 * (↑k : ℤ) / (↑k : ℤ)) ((↑k : ℤ) * z0 / (↑k : ℤ))
have neg : PythagoreanTriple x0 (y0 * (↑k : ℤ) / (↑k : ℤ)) ((↑k : ℤ) * z0 / (↑k : ℤ))
Tactic: rwa [Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel_left _ hk]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple x0 y0 z0
hk : Ne (α := ℤ) (↑k : ℤ) 0
neg : PythagoreanTriple x0 (y0 * (↑k : ℤ) / (↑k : ℤ)) ((↑k : ℤ) * z0 / (↑k : ℤ))
⊢ PythagoreanTriple (x0 * (↑k : ℤ) / (↑k : ℤ)) (y0 * (↑k : ℤ) / (↑k : ℤ)) ((↑k : ℤ) * z0 / (↑k : ℤ))
have neg₁ : PythagoreanTriple x0 y0 ((↑k : ℤ) * z0 / (↑k : ℤ))
Tactic: rwa [Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel_left _ hk]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hp : h.IsPrimitiveClassified
⊢ h.IsClassified
have obtain : ∀ (m n : ℤ)
  (H :
    (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
        x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
      m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)),
  h.IsClassified
Tactic: obtain ⟨m, n, H⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
m n : ℤ
H :
  (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
      x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ h.IsClassified
have h₁ : (x = 1 * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = 1 * (2 * m * n) ∨
    x = 1 * (2 * m * n) ∧ y = 1 * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
  m.gcd n = 1
Tactic: use 1, m, n
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ h.IsClassified
have h₁ : x = (↑(x.gcd y) : ℤ) * (x / (↑(x.gcd y) : ℤ))
Tactic: convert!
    h.normalize.mul_isClassified (Int.gcd x y)
      (isClassified_of_isPrimitiveClassified h.normalize hc)
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
h₁ : x = (↑(x.gcd y) : ℤ) * (x / (↑(x.gcd y) : ℤ))
⊢ h.IsClassified
have h₂ : y = (↑(x.gcd y) : ℤ) * (y / (↑(x.gcd y) : ℤ))
Tactic: convert!
    h.normalize.mul_isClassified (Int.gcd x y)
      (isClassified_of_isPrimitiveClassified h.normalize hc)
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
h₁ : x = (↑(x.gcd y) : ℤ) * (x / (↑(x.gcd y) : ℤ))
h₂ : y = (↑(x.gcd y) : ℤ) * (y / (↑(x.gcd y) : ℤ))
⊢ h.IsClassified
have h₃ : z = (↑(x.gcd y) : ℤ) * (z / (↑(x.gcd y) : ℤ))
Tactic: convert!
    h.normalize.mul_isClassified (Int.gcd x y)
      (isClassified_of_isPrimitiveClassified h.normalize hc)
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ x = (↑(x.gcd y) : ℤ) * (x / (↑(x.gcd y) : ℤ))
have h₁ : (↑(x.gcd y) : ℤ) ∣ x
Tactic: rw [Int.mul_ediv_cancel']
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ y = (↑(x.gcd y) : ℤ) * (y / (↑(x.gcd y) : ℤ))
have h₁ : (↑(x.gcd y) : ℤ) ∣ y
Tactic: rw [Int.mul_ediv_cancel']
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ z = (↑(x.gcd y) : ℤ) * (z / (↑(x.gcd y) : ℤ))
have h₁ : (↑(x.gcd y) : ℤ) ∣ z
Tactic: rw [Int.mul_ediv_cancel']
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ z ≠ 0
have suffices : 0 < z * z
Tactic: suffices 0 < z * z by
    rintro rfl
    norm_num at this
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < z * z
have rw : 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rw [← h.eq, ← sq, ← sq]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ x.gcd y ≠ 0
have rw : Ne (α := ℕ) 1 0
Tactic: rw [hc]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have hc' : x.gcd y ≠ 0
Tactic: have hc' : Int.gcd x y ≠ 0 := by
    rw [hc]
    exact one_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have inl : ∀ (hxz : x ≠ 0), 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rcases Int.ne_zero_of_gcd hc' with hxz | hyz
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
inl : ∀ (hxz : x ≠ 0), 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have inr : ∀ (hyz : y ≠ 0), 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rcases Int.ne_zero_of_gcd hc' with hxz | hyz
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x = 0
⊢ h.IsPrimitiveClassified
have subst : ∀ (h : PythagoreanTriple 0 y z) (hc : Int.gcd 0 y = 1), h.IsPrimitiveClassified
Tactic: subst x
Cleared hypotheses: x, h, hc, hx
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.gcd 0 y = 1
⊢ h.IsPrimitiveClassified
have hc₁ : Nat.gcd 0 y.natAbs = 1
Tactic: change Nat.gcd 0 (Int.natAbs y) = 1 at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Nat.gcd 0 y.natAbs = 1
⊢ h.IsPrimitiveClassified
have hc₁ : y.natAbs = 1
Tactic: rw [Nat.gcd_zero_left (Int.natAbs y)] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
⊢ h.IsPrimitiveClassified
have inl : ∀ (hy : y = (↑y.natAbs : ℤ)), h.IsPrimitiveClassified
Tactic: rcases Int.natAbs_eq y with hy | hy
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
inl : ∀ (hy : y = (↑y.natAbs : ℤ)), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified
have inr : ∀ (hy : y = -(↑y.natAbs : ℤ)), h.IsPrimitiveClassified
Tactic: rcases Int.natAbs_eq y with hy | hy
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = (↑y.natAbs : ℤ)
⊢ h.IsPrimitiveClassified
have h₁ : (0 = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2 ∧ y = HMul.hMul (α := ℤ) 2 1 * 0 ∨
    0 = HMul.hMul (α := ℤ) 2 1 * 0 ∧ y = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2) ∧
  Int.gcd 1 0 = 1 ∧
    (HMod.hMod (α := ℤ) 1 2 = 0 ∧ HMod.hMod (α := ℤ) 0 2 = 1 ∨ HMod.hMod (α := ℤ) 1 2 = 1 ∧ HMod.hMod (α := ℤ) 0 2 = 0)
Tactic: use 1, 0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = (↑y.natAbs : ℤ)
⊢ (0 = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2 ∧ y = HMul.hMul (α := ℤ) 2 1 * 0 ∨
      0 = HMul.hMul (α := ℤ) 2 1 * 0 ∧ y = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2) ∧
    Int.gcd 1 0 = 1 ∧
      (HMod.hMod (α := ℤ) 1 2 = 0 ∧ HMod.hMod (α := ℤ) 0 2 = 1 ∨
        HMod.hMod (α := ℤ) 1 2 = 1 ∧ HMod.hMod (α := ℤ) 0 2 = 0)
have h₁ : (0 = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2 ∧ (↑1 : ℤ) = HMul.hMul (α := ℤ) 2 1 * 0 ∨
    0 = HMul.hMul (α := ℤ) 2 1 * 0 ∧ (↑1 : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2) ∧
  Int.natAbs 1 = 1 ∧
    (HMod.hMod (α := ℤ) 1 2 = 0 ∧ HMod.hMod (α := ℤ) 0 2 = 1 ∨ HMod.hMod (α := ℤ) 1 2 = 1 ∧ HMod.hMod (α := ℤ) 0 2 = 0)
Tactic: rw [hy, hc, Int.gcd_zero_right]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -(↑y.natAbs : ℤ)
⊢ h.IsPrimitiveClassified
have h₁ : (0 = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2 ∧ y = HMul.hMul (α := ℤ) 2 0 * 1 ∨
    0 = HMul.hMul (α := ℤ) 2 0 * 1 ∧ y = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2) ∧
  Int.gcd 0 1 = 1 ∧
    (HMod.hMod (α := ℤ) 0 2 = 0 ∧ HMod.hMod (α := ℤ) 1 2 = 1 ∨ HMod.hMod (α := ℤ) 0 2 = 1 ∧ HMod.hMod (α := ℤ) 1 2 = 0)
Tactic: use 0, 1
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -(↑y.natAbs : ℤ)
⊢ (0 = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2 ∧ y = HMul.hMul (α := ℤ) 2 0 * 1 ∨
      0 = HMul.hMul (α := ℤ) 2 0 * 1 ∧ y = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2) ∧
    Int.gcd 0 1 = 1 ∧
      (HMod.hMod (α := ℤ) 0 2 = 0 ∧ HMod.hMod (α := ℤ) 1 2 = 1 ∨
        HMod.hMod (α := ℤ) 0 2 = 1 ∧ HMod.hMod (α := ℤ) 1 2 = 0)
have h₁ : (0 = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2 ∧ -(↑1 : ℤ) = HMul.hMul (α := ℤ) 2 0 * 1 ∨
    0 = HMul.hMul (α := ℤ) 2 0 * 1 ∧ -(↑1 : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) 0 2 - HPow.hPow (α := ℤ) (β := ℕ) 1 2) ∧
  Int.natAbs 1 = 1 ∧
    (HMod.hMod (α := ℤ) 0 2 = 0 ∧ HMod.hMod (α := ℤ) 1 2 = 1 ∨ HMod.hMod (α := ℤ) 0 2 = 1 ∧ HMod.hMod (α := ℤ) 1 2 = 0)
Tactic: rw [hy, hc, Int.gcd_zero_left]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ y.gcd z = 1
have by_contra : ∀ (H : ¬y.gcd z = 1), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
⊢ False
have obtain : ∀ (p : ℕ) (hp : Nat.Prime p) (hpy : p ∣ y.natAbs) (hpz : p ∣ z.natAbs), False
Tactic: obtain ⟨p, hp, hpy, hpz⟩ := Nat.Prime.not_coprime_iff_dvd.mp H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ False
have apply : p ∣ 1
Tactic: apply hp.not_dvd_one
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ p ∣ 1
have rw : p ∣ x.gcd y
Tactic: rw [← hc]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ p ∣ x.gcd y
have apply : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) x 2
Tactic: apply Nat.dvd_gcd (Int.Prime.dvd_natAbs_of_coe_dvd_sq hp _ _) hpy
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ (↑p : ℤ) ∣ HPow.hPow (β := ℕ) x 2
have rw : (↑p : ℤ) ∣ z * z - y * y
Tactic: rw [sq, eq_sub_of_add_eq h]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ (↑p : ℤ) ∣ z * z - y * y
have hpy₁ : (↑p : ℤ) ∣ y
Tactic: rw [← Int.natCast_dvd] at hpy hpz
Cleared hypotheses: hpy, hpz
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
hpy₁ : (↑p : ℤ) ∣ y
⊢ (↑p : ℤ) ∣ z * z - y * y
have hpz₁ : (↑p : ℤ) ∣ z
Tactic: rw [← Int.natCast_dvd] at hpy hpz
Cleared hypotheses: hpy, hpz
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
⊢ (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)).2 ≠ -1
have simp : ¬Eq.{u_1 + 1} (α := K) 1 (-1)
Tactic: simp only [Ne, div_eq_iff (hk x), neg_mul, one_mul, neg_add, sub_eq_add_neg, add_left_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
⊢ (fun (p : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }) ↦
        (↑p : K × K).1 / ((↑p : K × K).2 + 1))
      ((fun (x : K) ↦
          (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1)
              (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)) ⋯ :
            { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }))
        x) =
    x
have h2 : HAdd.hAdd (α := K) 1 1 = 2
Tactic: have h2 : (1 + 1 : K) = 2 := by norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
h2 : HAdd.hAdd (α := K) 1 1 = 2
⊢ Ne.{u_1 + 1} (α := K) 2 0
have h : 2 = 1 + HPow.hPow (α := K) (β := ℕ) 1 2
Tactic: convert! hk 1
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
h2 : HAdd.hAdd (α := K) 1 1 = 2
⊢ 2 = 1 + HPow.hPow (α := K) (β := ℕ) 1 2
have h : 2 = HAdd.hAdd (α := K) 1 1
Tactic: rw [one_pow 2, h2]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
h2 : HAdd.hAdd (α := K) 1 1 = 2
h : 2 = HAdd.hAdd (α := K) 1 1
⊢ 2 = 1 + HPow.hPow (α := K) (β := ℕ) 1 2
have h₁ : Eq.{u_1 + 1} (α := K) 2 2
Tactic: rw [one_pow 2, h2]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
K : Type u_1
inst : Field K
hk : ∀ (x : K), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
x : K
h2 : HAdd.hAdd (α := K) 1 1 = 2
⊢ (fun (p : { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }) ↦
        (↑p : K × K).1 / ((↑p : K × K).2 + 1))
      ((fun (x : K) ↦
          (Subtype.mk (p := fun (p : K × K) ↦ HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1)
              (2 * x / (1 + HPow.hPow (β := ℕ) x 2), (1 - HPow.hPow (β := ℕ) x 2) / (1 + HPow.hPow (β := ℕ) x 2)) ⋯ :
            { p : K × K // HPow.hPow (β := ℕ) p.1 2 + HPow.hPow (β := ℕ) p.2 2 = 1 ∧ p.2 ≠ -1 }))
        x) =
    x
have h3 : Ne.{u_1 + 1} (α := K) 2 0
Tactic: have h3 : (2 : K) ≠ 0 := by
      convert! hk 1
      rw [one_pow 2, h2]