a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ False
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ a ^ 4 + b ^ 4 ≠ c ^ 4
intro heq
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ a ^ 4 + b ^ 4 = (c ^ 2) ^ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ False
apply @not_fermat_42 _ _ (c ^ 2) ha hb
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ c ^ 4 = (c ^ 2) ^ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ a ^ 4 + b ^ 4 = (c ^ 2) ^ 2
rw [heq]
no goals
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ c ^ 4 = (c ^ 2) ^ 2
ring