Theorem: descent1left (Flt/Euler.lean)

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]
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

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]
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

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

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

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

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)
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

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

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, _, _, _⟩
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

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]
State after:
no goals

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]
State after:
no goals

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

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]
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

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
State after:
no goals

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

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]
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

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
State after:
no goals

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

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

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)
State after:
no goals

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

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

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
State after:
no goals

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
State after:
no goals

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)
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

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

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 : ℤ
hznu : z ∈ nonunits ℤ
hzp : z ∣ p
hzq : z ∣ q
⊢ False
Tactic:
apply hznu
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
⊢ IsUnit z

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 : ℤ
hznu : z ∈ nonunits ℤ
hzp : z ∣ p
hzq : z ∣ q
⊢ IsUnit z
Tactic:
exact hbccoprime.isUnit_of_dvd' (dvd_sub hzq hzp) (dvd_add hzp hzq)
State after:
no goals

State before:
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
Tactic:
constructor <;> intro H <;> simpa [H, parity_simps] using hc
State after:
no goals

State before:
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
Tactic:
rw [eq_sub_of_add_eq h]
State after:
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) = (p + q) ^ 3 - (q - p) ^ 3

State before:
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) = (p + q) ^ 3 - (q - p) ^ 3
Tactic:
ring
State after:
no goals