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 : 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 (β := ℕ) m 2 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ m < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2

Tactic:
apply lt_of_le_of_lt (Int.le_self_sq m)

Premises used: lt_of_le_of_lt, Int.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
⊢ HPow.hPow (β := ℕ) m 2 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2

Tactic:
lt_add_of_pos_right (m ^ 2) (sq_pos_of_ne_zero hn)

Premises used: lt_add_of_pos_right, HPow.hPow, sq_pos_of_ne_zero, OfNat.ofNat
-- 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
⊢ HPow.hPow (β := ℕ) m 2 < HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2

Tactic:
exact lt_add_of_pos_right (m ^ 2) (sq_pos_of_ne_zero hn)

Premises used: lt_add_of_pos_right, HPow.hPow, sq_pos_of_ne_zero, OfNat.ofNat
-- 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
⊢ 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)
-- 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
hic : i.natAbs < c.natAbs
apply : Fermat42 j k i
⊢ c.natAbs ≤ i.natAbs

Tactic:
apply h.2 j k i

Premises used: And.right
-- 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
hic : i.natAbs < c.natAbs
⊢ Fermat42 j k i

Tactic:
⟨hj0, hk0, hh.symm⟩

Premises used: And.intro, Fermat42, 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 : 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
⊢ Fermat42 j k i

Tactic:
exact ⟨hj0, hk0, hh.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 : 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

Tactic:
have hic' : Int.natAbs c ≤ Int.natAbs i := by
    apply h.2 j k i
    exact ⟨hj0, hk0, hh.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 : 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
hic' : c.natAbs ≤ i.natAbs
⊢ False

Tactic:
apply absurd (not_le_of_gt hic) (not_not.mpr hic')

Premises used: Iff.mpr, Classical.not_not, absurd, not_le_of_gt
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
h : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
obtain : ∀ (a0 b0 c0 : ℤ) (hf : Fermat42.Minimal a0 b0 c0) (h2 : a0 % 2 = 1) (hp : 0 < c0), False
⊢ False

Tactic:
obtain ⟨a0, b0, c0, ⟨hf, h2, hp⟩⟩ :=
    Fermat42.exists_pos_odd_minimal (And.intro ha (And.intro hb h))

Premises used: Fermat42.exists_pos_odd_minimal, And.intro
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
h : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
a0 b0 c0 : ℤ
hf : Fermat42.Minimal a0 b0 c0
h2 : a0 % 2 = 1
hp : 0 < c0
⊢ False

Tactic:
apply Fermat42.not_minimal hf h2 hp

Premises used: Fermat42.not_minimal
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
rw : FermatLastTheoremWith ℤ 4
⊢ FermatLastTheoremFor 4

Tactic:
rw [fermatLastTheoremFor_iff_int]

Premises used: fermatLastTheoremFor_iff_int
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
_ : c ≠ 0 → HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 ≠ HPow.hPow (β := ℕ) c 4
⊢ c ≠ 0 → HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 ≠ HPow.hPow (β := ℕ) c 4

Tactic:
_
-- Module: Mathlib.NumberTheory.FLT.Four
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
apply : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) c 2) 2
⊢ False

Tactic:
apply @not_fermat_42 _ _ (c ^ 2) ha hb

Premises used: not_fermat_42
-- Module: Mathlib.NumberTheory.FLT.Four
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
rw : HPow.hPow (β := ℕ) c 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) c 2) 2
⊢ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) c 2) 2

Tactic:
rw [heq]
-- Module: Mathlib.NumberTheory.FLT.Four
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 (β := ℕ) c 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) c 2) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
inl : ∀ (hdvd : 4 ∣ n), FermatLastTheoremFor n
inr : ∀ (p : ℕ) (hpprime : Nat.Prime p) (hdvd : p ∣ n) (hpodd : Odd p), FermatLastTheoremFor n
⊢ FermatLastTheoremFor n

Tactic:
obtain hdvd | ⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h

Premises used: Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
inl : FermatLastTheoremWith ℕ 4
⊢ FermatLastTheoremFor n

Tactic:
apply FermatLastTheoremWith.mono hdvd

Premises used: FermatLastTheoremWith.mono
-- Module: Mathlib.NumberTheory.FLT.Four
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
inr : FermatLastTheoremWith ℕ p
⊢ FermatLastTheoremFor n

Tactic:
apply FermatLastTheoremWith.mono hdvd

Premises used: FermatLastTheoremWith.mono
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremWith ℕ 4

Tactic:
fermatLastTheoremFour

Premises used: fermatLastTheoremFour, FermatLastTheoremFor
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremWith ℕ 4

Tactic:
exact fermatLastTheoremFour

Premises used: fermatLastTheoremFour
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ FermatLastTheoremWith ℕ p

Tactic:
hprimes p hpprime hpodd

Premises used: FermatLastTheoremFor
-- Module: Mathlib.NumberTheory.FLT.Four
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
⊢ FermatLastTheoremWith ℕ p

Tactic:
exact hprimes p hpprime hpodd
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
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
⊢ a * b ≠ 0

Tactic:
have ab_nz := mul_ne_zero ha hb
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
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
⊢ a * b * c ≠ 0

Tactic:
have abc_nz := mul_ne_zero ab_nz hc
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
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
abc_nz : a * b * c ≠ 0
⊢ let abc_dr := divRadical (a * b * c);
  abc_dr ∣ w

Tactic:
set abc_dr := divRadical (a * b * c)

Premises used: HMul.hMul, EuclideanDomain.divRadical
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
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 ≤ w.natDegree

Tactic:
Polynomial.natDegree_le_of_dvd abc_dr_dvd_w hw

Premises used: Polynomial.natDegree_le_of_dvd
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
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
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
⊢ w.natDegree < a.natDegree + b.natDegree

Tactic:
rw [wab] at hw ⊢
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
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
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree

Tactic:
natDegree_wronskian_lt_add hw

Premises used: Polynomial.natDegree_wronskian_lt_add
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c w : k[X]
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
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree

Tactic:
exact natDegree_wronskian_lt_add hw

Premises used: Polynomial.natDegree_wronskian_lt_add
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
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_dvd_w₁ : w.natDegree < a.natDegree + b.natDegree
⊢ abc_dr.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

Premises used: Polynomial.natDegree_le_of_dvd, Polynomial.natDegree
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
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

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
-- Module: Mathlib.NumberTheory.FLT.MasonStothers
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
set :
  let abc_r := radical (a * b * c);
  c.natDegree + 1 ≤ abc_r.natDegree
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
set abc_r := radical (a * b * c)

Premises used: HMul.hMul, UniqueFactorizationMonoid.radical