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 : 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
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
⊢ False
have hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
Tactic: have hk2 : s ^ 2 = k ^ 4 := 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
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
⊢ False
have hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
Tactic: have hh : i ^ 2 = j ^ 4 + k ^ 4 := 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
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
⊢ False
have hn : n ≠ 0
Tactic: have hn : n ≠ 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 : 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
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
hn : n ≠ 0
⊢ i.natAbs < c.natAbs
have apply : LT.lt (α := ℤ) (↑i.natAbs : ℤ) (↑c.natAbs : ℤ)
Tactic: apply Int.ofNat_lt.mp
-- 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
k : ℤ
hk : s = HPow.hPow (β := ℕ) k 2 ∨ s = -HPow.hPow (β := ℕ) k 2
hk0 : k ≠ 0
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
hn : n ≠ 0
⊢ LT.lt (α := ℤ) (↑i.natAbs : ℤ) (↑c.natAbs : ℤ)
have rw : (↑i.natAbs : ℤ) < c
Tactic: rw [← Int.eq_natAbs_of_nonneg (le_of_lt hc)]
-- 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
k : ℤ
hk : s = HPow.hPow (β := ℕ) k 2 ∨ s = -HPow.hPow (β := ℕ) k 2
hk0 : k ≠ 0
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
hn : n ≠ 0
⊢ (↑i.natAbs : ℤ) < c
have apply : HPow.hPow (β := ℕ) i 2 < c
Tactic: apply lt_of_le_of_lt (Int.natAbs_le_self_sq i)
-- 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
k : ℤ
hk : s = HPow.hPow (β := ℕ) k 2 ∨ s = -HPow.hPow (β := ℕ) k 2
hk0 : k ≠ 0
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
hn : n ≠ 0
⊢ HPow.hPow (β := ℕ) i 2 < c
have rw : m < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
Tactic: rw [← hi, ht3]
-- 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
k : ℤ
hk : s = HPow.hPow (β := ℕ) k 2 ∨ s = -HPow.hPow (β := ℕ) k 2
hk0 : k ≠ 0
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
hn : n ≠ 0
⊢ m < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
have apply : HPow.hPow (β := ℕ) m 2 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
Tactic: apply lt_of_le_of_lt (Int.le_self_sq 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 : 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
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
hn : n ≠ 0
⊢ False
have hic : i.natAbs < c.natAbs
Tactic: have hic : Int.natAbs i < Int.natAbs c := by
    apply Int.ofNat_lt.mp
    rw [← Int.eq_natAbs_of_nonneg (le_of_lt hc)]
    apply lt_of_le_of_lt (Int.natAbs_le_self_sq i)
    rw [← hi, ht3]
    apply lt_of_le_of_lt (Int.le_self_sq m)
    exact lt_add_of_pos_right (m ^ 2) (sq_pos_of_ne_zero hn)
-- 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
k : ℤ
hk : s = HPow.hPow (β := ℕ) k 2 ∨ s = -HPow.hPow (β := ℕ) k 2
hk0 : k ≠ 0
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
hn : n ≠ 0
hic : i.natAbs < c.natAbs
⊢ c.natAbs ≤ i.natAbs
have apply : Fermat42 j k i
Tactic: apply h.2 j k i
-- 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
hj2 : HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4
hk2 : HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4
hh : HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4
hn : n ≠ 0
hic : i.natAbs < c.natAbs
⊢ False
have hic' : c.natAbs ≤ i.natAbs
Tactic: have hic' : Int.natAbs c ≤ Int.natAbs i := by
    apply h.2 j k i
    exact ⟨hj0, hk0, hh.symm⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
h : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
⊢ False
have obtain : ∀ (a0 b0 c0 : ℤ) (hf : Fermat42.Minimal a0 b0 c0) (h2 : a0 % 2 = 1) (hp : 0 < c0), False
Tactic: obtain ⟨a0, b0, c0, ⟨hf, h2, hp⟩⟩ :=
    Fermat42.exists_pos_odd_minimal (And.intro ha (And.intro hb h))
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
⊢ FermatLastTheoremFor 4
have rw : FermatLastTheoremWith ℤ 4
Tactic: rw [fermatLastTheoremFor_iff_int]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
h : c ≠ 0
heq : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 4
⊢ False
have apply : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) c 2) 2
Tactic: apply @not_fermat_42 _ _ (c ^ 2) ha hb
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
h : c ≠ 0
heq : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 4
⊢ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) c 2) 2
have rw : HPow.hPow (β := ℕ) c 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) c 2) 2
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
⊢ FermatLastTheoremFor n
have inl : ∀ (hdvd : 4 ∣ n), FermatLastTheoremFor n
Tactic: obtain hdvd | ⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
inl : ∀ (hdvd : 4 ∣ n), FermatLastTheoremFor n
⊢ FermatLastTheoremFor n
have inr : ∀ (p : ℕ) (hpprime : Nat.Prime p) (hdvd : p ∣ n) (hpodd : Odd p), FermatLastTheoremFor n
Tactic: obtain hdvd | ⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremFor n
have inl : FermatLastTheoremWith ℕ 4
Tactic: apply FermatLastTheoremWith.mono hdvd
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
p : ℕ
hpprime : Nat.Prime p
hdvd : p ∣ n
hpodd : Odd p
⊢ FermatLastTheoremFor n
have inr : FermatLastTheoremWith ℕ p
Tactic: apply FermatLastTheoremWith.mono hdvd
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
have ab_nz : a * b ≠ 0
Tactic: have ab_nz := mul_ne_zero ha hb
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
ab_nz : a * b ≠ 0
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
have abc_nz : a * b * c ≠ 0
Tactic: have abc_nz := mul_ne_zero ab_nz hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
⊢ w.natDegree < a.natDegree + b.natDegree
have rw : ∀ (hw : a.wronskian b ≠ 0) (wab : w = a.wronskian b) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (ab_nz : a * b ≠ 0)
  (abc_nz : a * b * c ≠ 0),
  let abc_dr := divRadical (a * b * c);
  ∀ (abc_dr_dvd_w : abc_dr ∣ w), (a.wronskian b).natDegree < a.natDegree + b.natDegree
Tactic: rw [wab] at hw ⊢
Cleared hypotheses: hw, wab, ha, hb, hc, ab_nz, abc_nz, abc_dr, abc_dr_dvd_w
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
⊢ abc_dr.natDegree < a.natDegree + b.natDegree
have abc_dr_dvd_w₁ : w.natDegree < a.natDegree + b.natDegree
Tactic: calc
      abc_dr.natDegree ≤ w.natDegree := Polynomial.natDegree_le_of_dvd abc_dr_dvd_w hw
      _ < a.natDegree + b.natDegree := by rw [wab] at hw ⊢; exact natDegree_wronskian_lt_add hw
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
have abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
Tactic: have abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree := by
    calc
      abc_dr.natDegree ≤ w.natDegree := Polynomial.natDegree_le_of_dvd abc_dr_dvd_w hw
      _ < a.natDegree + b.natDegree := by rw [wab] at hw ⊢; exact natDegree_wronskian_lt_add hw
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ c.natDegree + 1 ≤ abc_r.natDegree
have a₁ : a.natDegree + b.natDegree + c.natDegree < a.natDegree + b.natDegree + abc_r.natDegree
Tactic: apply Nat.lt_of_add_lt_add_left