internlm/Lean-Github huggingface dataset:
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
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
set d := Int.gcd a b with 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 : ℕ := a.gcd b
hd' : d = a.gcd b
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' 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 : ℕ := a.gcd b
hd' : d = a.gcd b
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
obtain ⟨A, HA⟩ : ↑d ∣ a := @Int.gcd_dvd_left a b
Proof state after:
case 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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Theorem: exists_coprime
Proof state before:
case 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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
obtain ⟨B, HB⟩ : ↑d ∣ b := @Int.gcd_dvd_right a b
Proof state after:
case 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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Theorem: exists_coprime
Proof state before:
case 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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
obtain ⟨C, HC⟩ : ↑d ∣ c :=
  by
  rw [← Int.pow_dvd_pow_iff hn.ne', ← h, HA, HB, mul_pow, mul_pow, ← mul_add]
  exact dvd_mul_right _ _
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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
have hdpos : 0 < d := Int.gcd_pos_of_ne_zero_left _ ha'
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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
have hd := Int.natCast_ne_zero_iff_pos.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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
have hsoln : A ^ n + B ^ n = C ^ n :=
  by
  apply Int.eq_of_mul_eq_mul_left (pow_ne_zero n hd)
  simp only [mul_add, ← mul_pow, ← HA, ← HB, ← HC, h]
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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
have hsoln' : B ^ n + A ^ n = C ^ n := by rwa [add_comm] at hsoln
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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
have hcoprime : IsCoprime A B :=
  by
  rw [← Int.gcd_eq_one_iff_coprime]
  apply Nat.eq_of_mul_eq_mul_left hdpos
  rw [← Int.natAbs_ofNat d, ← Int.gcd_mul_left, ← HA, ← HB, hd', Int.natAbs_ofNat, mul_one]
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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c'
Tactic:
have HA' : A.natAbs ≤ a.natAbs := by
  rw [HA]
  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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
HC' : C.natAbs ≤ c.natAbs
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
HC' : C.natAbs ≤ c.natAbs
⊢ ∃ a' b' c', a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ 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 : ℕ := a.gcd b
hd' : d = a.gcd b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ↑d ∣ c
Tactic:
rw [← Int.pow_dvd_pow_iff hn.ne', ← 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 : ℕ := a.gcd b
hd' : d = a.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ A.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ A.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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 * A.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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 * A.gcd 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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ A.natAbs ≤ a.natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ A.natAbs ≤ (↑d * A).natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ A.natAbs ≤ (↑d * A).natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ A.natAbs ≤ d * A.natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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
⊢ A.natAbs ≤ d * A.natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
⊢ B.natAbs ≤ b.natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
⊢ B.natAbs ≤ (↑d * B).natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
⊢ B.natAbs ≤ (↑d * B).natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
⊢ B.natAbs ≤ d * B.natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
⊢ B.natAbs ≤ d * B.natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
⊢ C.natAbs ≤ c.natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
⊢ C.natAbs ≤ (↑d * C).natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
⊢ C.natAbs ≤ (↑d * C).natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
⊢ C.natAbs ≤ d * C.natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
⊢ C.natAbs ≤ d * C.natAbs
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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
HC' : C.natAbs ≤ c.natAbs
⊢ ?m.4102 * 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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
HC' : C.natAbs ≤ c.natAbs
⊢ ?m.4206 * 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 : ℕ := a.gcd b
hd' : d = a.gcd 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' : A.natAbs ≤ a.natAbs
HB' : B.natAbs ≤ b.natAbs
HC' : C.natAbs ≤ c.natAbs
⊢ ?m.4243 * C ≠ 0
Tactic:
rwa [HC] at hc'
Proof state after:
no goals
Theorem: descent1a
Proof state before:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
have contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False :=
  by
  intro x y hcoprime hx hy
  rw [even_iff_two_dvd] at hx hy
  have := Int.isUnit_eq_one_or (hcoprime.isUnit_of_dvd' hx hy)
  norm_num at this
Proof state after:
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
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c