internlm/Lean-Github huggingface dataset:
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
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
Tactic:
by_cases haparity : Even a <;> by_cases hbparity : Even b <;> by_cases hcparity : Even c
Proof state after:
case pos
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

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

case pos
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

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

case pos
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

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

case pos
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

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
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
⊢ ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
Tactic:
intro x y hcoprime hx hy
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
x y : ℤ
hcoprime : IsCoprime x y
hx : Even x
hy : Even y
⊢ False
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
x y : ℤ
hcoprime : IsCoprime x y
hx : Even x
hy : Even y
⊢ False
Tactic:
rw [even_iff_two_dvd] at hx hy
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
x y : ℤ
hcoprime : IsCoprime x y
hx : 2 ∣ x
hy : 2 ∣ y
⊢ False
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
x y : ℤ
hcoprime : IsCoprime x y
hx : 2 ∣ x
hy : 2 ∣ y
⊢ False
Tactic:
have := Int.isUnit_eq_one_or (hcoprime.isUnit_of_dvd' hx hy)
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
x y : ℤ
hcoprime : IsCoprime x y
hx : 2 ∣ x
hy : 2 ∣ y
this : 2 = 1 ∨ 2 = -1
⊢ False
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
x y : ℤ
hcoprime : IsCoprime x y
hx : 2 ∣ x
hy : 2 ∣ y
this : 2 = 1 ∨ 2 = -1
⊢ False
Tactic:
norm_num at this
Proof state after:
no goals
Theorem: descent1a
Proof state before:
case pos
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:
exact False.elim (contra habcoprime ‹_› ‹_›)
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:
exact False.elim (contra habcoprime ‹_› ‹_›)
Proof state after:
no goals
Theorem: descent1a
Proof state before:
case pos
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:
exact False.elim (contra haccoprime ‹_› ‹_›)
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:
tauto
Proof state after:
no goals
Theorem: descent1a
Proof state before:
case pos
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:
exact False.elim (contra hbccoprime ‹_› ‹_›)
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:
tauto
Proof state after:
no goals
Theorem: descent1a
Proof state before:
case pos
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:
tauto
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
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
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
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
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
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
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 b c : ℤ
ha : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
⊢ a ≠ b
Tactic:
rintro rfl
Proof state after:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 + a ^ 3 = c ^ 3
⊢ False
Theorem: flt_not_add_self
Proof state before:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 + a ^ 3 = c ^ 3
⊢ False
Tactic:
rw [← mul_two] at h
Proof state after:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ False
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 : 3 ≠ 0), ← 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:
case intro
a : ℤ
ha : a ≠ 0
d : ℤ
h : a ^ 3 * 2 = (a * d) ^ 3
⊢ False
Tactic:
apply Int.two_not_cube d
Proof state after:
case intro
a : ℤ
ha : a ≠ 0
d : ℤ
h : a ^ 3 * 2 = (a * d) ^ 3
⊢ d ^ 3 = 2
Theorem: flt_not_add_self
Proof state before:
case intro
a : ℤ
ha : a ≠ 0
d : ℤ
h : a ^ 3 * 2 = (a * d) ^ 3
⊢ d ^ 3 = 2
Tactic:
rwa [mul_pow, mul_right_inj' (pow_ne_zero 3 ha), eq_comm] at h
Proof state after:
no goals
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 : 3 ≠ 0), ← 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
⊢ a ^ 3 ∣ a ^ 3 * 2
Tactic:
apply dvd_mul_right
Proof state after:
no goals
Theorem: flt_not_add_self
Proof state before:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ 3 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: descent1left
Proof state before:
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Tactic:
obtain ⟨p, hp⟩ : Even (c - b) := by simp [hb, hc, parity_simps]
Proof state after:
case intro
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = p + p
⊢ ∃ 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:
case intro
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = p + p
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Tactic:
obtain ⟨q, hq⟩ : Even (c + b) := by simp [hb, hc, parity_simps]
Proof state after:
case intro.intro
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = p + p
q : ℤ
hq : c + b = q + q
⊢ ∃ 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:
case intro.intro
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = p + p
q : ℤ
hq : c + b = q + q
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Tactic:
rw [← two_mul] at hp hq
Proof state after:
case intro.intro
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = 2 * p
q : ℤ
hq : c + b = 2 * q
⊢ ∃ 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:
case intro.intro
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = 2 * p
q : ℤ
hq : c + b = 2 * q
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Tactic:
obtain rfl : p + q = c := by
  apply Int.eq_of_mul_eq_mul_left two_ne_zero
  rw [mul_add, ← hp, ← hq]
  ring
