awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
h₁ : 0 < HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) a 2) 2 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) b 2) 2
⊢ 0 < HPow.hPow (β := ℕ) c 2

Tactic:
rw [← h.2.2, (by ring : a ^ 4 + b ^ 4 = (a ^ 2) ^ 2 + (b ^ 2) ^ 2)]

Premises used: And.right
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
⊢ 0 < HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) a 2) 2 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) b 2) 2

Tactic:
add_pos (sq_pos_of_ne_zero (pow_ne_zero 2 h.1)) (sq_pos_of_ne_zero (pow_ne_zero 2 h.2.1))

Premises used: add_pos, pow_ne_zero, And.right, And.left, sq_pos_of_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
⊢ 0 < HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) a 2) 2 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) b 2) 2

Tactic:
exact
    add_pos (sq_pos_of_ne_zero (pow_ne_zero 2 h.1)) (sq_pos_of_ne_zero (pow_ne_zero 2 h.2.1))

Premises used: add_pos, pow_ne_zero, And.right, And.left, sq_pos_of_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
h₁ : c.natAbs ∈ S
⊢ S.Nonempty

Tactic:
use Int.natAbs c

Premises used: Int.natAbs
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
h₁ : ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ c.natAbs = s.2.2.natAbs
⊢ c.natAbs ∈ S

Tactic:
rw [Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
w : ℤ × ℤ × ℤ
h₁ : Fermat42 (a, b, c).1 (a, b, c).2.1 (a, b, c).2.2 ∧ c.natAbs = (a, b, c).2.2.natAbs
⊢ ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ c.natAbs = s.2.2.natAbs

Tactic:
use ⟨a, ⟨b, c⟩⟩
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
⊢ S.Nonempty

Tactic:
have S_nonempty : S.Nonempty := by
    use Int.natAbs c
    rw [Set.mem_setOf_eq]
    use ⟨a, ⟨b, c⟩⟩
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find (p := Membership.mem S) S_nonempty
⊢ m ∈ S

Tactic:
have m_mem : m ∈ S := Nat.find_spec S_nonempty
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find (p := Membership.mem S) S_nonempty
m_mem : m ∈ S
rcases :
  ∀ (s0 : ℤ × ℤ × ℤ) (hs0 : Fermat42 s0.1 s0.2.1 s0.2.2) (hs1 : m = s0.2.2.natAbs),
    ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0

Tactic:
rcases m_mem with ⟨s0, hs0, hs1⟩
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find (p := Membership.mem S) S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
right : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0

Tactic:
use s0.1, s0.2.1, s0.2.2, hs0

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find (p := Membership.mem S) S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
right : m ≤ c1.natAbs
⊢ s0.2.2.natAbs ≤ c1.natAbs

Tactic:
rw [← hs1]
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find (p := Membership.mem S) S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
right : c1.natAbs ∈ S
⊢ m ≤ c1.natAbs

Tactic:
apply Nat.find_min'

Premises used: Nat.find_min'
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find (p := Membership.mem S) S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
w : ℤ × ℤ × ℤ
h₁ : Fermat42 (a1, b1, c1).1 (a1, b1, c1).2.1 (a1, b1, c1).2.2 ∧ c1.natAbs = (a1, b1, c1).2.2.natAbs
⊢ c1.natAbs ∈ S

Tactic:
use ⟨a1, ⟨b1, c1⟩⟩
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
let let₁ let₂ : ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
let₃ let₄ :
  let S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs};
  ∀ (S_nonempty : S.Nonempty), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
let₅ :
  let S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs};
  ∀ (S_nonempty : S.Nonempty),
    let m := Nat.find (p := Membership.mem S) S_nonempty;
    ∀ (m_mem : m ∈ S), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
let₆ :
  let S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs};
  ∀ (S_nonempty : S.Nonempty),
    let m := Nat.find (p := Membership.mem S) S_nonempty;
    ∀ (s0 : ℤ × ℤ × ℤ) (hs0 : Fermat42 s0.1 s0.2.1 s0.2.2) (hs1 : m = s0.2.2.natAbs),
      ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
right right₁ :
  let S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs};
  ∀ (S_nonempty : S.Nonempty),
    let m := Nat.find (p := Membership.mem S) S_nonempty;
    ∀ (s0 : ℤ × ℤ × ℤ) (hs0 : Fermat42 s0.1 s0.2.1 s0.2.2) (hs1 : m = s0.2.2.natAbs) (a1 b1 c1 : ℤ)
      (h1 : Fermat42 a1 b1 c1), s0.2.2.natAbs ≤ c1.natAbs
