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 : m.gcd (r * s) = 1
hb2 : 2 ∣ b
obtain : ∀ (b' : ℤ) (hb2' : b = 2 * b'), False
⊢ False

Tactic:
obtain ⟨b', hb2'⟩ := hb2
-- 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 : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
⊢ Ne (α := ℤ) 4 0

Tactic:
simp
-- 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 : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
apply : 4 * HPow.hPow (β := ℕ) b' 2 = 4 * (m * (r * s))
⊢ HPow.hPow (β := ℕ) b' 2 = m * (r * s)

Tactic:
apply (mul_right_inj' (by simp : (4 : ℤ) ≠ 0)).mp

Premises used: Iff.mp, mul_right_inj'
-- 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 : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
⊢ 4 * HPow.hPow (β := ℕ) b' 2 = 4 * (m * (r * s))

Tactic:
linear_combination (-b - 2 * b') * hb2' + ht2 + 2 * m * htt2

Premises used: HMul.hMul, HSub.hSub, OfNat.ofNat, Neg.neg
-- 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 : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
⊢ HPow.hPow (β := ℕ) b' 2 = m * (r * s)

Tactic:
have hs : b' ^ 2 = m * (r * s) := by
    apply (mul_right_inj' (by simp : (4 : ℤ) ≠ 0)).mp
    linear_combination (-b - 2 * b') * hb2' + ht2 + 2 * m * htt2
-- 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 : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : HPow.hPow (β := ℕ) b' 2 = m * (r * s)
⊢ r * s ≠ 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 : 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)
⊢ r * s ≠ 0

Tactic:
have hrsz : r * s ≠ 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 : 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
⊢ b' ≠ 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 : 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
⊢ b' ≠ 0

Tactic:
have h2b0 : b' ≠ 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 : 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
obtain : ∀ (i : ℤ) (hi : m = HPow.hPow (β := ℕ) i 2 ∨ m = -HPow.hPow (β := ℕ) i 2), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := Int.sq_of_gcd_eq_one hcp hs.symm

Premises used: Int.sq_of_gcd_eq_one, Eq.symm
-- 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 : 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
by_contra : ∀ (h1 : m = -HPow.hPow (β := ℕ) i 2), False
⊢ ¬m = -HPow.hPow (β := ℕ) i 2

Tactic:
by_contra h1
-- 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 : 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
h1 : m = -HPow.hPow (β := ℕ) i 2
⊢ -HPow.hPow (β := ℕ) i 2 ≤ 0

Tactic:
have hit : -i ^ 2 ≤ 0 := neg_nonpos.mpr (sq_nonneg i)
-- 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 : 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
h1 : m = -HPow.hPow (β := ℕ) i 2
hit : -HPow.hPow (β := ℕ) i 2 ≤ 0
⊢ m ≤ 0

Tactic:
rw [← h1] at hit
-- 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 : 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
h1 : m = -HPow.hPow (β := ℕ) i 2
hit : m ≤ 0
⊢ False

Tactic:
apply absurd h4 (not_lt.mpr hit)

Premises used: Iff.mpr, absurd, not_lt
-- 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 : 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
⊢ ¬m = -HPow.hPow (β := ℕ) i 2

Tactic:
have hi' : ¬m = -i ^ 2 := by
    by_contra h1
    have hit : -i ^ 2 ≤ 0 := neg_nonpos.mpr (sq_nonneg i)
    rw [← h1] at hit
    apply absurd h4 (not_lt.mpr hit)
-- 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 : 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
⊢ m = HPow.hPow (β := ℕ) i 2

Tactic:
replace hi : m = i ^ 2 := Or.resolve_right hi hi'
-- 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 : 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
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
⊢ False

Tactic:
rw [mul_comm] at hs

Premises used: mul_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 : 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
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
⊢ False

Tactic:
rw [Int.gcd_comm] at hcp

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 : 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
obtain : ∀ (d : ℤ) (hd : r * s = HPow.hPow (β := ℕ) d 2 ∨ r * s = -HPow.hPow (β := ℕ) d 2), False
⊢ False

Tactic:
obtain ⟨d, hd⟩ := Int.sq_of_gcd_eq_one hcp hs.symm

Premises used: Int.sq_of_gcd_eq_one, Eq.symm
-- 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 ∨ r * s = -HPow.hPow (β := ℕ) d 2
by_contra : ∀ (h1 : r * s = -HPow.hPow (β := ℕ) d 2), False
⊢ ¬r * s = -HPow.hPow (β := ℕ) d 2

Tactic:
by_contra h1
-- 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 ∨ r * s = -HPow.hPow (β := ℕ) d 2
h1 : r * s = -HPow.hPow (β := ℕ) d 2
⊢ HPow.hPow (β := ℕ) b' 2 = -HPow.hPow (β := ℕ) d 2 * m

Tactic:
rw [h1] at hs