internlm/Lean-Github huggingface dataset:
Theorem: exists_coprime
Proof state before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have HB' : B.natAbs ≤ b.natAbs := by
  rw [HB]
  simp only [Int.natAbs_ofNat, Int.natAbs_mul]
  exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
Proof state after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Theorem: exists_coprime
Proof state before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have HC' : C.natAbs ≤ c.natAbs := by
  rw [HC]
  simp only [Int.natAbs_ofNat, Int.natAbs_mul]
  exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
Proof state after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Theorem: exists_coprime
Proof state before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
exact
  ⟨A, B, C, HA', HB', HC',
    ⟨right_ne_zero_of_mul (by rwa [HA] at ha'), right_ne_zero_of_mul (by rwa [HB] at hb'),
      right_ne_zero_of_mul (by rwa [HC] at hc'), hsoln⟩,
    hcoprime, coprime_add_self_pow hn hsoln hcoprime,
    coprime_add_self_pow hn hsoln' hcoprime.symm⟩
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ↑d ∣ c
Tactic:
rw [← Int.pow_dvd_pow_iff hn, ← h, HA, HB, mul_pow, mul_pow, ← mul_add]
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ↑d ^ n ∣ ↑d ^ n * (A ^ n + B ^ n)
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ↑d ^ n ∣ ↑d ^ n * (A ^ n + B ^ n)
Tactic:
exact dvd_mul_right _ _
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ A ^ n + B ^ n = C ^ n
Tactic:
apply Int.eq_of_mul_eq_mul_left (pow_ne_zero n hd)
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ ↑d ^ n * (A ^ n + B ^ n) = ↑d ^ n * C ^ n
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ ↑d ^ n * (A ^ n + B ^ n) = ↑d ^ n * C ^ n
Tactic:
simp only [mul_add, ← mul_pow, ← HA, ← HB, ← HC, h]
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
⊢ B ^ n + A ^ n = C ^ n
Tactic:
rwa [add_comm] at hsoln
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ IsCoprime A B
Tactic:
rw [← Int.gcd_eq_one_iff_coprime]
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ Int.gcd A B = 1
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ Int.gcd A B = 1
Tactic:
apply Nat.eq_of_mul_eq_mul_left hdpos
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ d * Int.gcd A B = d * 1
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ d * Int.gcd A B = d * 1
Tactic:
rw [← Int.natAbs_ofNat d, ← Int.gcd_mul_left, ← HA, ← HB, hd', Int.natAbs_ofNat, mul_one]
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.natAbs a
Tactic:
rw [HA]
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.natAbs (↑d * A)
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.natAbs (↑d * A)
Tactic:
simp only [Int.natAbs_ofNat, Int.natAbs_mul]
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.gcd a b * Int.natAbs A
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.gcd a b * Int.natAbs A
Tactic:
exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.natAbs b
Tactic:
rw [HB]
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.natAbs (↑d * B)
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.natAbs (↑d * B)
Tactic:
simp only [Int.natAbs_ofNat, Int.natAbs_mul]
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.gcd a b * Int.natAbs B
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.gcd a b * Int.natAbs B
Tactic:
exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.natAbs c
Tactic:
rw [HC]
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.natAbs (↑d * C)
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.natAbs (↑d * C)
Tactic:
simp only [Int.natAbs_ofNat, Int.natAbs_mul]
Proof state after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.gcd a b * Int.natAbs C
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.gcd a b * Int.natAbs C
Tactic:
exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ?m.4410 * A ≠ 0
Tactic:
rwa [HA] at ha'
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ?m.4476 * B ≠ 0
Tactic:
rwa [HB] at hb'
Proof state after:
no goals
Theorem: exists_coprime
Proof state before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ?m.4512 * C ≠ 0
Tactic:
rwa [HC] at hc'
Proof state after:
no goals
Theorem: descent1a
Proof state before:
case neg
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
exfalso
Proof state after:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ False
Theorem: descent1a
Proof state before:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ False
Tactic:
apply hcparity
Proof state after:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ Even c
Theorem: descent1a
Proof state before:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ Even c
Tactic:
rw [← Int.even_pow' three_ne_zero, ← h]
Proof state after:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ Even (a ^ 3 + b ^ 3)
Theorem: descent1a
Proof state before:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ Even (a ^ 3 + b ^ 3)
Tactic:
simp [haparity, hbparity, three_ne_zero, parity_simps]
Proof state after:
no goals
Theorem: flt_not_add_self
Proof state before:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ False
Tactic:
obtain ⟨d, rfl⟩ : a ∣ c :=
  by
  rw [← Int.pow_dvd_pow_iff (by norm_num : 0 < 3), ← h]
  apply dvd_mul_right
Proof state after:
case intro
a : ℤ
ha : a ≠ 0
d : ℤ
h : a ^ 3 * 2 = (a * d) ^ 3
⊢ False
Theorem: flt_not_add_self
Proof state before:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ a ∣ c
Tactic:
rw [← Int.pow_dvd_pow_iff (by norm_num : 0 < 3), ← h]
Proof state after:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ a ^ 3 ∣ a ^ 3 * 2
Theorem: flt_not_add_self
Proof state before:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: descent1left
Proof state before:
case intro.intro
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Tactic:
have hqnezero : q ≠ 0 := by
  rintro rfl
  rw [zero_sub, add_zero, Odd.neg_pow (by norm_num), ← sub_eq_add_neg, sub_eq_iff_eq_add] at h
  exact flt_not_add_self hpnezero h.symm rfl
Proof state after:
case intro.intro
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Theorem: descent1left
Proof state before:
a : ℤ
hapos : a ≠ 0
p : ℤ
hpnezero : p ≠ 0
hc : ¬Even (p + 0)
hb : ¬Even (0 - p)
h : a ^ 3 + (0 - p) ^ 3 = (p + 0) ^ 3
hbccoprime : IsCoprime (0 - p) (p + 0)
hp : p + 0 - (0 - p) = 2 * p
hq : p + 0 + (0 - p) = 2 * 0
⊢ False
Tactic:
rw [zero_sub, add_zero, Odd.neg_pow (by norm_num), ← sub_eq_add_neg, sub_eq_iff_eq_add] at h
Proof state after:
a : ℤ
hapos : a ≠ 0
p : ℤ
hpnezero : p ≠ 0
hc : ¬Even (p + 0)
hb : ¬Even (0 - p)
h : a ^ 3 = p ^ 3 + p ^ 3
hbccoprime : IsCoprime (0 - p) (p + 0)
hp : p + 0 - (0 - p) = 2 * p
hq : p + 0 + (0 - p) = 2 * 0
⊢ False
Theorem: descent1left
Proof state before:
a : ℤ
hapos : a ≠ 0
p : ℤ
hpnezero : p ≠ 0
hc : ¬Even (p + 0)
hb : ¬Even (0 - p)
h : a ^ 3 + (-p) ^ 3 = p ^ 3
hbccoprime : IsCoprime (0 - p) (p + 0)
hp : p + 0 - (0 - p) = 2 * p
hq : p + 0 + (0 - p) = 2 * 0
⊢ Odd 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: descent1left
Proof state before:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ IsCoprime p q
Tactic:
apply isCoprime_of_dvd _ _ (not_and_of_not_left _ hpnezero)
Proof state after:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ ∀ (z : ℤ), z ∈ nonunits ℤ → z ≠ 0 → z ∣ p → ¬z ∣ q
Theorem: descent1left
Proof state before:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ ∀ (z : ℤ), z ∈ nonunits ℤ → z ≠ 0 → z ∣ p → ¬z ∣ q
Tactic:
rintro z hznu - hzp hzq
Proof state after:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
z : ℤ
hznu : z ∈ nonunits ℤ
hzp : z ∣ p
hzq : z ∣ q
⊢ False
Theorem: descent2
Proof state before:
a b c : ℤ
h : FltCoprime 3 a b c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
                2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) ∧
              Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
Tactic:
obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube⟩ := descent1 a b c h
Proof state after:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
                2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) ∧
              Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
                2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) ∧
              Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)
Tactic:
refine' ⟨p, q, hp, hq, hcoprime, hodd, hcube, _⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)