right₂ :
  let S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs};
  ∀ (S_nonempty : S.Nonempty),
    let m := Nat.find (p := Membership.mem S) S_nonempty;
    ∀ (s0 : ℤ × ℤ × ℤ) (hs0 : Fermat42 s0.1 s0.2.1 s0.2.2) (hs1 : m = s0.2.2.natAbs) (a1 b1 c1 : ℤ)
      (h1 : Fermat42 a1 b1 c1), m ≤ c1.natAbs
right₃ :
  let S : Set ℕ := {n : ℕ | ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs};
  ∀ (S_nonempty : S.Nonempty),
    let m := Nat.find (p := Membership.mem S) S_nonempty;
    ∀ (s0 : ℤ × ℤ × ℤ) (hs0 : Fermat42 s0.1 s0.2.1 s0.2.2) (hs1 : m = s0.2.2.natAbs) (a1 b1 c1 : ℤ)
      (h1 : Fermat42 a1 b1 c1), c1.natAbs ∈ S
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0

Tactic:
classical
  let S : Set ℕ := { n | ∃ s : ℤ × ℤ × ℤ, Fermat42 s.1 s.2.1 s.2.2 ∧ n = Int.natAbs s.2.2 }
  have S_nonempty : S.Nonempty := by
    use Int.natAbs c
    rw [Set.mem_setOf_eq]
    use ⟨a, ⟨b, c⟩⟩
  let m : ℕ := Nat.find S_nonempty
  have m_mem : m ∈ S := Nat.find_spec S_nonempty
  rcases m_mem with ⟨s0, hs0, hs1⟩
  use s0.1, s0.2.1, s0.2.2, hs0
  intro a1 b1 c1 h1
  rw [← hs1]
  apply Nat.find_min'
  use ⟨a1, ⟨b1, c1⟩⟩

Premises used: Nat.find_min'
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Minimal a b c
apply : a.gcd b = 1
⊢ IsCoprime a b

Tactic:
apply Int.isCoprime_iff_gcd_eq_one.mpr

Premises used: Iff.mpr, Int.isCoprime_iff_gcd_eq_one
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Minimal a b c
by_contra : ∀ (hab : ¬a.gcd b = 1), False
⊢ a.gcd b = 1

Tactic:
by_contra hab
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Minimal a b c
hab : ¬a.gcd b = 1
obtain : ∀ (p : ℕ) (hp : Nat.Prime p) (hpa : p ∣ a.natAbs) (hpb : p ∣ b.natAbs), False
⊢ False

Tactic:
obtain ⟨p, hp, hpa, hpb⟩ := Nat.Prime.not_coprime_iff_dvd.mp hab

Premises used: Iff.mp, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Minimal a b c
hab : ¬a.gcd b = 1
p : ℕ
hp : Nat.Prime p
hpa : p ∣ a.natAbs
hpb : p ∣ b.natAbs
obtain :
  ∀ (a1 : ℤ) (h : Minimal ((↑p : ℤ) * a1) b c) (hab : ¬((↑p : ℤ) * a1).gcd b = 1) (hpa : p ∣ ((↑p : ℤ) * a1).natAbs),
    False
⊢ False

Tactic:
obtain ⟨a1, rfl⟩ := Int.natCast_dvd.mpr hpa

Premises used: Iff.mpr, Int.natCast_dvd, rfl
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
b c : ℤ
p : ℕ
hp : Nat.Prime p
hpb : p ∣ b.natAbs
a1 : ℤ
h : Minimal ((↑p : ℤ) * a1) b c
hab : ¬((↑p : ℤ) * a1).gcd b = 1
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
obtain :
  ∀ (b1 : ℤ) (hpb : p ∣ ((↑p : ℤ) * b1).natAbs) (h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) c)
    (hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1), False
⊢ False

Tactic:
obtain ⟨b1, rfl⟩ := Int.natCast_dvd.mpr hpb

Premises used: Iff.mpr, Int.natCast_dvd, rfl
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) c
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
rw :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2) 2 ∣
    HPow.hPow (β := ℕ) ((↑p : ℤ) * a1) 4 + HPow.hPow (β := ℕ) ((↑p : ℤ) * b1) 4
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ c

Tactic:
rw [← Int.pow_dvd_pow_iff two_ne_zero, ← h.1.2.2]

