showing contradiction

Stream: new members

[Rohan Joshi]

Hello everyone, I had a question regarding proving a contradiction in lean4. In this scenario, I have the hypothesis h1: a^4 + b^4 = c^4 and the goal: a^4 + b^4 ≠ c^4. I tried using By.contradiction but it does not work. Any idea on how to proceed with this?

[Ruben Van de Velde]

This is not a logically correct argument

[Ruben Van de Velde]

Given a hypothesis that 1 = 1, you cannot prove that 1 \ne 1

[Edward van de Meent]

it will need to be concluded from other hypotheses.

[Bulhwi Cha]

Rohan Joshi said:

In this scenario, I have the hypothesis h1: a^4 + b^4 = c^4 and the goal: a^4 + b^4 ≠ c^4.

Is h1 the only hypothesis you have?

[Rohan Joshi]

no, I have hypotheses :
h: a^4 + b^4 = c^4 \im \exists d, a^4 + b^4 = d^2 \and abd \neq 0
h2: \exists d, a^4 + b^4 = d^2 \and abd \neq 0

[Bulhwi Cha]

Can you show us #mwe?

[Rohan Joshi]

Screenshot-2024-08-08-at-7.15.43PM.png

[Rohan Joshi]

Screenshot-2024-08-08-at-7.15.57PM.png

[Ruben Van de Velde]

Please read the page behind the link #mwe

[Rohan Joshi]

import Mathlib
namespace FLT
open Classical

theorem reduce_c_exponent_2(a b c :ℤ) (k: a*b*c ≠ 0):
a^4+b^4=c^4 → ∃ d, a^4+b^4 = d^2 ∧ a*b*d ≠ 0 := by
intro h
use c^2
have h1 : a^4 + b^4 = (c^2)^2
linarith
have h2: a*b*(c^2) ≠ 0
have h3: c ≠ 0
contrapose! k
rw[k]
apply mul_zero
rw[pow_two]
rw[← mul_assoc]
rw[mul_comm]
apply mul_ne_zero
use h3
use k
apply And.intro
exact h1
exact h2

variable (d: ℤ)
theorem fermat_for_4(a b c : ℤ):
a*b*c ≠ 0 → a^4+b^4≠ c^4:= by
intro h
apply reduce_c_exponent_2 at h
have h1: a^4 + b^4 = c^4
sorry
--------------------------------------
have h2: ∃ d, a^4+b^4 = d^2 ∧ a*b*d ≠ 0
apply h
exact h1
sorry

[Rohan Joshi]

One thing I tried was using another hypothesis:
h3: a^4 + b^4 = d^2 ∧ abd ≠ 0
but in order to prove this hypothesis, I need to get rid of the \exists d from h2. I tried using apply Exists.elim but it does not seem to work. Is there any way to work around this?
Screenshot-2024-08-08-at-7.38.35PM.png

[Edward van de Meent]

Rohan Joshi said:

import Mathlib
namespace FLT
open Classical

theorem reduce_c_exponent_2(a b c :ℤ) (k: a*b*c ≠ 0):
a^4+b^4=c^4 → ∃ d, a^4+b^4 = d^2 ∧ a*b*d ≠ 0 := by
intro h
use c^2
have h1 : a^4 + b^4 = (c^2)^2
linarith
have h2: a*b*(c^2) ≠ 0
have h3: c ≠ 0
contrapose! k
rw[k]
apply mul_zero
rw[pow_two]
rw[← mul_assoc]
rw[mul_comm]
apply mul_ne_zero
use h3
use k
apply And.intro
exact h1
exact h2

variable (d: ℤ)
theorem fermat_for_4(a b c : ℤ):
a*b*c ≠ 0 → a^4+b^4≠ c^4:= by
intro h
apply reduce_c_exponent_2 at h
have h1: a^4 + b^4 = c^4
sorry
--------------------------------------
have h2: ∃ d, a^4+b^4 = d^2 ∧ a*b*d ≠ 0
apply h
exact h1
sorry

could you maybe also remove the python from the codeblock? on zulip, it will use lean4 as default syntax higlighting. you can read more about this at #backticks.

[Edward van de Meent]

doing this will also add a link to the lean playground in the upper right corner of the code block, allowing us to open the code with one click and try and look for a fix more easily

[Rohan Joshi]

import Mathlib
namespace FLT
open Classical

theorem reduce_c_exponent_2(a b c :ℤ) (k: a*b*c ≠ 0):
a^4+b^4=c^4 → ∃ d, a^4+b^4 = d^2 ∧ a*b*d ≠ 0 := by
intro h
use c^2
have h1 : a^4 + b^4 = (c^2)^2
linarith
have h2: a*b*(c^2) ≠ 0
have h3: c ≠ 0
contrapose! k
rw[k]
apply mul_zero
rw[pow_two]
rw[← mul_assoc]
rw[mul_comm]
apply mul_ne_zero
use h3
use k
apply And.intro
exact h1
exact h2
------------------------------------------
theorem not_reduce_c_exponent_2(a b c : ℤ):
a*b*c ≠ 0 → a^4+b^4 ≠ c^2:= by
intro h
contrapose! h
sorry
-------------------------------------------
variable (d: ℤ)
theorem fermat_for_4(a b c : ℤ):
a*b*c ≠ 0 → a^4+b^4≠ c^4:= by
intro h
apply reduce_c_exponent_2 at h
have h1: a^4 + b^4 = c^4
sorry
--------------------------------------
have h2: ∃ d, a^4+b^4 = d^2 ∧ a*b*d ≠ 0
apply h
exact h1
have h3: a^4 + b^4 = d^2 ∧ a*b*d ≠ 0
apply Exists.elim at h2
sorry
---------------------------------
sorry

[Edward van de Meent]

regarding the Exists.elim, what you can do if you have a h : ∃ (d:SomeType), some_prop d is use obtain ⟨d,hd⟩ := h2, which adds d:SomeType and hd : some_prop d to the context.

[Edward van de Meent]

btw, using variable (d: ℤ) in this case is more harmful than good, because you don't want any integer d, but specifically the one you proved exists with the property you want

[Edward van de Meent]

and having multiple integers d floating around only leads to confusion

[Rohan Joshi]

i see the problem now. Thank you so much for your help! :grinning: