awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Four
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
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
⊢ False

Tactic:
rw [Int.gcd_comm] at htt4

Premises used: Int.gcd_comm
-- Module: Mathlib.NumberTheory.FLT.Four
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
obtain : ∀ (k : ℤ) (hk : s = HPow.hPow (β := ℕ) k 2 ∨ s = -HPow.hPow (β := ℕ) k 2), False
⊢ False

Tactic:
obtain ⟨k, hk⟩ := Int.sq_of_gcd_eq_one htt4 hd

Premises used: Int.sq_of_gcd_eq_one
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ k ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ k ≠ 0

Tactic:
have hk0 : k ≠ 0 := by grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4

Tactic:
grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ HPow.hPow (β := ℕ) r 2 = HPow.hPow (β := ℕ) j 4

Tactic:
have hj2 : r ^ 2 = j ^ 4 := by grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4

Tactic:
grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ HPow.hPow (β := ℕ) s 2 = HPow.hPow (β := ℕ) k 4

Tactic:
have hk2 : s ^ 2 = k ^ 4 := by grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4

Tactic:
grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ HPow.hPow (β := ℕ) i 2 = HPow.hPow (β := ℕ) j 4 + HPow.hPow (β := ℕ) k 4

Tactic:
have hh : i ^ 2 = j ^ 4 + k ^ 4 := by grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ n ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ n ≠ 0

Tactic:
have hn : n ≠ 0 := by grind
-- Module: Mathlib.NumberTheory.FLT.Four
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
apply : LT.lt (α := ℤ) (↑i.natAbs : ℤ) (↑c.natAbs : ℤ)
⊢ i.natAbs < c.natAbs

Tactic:
apply Int.ofNat_lt.mp

Premises used: Int.ofNat_lt, Iff.mp
-- Module: Mathlib.NumberTheory.FLT.Four
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
rw : (↑i.natAbs : ℤ) < c
⊢ LT.lt (α := ℤ) (↑i.natAbs : ℤ) (↑c.natAbs : ℤ)

Tactic:
rw [← Int.eq_natAbs_of_nonneg (le_of_lt hc)]

Premises used: le_of_lt, Int.eq_natAbs_of_nonneg
-- Module: Mathlib.NumberTheory.FLT.Four
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
apply : HPow.hPow (β := ℕ) i 2 < c
⊢ (↑i.natAbs : ℤ) < c

Tactic:
apply lt_of_le_of_lt (Int.natAbs_le_self_sq i)

Premises used: lt_of_le_of_lt, Int.natAbs_le_self_sq
-- Module: Mathlib.NumberTheory.FLT.Four
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
rw : m < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ HPow.hPow (β := ℕ) i 2 < c

Tactic:
rw [← hi, ht3]