Theorem: flt_not_add_self (Flt/Euler.lean)

State before:
a b c : ℤ
ha : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
⊢ a ≠ b
Tactic:
rintro rfl
State after:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 + a ^ 3 = c ^ 3
⊢ False

State before:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 + a ^ 3 = c ^ 3
⊢ False
Tactic:
rw [← mul_two] at h
State after:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ False

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
State after:
case intro
a : ℤ
ha : a ≠ 0
d : ℤ
h : a ^ 3 * 2 = (a * d) ^ 3
⊢ False

State before:
case intro
a : ℤ
ha : a ≠ 0
d : ℤ
h : a ^ 3 * 2 = (a * d) ^ 3
⊢ False
Tactic:
apply Int.two_not_cube d
State after:
case intro
a : ℤ
ha : a ≠ 0
d : ℤ
h : a ^ 3 * 2 = (a * d) ^ 3
⊢ d ^ 3 = 2

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

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]
State after:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ a ^ 3 ∣ a ^ 3 * 2

State before:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ a ^ 3 ∣ a ^ 3 * 2
Tactic:
apply dvd_mul_right
State after:
no goals

State before:
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals