awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi : m = HPow.hPow (β := ℕ) i 2 ∨ m = -HPow.hPow (β := ℕ) i 2
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
⊢ False
have hi₁ : m = HPow.hPow (β := ℕ) i 2
Tactic: replace hi : m = i ^ 2 := Or.resolve_right hi hi'
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
⊢ False
have rw : ∀ (hs : HPow.hPow (β := ℕ) b' 2 = r * s * m) (hrsz : r * s ≠ 0) (h2b0 : b' ≠ 0) (i : ℤ)
  (hi' : ¬m = -HPow.hPow (β := ℕ) i 2) (hi : m = HPow.hPow (β := ℕ) i 2), False
Tactic: rw [mul_comm] at hs
Cleared hypotheses: hs, hrsz, h2b0, i, hi', hi
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
⊢ False
have rw : ∀ (hcp : (r * s).gcd m = 1) (b' : ℤ) (hb2' : b = 2 * b') (hs : HPow.hPow (β := ℕ) b' 2 = r * s * m) (hrsz : r * s ≠ 0)
  (h2b0 : b' ≠ 0) (i : ℤ) (hi' : ¬m = -HPow.hPow (β := ℕ) i 2) (hi : m = HPow.hPow (β := ℕ) i 2), False
Tactic: rw [Int.gcd_comm] at hcp
Cleared hypotheses: hcp, b', hb2', hs, hrsz, h2b0, i, hi', hi
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
⊢ False
have obtain : ∀ (d : ℤ) (hd : r * s = HPow.hPow (β := ℕ) d 2 ∨ r * s = -HPow.hPow (β := ℕ) d 2), False
Tactic: obtain ⟨d, hd⟩ := Int.sq_of_gcd_eq_one hcp hs.symm
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd : r * s = HPow.hPow (β := ℕ) d 2 ∨ r * s = -HPow.hPow (β := ℕ) d 2
h1 : r * s = -HPow.hPow (β := ℕ) d 2
⊢ False
have hs₁ : HPow.hPow (β := ℕ) b' 2 = -HPow.hPow (β := ℕ) d 2 * m
Tactic: rw [h1] at hs
Cleared hypotheses: hs, hd, h1
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hs : HPow.hPow (β := ℕ) b' 2 = -HPow.hPow (β := ℕ) d 2 * m
hd : r * s = HPow.hPow (β := ℕ) d 2 ∨ r * s = -HPow.hPow (β := ℕ) d 2
h1 : r * s = -HPow.hPow (β := ℕ) d 2
⊢ HPow.hPow (β := ℕ) b' 2 ≤ 0
have rw : -(HPow.hPow (β := ℕ) d 2 * m) ≤ 0
Tactic: rw [hs, (by ring : -d ^ 2 * m = -(d ^ 2 * m))]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hs : HPow.hPow (β := ℕ) b' 2 = -HPow.hPow (β := ℕ) d 2 * m
hd : r * s = HPow.hPow (β := ℕ) d 2 ∨ r * s = -HPow.hPow (β := ℕ) d 2
h1 : r * s = -HPow.hPow (β := ℕ) d 2
⊢ False
have h2₁ : HPow.hPow (β := ℕ) b' 2 ≤ 0
Tactic: have h2 : b' ^ 2 ≤ 0 := by
      rw [hs, (by ring : -d ^ 2 * m = -(d ^ 2 * m))]
      exact neg_nonpos.mpr ((mul_nonneg_iff_of_pos_right h4).mpr (sq_nonneg d))
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2_1 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hs : HPow.hPow (β := ℕ) b' 2 = -HPow.hPow (β := ℕ) d 2 * m
hd : r * s = HPow.hPow (β := ℕ) d 2 ∨ r * s = -HPow.hPow (β := ℕ) d 2
h1 : r * s = -HPow.hPow (β := ℕ) d 2
h2 : HPow.hPow (β := ℕ) b' 2 ≤ 0
⊢ False
have h2' : 0 ≤ HPow.hPow (β := ℕ) b' 2
Tactic: have h2' : 0 ≤ b' ^ 2 := by apply sq_nonneg b'
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd : r * s = HPow.hPow (β := ℕ) d 2 ∨ r * s = -HPow.hPow (β := ℕ) d 2
⊢ False
have hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2
Tactic: have hd' : ¬r * s = -d ^ 2 := by
    by_contra h1
    rw [h1] at hs
    have h2 : b' ^ 2 ≤ 0 := by
      rw [hs, (by ring : -d ^ 2 * m = -(d ^ 2 * m))]
      exact neg_nonpos.mpr ((mul_nonneg_iff_of_pos_right h4).mpr (sq_nonneg d))
    have h2' : 0 ≤ b' ^ 2 := by apply sq_nonneg b'
    exact absurd (lt_of_le_of_ne h2' (Ne.symm (pow_ne_zero _ h2b0))) (not_lt.mpr h2)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd : r * s = HPow.hPow (β := ℕ) d 2 ∨ r * s = -HPow.hPow (β := ℕ) d 2
hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2
⊢ False
have hd₁ : r * s = HPow.hPow (β := ℕ) d 2
Tactic: replace hd : r * s = d ^ 2 := Or.resolve_right hd hd'
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2
hd : r * s = HPow.hPow (β := ℕ) d 2
⊢ False
have obtain : ∀ (j : ℤ) (hj : r = HPow.hPow (β := ℕ) j 2 ∨ r = -HPow.hPow (β := ℕ) j 2), False
Tactic: obtain ⟨j, hj⟩ := Int.sq_of_gcd_eq_one htt4 hd
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2
hd : r * s = HPow.hPow (β := ℕ) d 2
j : ℤ
hj : r = HPow.hPow (β := ℕ) j 2 ∨ r = -HPow.hPow (β := ℕ) j 2
⊢ False
have hj0 : j ≠ 0
Tactic: have hj0 : j ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2
hd : r * s = HPow.hPow (β := ℕ) d 2
j : ℤ
hj : r = HPow.hPow (β := ℕ) j 2 ∨ r = -HPow.hPow (β := ℕ) j 2
hj0 : j ≠ 0
⊢ False
have rw : ∀ (hd : s * r = HPow.hPow (β := ℕ) d 2) (j : ℤ) (hj : r = HPow.hPow (β := ℕ) j 2 ∨ r = -HPow.hPow (β := ℕ) j 2)
  (hj0 : j ≠ 0), False
Tactic: rw [mul_comm] at hd
Cleared hypotheses: hd, j, hj, hj0
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2
hd : s * r = HPow.hPow (β := ℕ) d 2
j : ℤ
hj : r = HPow.hPow (β := ℕ) j 2 ∨ r = -HPow.hPow (β := ℕ) j 2
hj0 : j ≠ 0
⊢ False
have rw : ∀ (htt4 : s.gcd r = 1) (htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0) (htt6 : 0 ≤ r) (hcp : (r * s).gcd m = 1)
  (b' : ℤ) (hb2' : b = 2 * b') (hs : HPow.hPow (β := ℕ) b' 2 = r * s * m) (hrsz : r * s ≠ 0) (h2b0 : b' ≠ 0) (i : ℤ)
  (hi' : ¬m = -HPow.hPow (β := ℕ) i 2) (hi : m = HPow.hPow (β := ℕ) i 2) (d : ℤ)
  (hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2) (hd : s * r = HPow.hPow (β := ℕ) d 2) (j : ℤ)
  (hj : r = HPow.hPow (β := ℕ) j 2 ∨ r = -HPow.hPow (β := ℕ) j 2) (hj0 : j ≠ 0), False
Tactic: rw [Int.gcd_comm] at htt4
Cleared hypotheses: htt4, htt5, htt6, hcp, b', hb2', hs, hrsz, h2b0, i, hi', hi, d, hd', hd, j, hj, hj0
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : s.gcd r = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2
hd : s * r = HPow.hPow (β := ℕ) d 2
j : ℤ
hj : r = HPow.hPow (β := ℕ) j 2 ∨ r = -HPow.hPow (β := ℕ) j 2
hj0 : j ≠ 0
⊢ False
have obtain : ∀ (k : ℤ) (hk : s = HPow.hPow (β := ℕ) k 2 ∨ s = -HPow.hPow (β := ℕ) k 2), False
Tactic: obtain ⟨k, hk⟩ := Int.sq_of_gcd_eq_one htt4 hd
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : s.gcd r = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2
hd : s * r = HPow.hPow (β := ℕ) d 2
j : ℤ
hj : r = HPow.hPow (β := ℕ) j 2 ∨ r = -HPow.hPow (β := ℕ) j 2
hj0 : j ≠ 0
k : ℤ
hk : s = HPow.hPow (β := ℕ) k 2 ∨ s = -HPow.hPow (β := ℕ) k 2
⊢ False
have hk0 : k ≠ 0
Tactic: have hk0 : k ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
ha22 : HPow.hPow (β := ℕ) a 2 % 2 = 1
m n : ℤ
ht1 : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
ht2 : HPow.hPow (β := ℕ) b 2 = 2 * m * n
ht3 : c = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : HPow.hPow (β := ℕ) b 2 ≠ 0
h4 : 0 < m
r s : ℤ
left : a = HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) s 2
htt2 : n = 2 * r * s
htt3 : m = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
htt4 : s.gcd r = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -HPow.hPow (β := ℕ) i 2
hi : m = HPow.hPow (β := ℕ) i 2
d : ℤ
hd' : ¬r * s = -HPow.hPow (β := ℕ) d 2
hd : s * r = HPow.hPow (β := ℕ) d 2
j : ℤ
hj : r = HPow.hPow (β := ℕ) j 2 ∨ r = -HPow.hPow (β := ℕ) j 2
hj0 : j ≠ 0
k : ℤ
hk : s = HPow.hPow (β := ℕ) k 2 ∨ s = -HPow.hPow (β := ℕ) k 2
hk0 : k ≠ 0
⊢ False
have hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
Tactic: have hj2 : r ^ 2 = j ^ 4 := by grind