awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
let let₁ let₂ : ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have 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 : ℤ),
    Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs
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⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
⊢ IsCoprime a b
have apply : a.gcd b = 1
Tactic: apply Int.isCoprime_iff_gcd_eq_one.mpr
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
⊢ a.gcd b = 1
have by_contra : ∀ (hab : ¬a.gcd b = 1), False
Tactic: by_contra hab
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Minimal a b c
hab : ¬a.gcd b = 1
⊢ False
have obtain : ∀ (p : ℕ) (hp : Nat.Prime p) (hpa : p ∣ a.natAbs) (hpb : p ∣ b.natAbs), False
Tactic: obtain ⟨p, hp, hpa, hpb⟩ := Nat.Prime.not_coprime_iff_dvd.mp hab
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ False
have obtain : ∀ (a1 : ℤ) (h : Minimal ((↑p : ℤ) * a1) b c) (hab : ¬((↑p : ℤ) * a1).gcd b = 1) (hpa : p ∣ ((↑p : ℤ) * a1).natAbs),
  False
Tactic: obtain ⟨a1, rfl⟩ := Int.natCast_dvd.mpr hpa
Cleared hypotheses: a, h, hab, hpa
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ False
have obtain : ∀ (b1 : ℤ) (hpb : p ∣ ((↑p : ℤ) * b1).natAbs) (h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) c)
  (hab : ¬((↑p : ℤ) * a1).gcd ((↑p : ℤ) * b1) = 1), False
Tactic: obtain ⟨b1, rfl⟩ := Int.natCast_dvd.mpr hpb
Cleared hypotheses: b, hpb, h, hab
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
have rw : HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2) 2 ∣
  HPow.hPow (β := ℕ) ((↑p : ℤ) * a1) 4 + HPow.hPow (β := ℕ) ((↑p : ℤ) * b1) 4
Tactic: rw [← Int.pow_dvd_pow_iff two_ne_zero, ← h.1.2.2]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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 (β := ℕ) ((↑p : ℤ) * a1) 4 + HPow.hPow (β := ℕ) ((↑p : ℤ) * b1) 4
have 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
Tactic: apply Dvd.intro (a1 ^ 4 + b1 ^ 4)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
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
⊢ False
have hpc : 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
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ False
have obtain : ∀ (c1 : ℤ) (h : Minimal ((↑p : ℤ) * a1) ((↑p : ℤ) * b1) (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1)), False
Tactic: obtain ⟨c1, rfl⟩ := hpc
Cleared hypotheses: c, h, hpc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
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)
⊢ False
have hf : 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
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ False
have apply : c1.natAbs < (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1).natAbs
Tactic: apply Nat.le_lt_asymm (h.2 _ _ _ hf)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ c1.natAbs < (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1).natAbs
have rw : 1 < HPow.hPow (β := ℕ) p 2
Tactic: rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ c1.natAbs < (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 * c1).natAbs
have rw₁ : 0 < c1.natAbs
Tactic: rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ Minimal a b (-c)
have left : Fermat42 a b (-c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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)
⊢ Minimal a b (-c)
have right : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ Fermat42 a b (-c)
have apply : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) (-c) 2
Tactic: apply And.intro ha (And.intro hb _)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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 (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) (-c) 2
have rw : HPow.hPow (β := ℕ) c 2 = HPow.hPow (β := ℕ) (-c) 2
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
have obtain : ∀ (a0 b0 c0 : ℤ) (hf : Minimal a0 b0 c0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
Tactic: obtain ⟨a0, b0, c0, hf⟩ := exists_minimal h
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
have inl : ∀ (hap : a0 % 2 = 0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
Tactic: rcases Int.emod_two_eq_zero_or_one a0 with hap | hap
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
have inr : ∀ (hap : 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
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
have inl : ∀ (hbp : b0 % 2 = 0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
Tactic: rcases Int.emod_two_eq_zero_or_one b0 with hbp | hbp
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
have inl₁ : ∀ (hbp : b0 % 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
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
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
⊢ False
have h1 : 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)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
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) : ℤ)
⊢ False
have h1₁ : Dvd.dvd (α := ℤ) 2 (↑1 : ℤ)
Tactic: rw [Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal hf)] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
have inl : ∀ (h1 : Dvd.dvd (α := ℤ) 2 (↑1 : ℤ)), False
Tactic: revert h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
have 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
Tactic: obtain ⟨a0, b0, c0, hf, hc⟩ := exists_odd_minimal h
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
have inl : ∀ (h1 : 0 < c0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
Tactic: rcases lt_trichotomy 0 c0 with (h1 | h1 | h1)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
have inr : ∀ (h1 : 0 = c0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
Tactic: rcases lt_trichotomy 0 c0 with (h1 | h1 | h1)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
have inr₁ : ∀ (h1 : c0 < 0), ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
Tactic: rcases lt_trichotomy 0 c0 with (h1 | h1 | h1)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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₂ : ℤ
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
have h₁ : Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
Tactic: use a0, b0, c0
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
have right : 0 < -c0
Tactic: use a0, b0, -c0, neg_of_minimal hf, hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2) r
have rw : IsCoprime (r * r + s * s) r
Tactic: rw [sq, sq]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2) (r * s)
have apply : IsCoprime (HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2) s
Tactic: apply IsCoprime.mul_right (Int.isCoprime_of_sq_sum (isCoprime_comm.mp h))
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2) s
have rw : IsCoprime (HPow.hPow (β := ℕ) s 2 + HPow.hPow (β := ℕ) r 2) s
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
⊢ False
have ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
Tactic: have ht : PythagoreanTriple (a ^ 2) (b ^ 2) c := by
    delta PythagoreanTriple
    linear_combination h.1.2.2
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
Goal:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (HPow.hPow (β := ℕ) a 2) (HPow.hPow (β := ℕ) b 2) c
⊢ False
have h2 : (HPow.hPow (β := ℕ) a 2).gcd (HPow.hPow (β := ℕ) b 2) = 1
Tactic: have h2 : Int.gcd (a ^ 2) (b ^ 2) = 1 :=
    Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal h).pow