awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
c : ℤ
hn : n ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {0, 0, c} id) 1
HF : HPow.hPow (α := ℤ) 0 n + HPow.hPow (α := ℤ) 0 n + c ^ n = 0
⊢ False
have HF₁ : c = 0
Tactic: simp only [ne_eq, hn, not_false_eq_true, zero_pow, add_zero, zero_add, pow_eq_zero_iff]
      at HF
Cleared hypotheses: HF
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ 1
have inr : p ∣ Finset.gcd {a, b, c} id
Tactic: rw [← Hgcd]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ Finset.gcd {a, b, c} id
have inr : ∀ (x : ℤ) (hx : Membership.mem (γ := Finset ℤ) {a, b, c} x), p ∣ id x
Tactic: refine Finset.dvd_gcd_iff.mpr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : Membership.mem (γ := Finset ℤ) {a, b, c} x
⊢ p ∣ id x
have hx₁ : x = a ∨ x = b ∨ x = c
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ p ∣ id x
have inr : ∀ (hx : x = a), p ∣ id x
Tactic: rcases hx with hx | hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = a ∨ x = b ∨ x = c
inr : ∀ (hx : x = a), p ∣ id x
⊢ p ∣ id x
have inr₁ : ∀ (hx : x = b), p ∣ id x
Tactic: rcases hx with hx | hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = a ∨ x = b ∨ x = c
inr : ∀ (hx : x = a), p ∣ id x
inr₁ : ∀ (hx : x = b), p ∣ id x
⊢ p ∣ id x
have inr₂ : ∀ (hx : x = c), p ∣ id x
Tactic: rcases hx with hx | hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have rw : a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mp : a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mpr : b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr :
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mp₁ : a ≠ 0 →
  b ≠ 0 →
    HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
      b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr :
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₁ mp₂ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mp₃ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr :
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₁ mp₂ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₃ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mp₄ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr :
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₁ mp₂ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₃ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
mp₄ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mp₅ : a ≠ 0 →
  b ≠ 0 →
    HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr :
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₁ mp₂ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₃ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
mp₄ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
mp₅ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mpr₁ : b ≠ 0 →
  a ≠ 0 →
    HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
      a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr :
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₁ mp₂ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₃ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
mp₄ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
mp₅ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr₁ mpr₂ :
  b ≠ 0 →
    a ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mpr₃ : b ≠ 0 → a ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr :
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₁ mp₂ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₃ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
mp₄ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
mp₅ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr₁ mpr₂ :
  b ≠ 0 →
    a ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr₃ : b ≠ 0 → a ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mpr₄ : b ≠ 0 → a ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr :
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₁ mp₂ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₃ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
mp₄ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
mp₅ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr₁ mpr₂ :
  b ≠ 0 →
    a ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr₃ : b ≠ 0 → a ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
mpr₄ : b ≠ 0 → a ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
have mpr₅ : b ≠ 0 →
  a ≠ 0 →
    HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2 ↔
    k * a ≠ 0 ∧
      k * b ≠ 0 ∧
        HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
have mp : a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2 →
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c k : ℤ
hk0 : k ≠ 0
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2 →
    k * a ≠ 0 ∧
      k * b ≠ 0 ∧
        HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2 ↔
    k * a ≠ 0 ∧
      k * b ≠ 0 ∧
        HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
have mpr : k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2 →
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
have mpr : a ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
mpr : a ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
have mpr₁ : b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
⊢ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
have mpr : b ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
mpr : b ≠ 0
⊢ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
have mpr₁ : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
⊢ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
have mpr : HPow.hPow (β := ℕ) k 4 * (HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4) =
  HPow.hPow (β := ℕ) k 4 * HPow.hPow (β := ℕ) c 2
Tactic: apply (mul_right_inj' (pow_ne_zero 4 hk0)).mp
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
⊢ c ≠ 0
have apply : HPow.hPow (β := ℕ) c 2 ≠ 0
Tactic: apply ne_zero_pow two_ne_zero _
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
⊢ HPow.hPow (β := ℕ) c 2 ≠ 0
have h₁ : 0 < HPow.hPow (β := ℕ) c 2
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
Goal:
a b c : ℤ
h : Fermat42 a b c
⊢ 0 < HPow.hPow (β := ℕ) c 2
have h₁ : 0 < HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) a 2) 2 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) b 2) 2
Tactic: rw [← h.2.2, (by ring : a ^ 4 + b ^ 4 = (a ^ 2) ^ 2 + (b ^ 2) ^ 2)]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
have h₁ : c.natAbs ∈ S
Tactic: use Int.natAbs c
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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}
⊢ c.natAbs ∈ S
have h₁ : ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ c.natAbs = s.2.2.natAbs
Tactic: rw [Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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 : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ c.natAbs = s.2.2.natAbs
have w : ℤ × ℤ × ℤ
Tactic: use ⟨a, ⟨b, c⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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 : ℤ × ℤ × ℤ
⊢ ∃ (s : ℤ × ℤ × ℤ), Fermat42 s.1 s.2.1 s.2.2 ∧ c.natAbs = s.2.2.natAbs
have h₁ : Fermat42 (a, b, c).1 (a, b, c).2.1 (a, b, c).2.2 ∧ c.natAbs = (a, b, c).2.2.natAbs
Tactic: use ⟨a, ⟨b, c⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
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}
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have S_nonempty : S.Nonempty
Tactic: have S_nonempty : S.Nonempty := by
    use Int.natAbs c
    rw [Set.mem_setOf_eq]
    use ⟨a, ⟨b, c⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (hypothesis)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have m_mem : m ∈ S
Tactic: have m_mem : m ∈ S := Nat.find_spec S_nonempty
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have 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
Tactic: rcases m_mem with ⟨s0, hs0, hs1⟩
Cleared hypotheses: m_mem
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ ∃ (a0 : ℤ) (b0 : ℤ) (c0 : ℤ), Minimal a0 b0 c0
have right : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs
Tactic: use s0.1, s0.2.1, s0.2.2, hs0
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ s0.2.2.natAbs ≤ c1.natAbs
have right : m ≤ c1.natAbs
Tactic: rw [← hs1]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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
⊢ m ≤ c1.natAbs
have right : c1.natAbs ∈ S
Tactic: apply Nat.find_min'
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Four (goal)
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 : ℤ × ℤ × ℤ
⊢ c1.natAbs ∈ S
have h₁ : Fermat42 (a1, b1, c1).1 (a1, b1, c1).2.1 (a1, b1, c1).2.2 ∧ c1.natAbs = (a1, b1, c1).2.2.natAbs
Tactic: use ⟨a1, ⟨b1, c1⟩⟩