Premises used: Int.pow_dvd_pow_iff, two_ne_zero, And.right, And.left
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) c
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
apply :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2) 2 * (HPow.hPow (β := ℕ) a1 4 + HPow.hPow (β := ℕ) b1 4) =
    HPow.hPow (β := ℕ) ((↑p : ℤ) * a1) 4 + HPow.hPow (β := ℕ) ((↑p : ℤ) * b1) 4
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2) 2 ∣
    HPow.hPow (β := ℕ) ((↑p : ℤ) * a1) 4 + HPow.hPow (β := ℕ) ((↑p : ℤ) * b1) 4

Tactic:
apply Dvd.intro (a1 ^ 4 + b1 ^ 4)

Premises used: Dvd.intro, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) c
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2) 2 * (HPow.hPow (β := ℕ) a1 4 + HPow.hPow (β := ℕ) b1 4) =
    HPow.hPow (β := ℕ) ((↑p : ℤ) * a1) 4 + HPow.hPow (β := ℕ) ((↑p : ℤ) * b1) 4

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) c
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ c

Tactic:
have hpc : (p : ℤ) ^ 2 ∣ c := by
    rw [← Int.pow_dvd_pow_iff two_ne_zero, ← h.1.2.2]
    apply Dvd.intro (a1 ^ 4 + b1 ^ 4)
    ring
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) c
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
hpc : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ c
obtain : ∀ (c1 : ℤ) (h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1)), False
⊢ False

Tactic:
obtain ⟨c1, rfl⟩ := hpc

Premises used: rfl
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
c1 : ℤ
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1)
⊢ Fermat42 a1 b1 c1

Tactic:
have hf : Fermat42 a1 b1 c1 :=
    (Fermat42.mul (Int.natCast_ne_zero.mpr (Nat.Prime.ne_zero hp))).mpr h.1
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
c1 : ℤ
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1)
hf : Fermat42 a1 b1 c1
apply : c1.natAbs < (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1).natAbs
⊢ False

Tactic:
apply Nat.le_lt_asymm (h.2 _ _ _ hf)

Premises used: Nat.le_lt_asymm, And.right
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
c1 : ℤ
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1)
hf : Fermat42 a1 b1 c1
rw : 1 < HPow.hPow (β := ℕ) p 2
rw₁ : 0 < c1.natAbs
⊢ c1.natAbs < (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1).natAbs

Tactic:
rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_natCast]

Premises used: Int.natAbs_mul, Int.natAbs_pow, lt_mul_iff_one_lt_left, Int.natAbs_natCast
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
c1 : ℤ
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 1 < HPow.hPow (β := ℕ) p 2

Tactic:
Nat.one_lt_pow two_ne_zero (Nat.Prime.one_lt hp)

Premises used: Nat.one_lt_pow, Nat.Prime.one_lt, two_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
c1 : ℤ
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 1 < HPow.hPow (β := ℕ) p 2

Tactic:
exact Nat.one_lt_pow two_ne_zero (Nat.Prime.one_lt hp)

Premises used: Nat.one_lt_pow, Nat.Prime.one_lt, two_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
c1 : ℤ
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < c1.natAbs

Tactic:
Nat.pos_of_ne_zero (Int.natAbs_ne_zero.2 (ne_zero hf))

Premises used: Iff.mpr, Fermat42.ne_zero, Nat.pos_of_ne_zero, Int.natAbs_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ ((↑p : ℤ) * a1).natAbs
b1 : ℤ
hpb : p ∣ ((↑p : ℤ) * b1).natAbs
hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1
c1 : ℤ
h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < c1.natAbs

Tactic:
exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero.2 (ne_zero hf))

Premises used: Iff.mpr, Fermat42.ne_zero, Nat.pos_of_ne_zero, Int.natAbs_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
⊢ Minimal a b c → Minimal b a c

Tactic:
fun ⟨h1, h2⟩ =>
  ⟨Fermat42.comm.mp h1, h2⟩

Premises used: Fermat42.comm, And.intro, Iff.mp, Fermat42.Minimal, _private.0.Fermat42.minimal_comm.match_1
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
left : Fermat42 a b (-c)
right : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs
⊢ Minimal a b (-c)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
apply : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) (-c) 2
⊢ Fermat42 a b (-c)

Tactic:
apply And.intro ha (And.intro hb _)

Premises used: And.intro
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
rw : HPow.hPow (β := ℕ) c 2 = HPow.hPow (β := ℕ) (-c) 2
⊢ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) (-c) 2

Tactic:
rw [heq]
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
⊢ HPow.hPow (β := ℕ) c 2 = HPow.hPow (β := ℕ) (-c) 2