Proof state after:
case intro.intro
a b : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ ∃ 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:
case intro.intro
a b : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Tactic:
obtain rfl : q - p = b := by
  apply Int.eq_of_mul_eq_mul_left two_ne_zero
  rw [mul_sub, ← hp, ← hq]
  ring
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
⊢ ∃ 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:
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
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Tactic:
have hpnezero : p ≠ 0 := by
  rintro rfl
  rw [sub_zero, zero_add, add_left_eq_self] at h
  exact hapos (pow_eq_zero h)
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
⊢ ∃ 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:
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; decide), ← 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:
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
Tactic:
refine' ⟨p, q, hpnezero, hqnezero, _, _, _⟩
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
⊢ IsCoprime p q

case intro.intro.refine'_2
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
⊢ Even p ↔ ¬Even q

case intro.intro.refine'_3
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
⊢ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Theorem: descent1left
Proof state before:
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
⊢ Even (c - b)
Tactic:
simp [hb, hc, parity_simps]
Proof state after:
no goals
Theorem: descent1left
Proof state before:
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = p + p
⊢ Even (c + b)
Tactic:
simp [hb, hc, parity_simps]
Proof state after:
no goals
Theorem: descent1left
Proof state before:
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = 2 * p
q : ℤ
hq : c + b = 2 * q
⊢ p + q = c
Tactic:
apply Int.eq_of_mul_eq_mul_left two_ne_zero
Proof state after:
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = 2 * p
q : ℤ
hq : c + b = 2 * q
⊢ 2 * (p + q) = 2 * c
Theorem: descent1left
Proof state before:
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = 2 * p
q : ℤ
hq : c + b = 2 * q
⊢ 2 * (p + q) = 2 * c
Tactic:
rw [mul_add, ← hp, ← hq]
Proof state after:
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = 2 * p
q : ℤ
hq : c + b = 2 * q
⊢ c - b + (c + b) = 2 * c
Theorem: descent1left
Proof state before:
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = 2 * p
q : ℤ
hq : c + b = 2 * q
⊢ c - b + (c + b) = 2 * c
Tactic:
ring
Proof state after:
no goals
Theorem: descent1left
Proof state before:
a b : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ q - p = b
Tactic:
apply Int.eq_of_mul_eq_mul_left two_ne_zero
Proof state after:
a b : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ 2 * (q - p) = 2 * b
Theorem: descent1left
Proof state before:
a b : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ 2 * (q - p) = 2 * b
Tactic:
rw [mul_sub, ← hp, ← hq]
Proof state after:
a b : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ p + q + b - (p + q - b) = 2 * b
Theorem: descent1left
Proof state before:
a b : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ p + q + b - (p + q - b) = 2 * b
Tactic:
ring
Proof state after:
no goals
Theorem: descent1left
Proof state before:
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
⊢ p ≠ 0
Tactic:
rintro rfl
Proof state after:
a : ℤ
hapos : a ≠ 0
q : ℤ
hc : ¬Even (0 + q)
hb : ¬Even (q - 0)
h : a ^ 3 + (q - 0) ^ 3 = (0 + q) ^ 3
hbccoprime : IsCoprime (q - 0) (0 + q)
hp : 0 + q - (q - 0) = 2 * 0
hq : 0 + q + (q - 0) = 2 * q
⊢ False
Theorem: descent1left
Proof state before:
a : ℤ
hapos : a ≠ 0
q : ℤ
hc : ¬Even (0 + q)
hb : ¬Even (q - 0)
h : a ^ 3 + (q - 0) ^ 3 = (0 + q) ^ 3
hbccoprime : IsCoprime (q - 0) (0 + q)
hp : 0 + q - (q - 0) = 2 * 0
hq : 0 + q + (q - 0) = 2 * q
⊢ False
Tactic:
rw [sub_zero, zero_add, add_left_eq_self] at h
Proof state after:
a : ℤ
hapos : a ≠ 0
q : ℤ
hc : ¬Even (0 + q)
hb : ¬Even (q - 0)
h : a ^ 3 = 0
hbccoprime : IsCoprime (q - 0) (0 + q)
hp : 0 + q - (q - 0) = 2 * 0
hq : 0 + q + (q - 0) = 2 * q
⊢ False
Theorem: descent1left
Proof state before:
a : ℤ
hapos : a ≠ 0
q : ℤ
hc : ¬Even (0 + q)
hb : ¬Even (q - 0)
h : a ^ 3 = 0
hbccoprime : IsCoprime (q - 0) (0 + q)
hp : 0 + q - (q - 0) = 2 * 0
hq : 0 + q + (q - 0) = 2 * q
⊢ False
Tactic:
exact hapos (pow_eq_zero h)
Proof state after:
no goals
Theorem: descent1left
Proof state before:
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
⊢ q ≠ 0
Tactic:
rintro rfl
Proof state after:
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
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; decide), ← 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
⊢ False
Tactic:
exact flt_not_add_self hpnezero h.symm rfl
Proof state after:
no goals
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:
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
⊢ ¬Even 3