Tactic:
(neg_sq c).symm

Premises used: neg_sq, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
⊢ HPow.hPow (β := ℕ) c 2 = HPow.hPow (β := ℕ) (-c) 2

Tactic:
exact (neg_sq c).symm

Premises used: neg_sq, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
right right₁ right₂ right₃ : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs

Tactic:
rwa [Int.natAbs_neg c]

Premises used: Int.natAbs_neg
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
obtain : ∀ (a0 b0 c0 : ℤ) (hf : Minimal a0 b0 c0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
obtain ⟨a0, b0, c0, hf⟩ := exists_minimal h

Premises used: Fermat42.exists_minimal
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
inl : ∀ (hap : a0 % 2 = 0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
inr : ∀ (hap : a0 % 2 = 1), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
rcases Int.emod_two_eq_zero_or_one a0 with hap | hap

Premises used: Int.emod_two_eq_zero_or_one
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
inl : ∀ (hbp : b0 % 2 = 0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
inl₁ : ∀ (hbp : b0 % 2 = 1), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
rcases Int.emod_two_eq_zero_or_one b0 with hbp | hbp

Premises used: Int.emod_two_eq_zero_or_one
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
inl : False
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
⊢ Dvd.dvd (α := ℤ) 2 (↑(a0.gcd b0) : ℤ)

Tactic:
have h1 : 2 ∣ (Int.gcd a0 b0 : ℤ) :=
        Int.dvd_coe_gcd (Int.dvd_of_emod_eq_zero hap) (Int.dvd_of_emod_eq_zero hbp)
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
h1 : Dvd.dvd (α := ℤ) 2 (↑(a0.gcd b0) : ℤ)
⊢ Dvd.dvd (α := ℤ) 2 (↑1 : ℤ)

Tactic:
rw [Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal hf)] at h1

Premises used: Int.isCoprime_iff_gcd_eq_one, Iff.mp, Fermat42.coprime_of_minimal
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
h1 : Dvd.dvd (α := ℤ) 2 (↑1 : ℤ)
inl : ∀ (h1 : Dvd.dvd (α := ℤ) 2 (↑1 : ℤ)), False
⊢ False

Tactic:
revert h1
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
⊢ ∀ (h1 : Dvd.dvd (α := ℤ) 2 (↑1 : ℤ)), False

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 1
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
⟨b0, ⟨a0, ⟨c0, minimal_comm hf, hbp⟩⟩⟩

Premises used: Fermat42.minimal_comm, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 1
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
exact ⟨b0, ⟨a0, ⟨c0, minimal_comm hf, hbp⟩⟩⟩
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 1
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
⟨a0, ⟨b0, ⟨c0, hf, hap⟩⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 1
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
exact ⟨a0, ⟨b0, ⟨c0, hf, hap⟩⟩⟩
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
obtain :
  ∀ (a0 b0 c0 : ℤ) (hf : Minimal a0 b0 c0) (hc : a0 % 2 = 1),
    ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
obtain ⟨a0, b0, c0, hf, hc⟩ := exists_odd_minimal h

Premises used: Fermat42.exists_odd_minimal
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
inl : ∀ (h1 : 0 < c0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
inr : ∀ (h1 : 0 = c0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
inr₁ : ∀ (h1 : c0 < 0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
rcases lt_trichotomy 0 c0 with (h1 | h1 | h1)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 < c0
w w₁ w₂ : ℤ
h₁ : Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
use a0, b0, c0
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
inr : False
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ False

Tactic:
ne_zero hf.1 h1.symm

Premises used: Fermat42.ne_zero, And.left, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ False

Tactic:
exact ne_zero hf.1 h1.symm

Premises used: Fermat42.ne_zero, And.left, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
right : 0 < -c0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
use a0, b0, -c0, neg_of_minimal hf, hc

Premises used: Fermat42.neg_of_minimal
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ 0 < -c0

Tactic:
neg_pos.mpr h1

Premises used: Iff.mpr, neg_pos
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ 0 < -c0

Tactic:
exact neg_pos.mpr h1

Premises used: Iff.mpr, neg_pos
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
r s : ℤ
h2 : IsCoprime s r
rw : IsCoprime (r * r + s * s) r
⊢ IsCoprime (HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2) r

Tactic:
rw [sq, sq]

Premises used: sq
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (r * r + s * s) r

Tactic:
(IsCoprime.mul_left h2 h2).mul_add_left_left r

Premises used: IsCoprime.mul_left, IsCoprime.mul_add_left_left