Proof by Contradiction

Stream: new members

[Mohammed]

I am new to Lean, so I am very inexperienced with all the specific tactics we could use to prove things.
Currently I am trying to prove this:

$$x = 4 \Rightarrow x * (x * x) - x * x * 5 - (x + x) = -24$$

I plan to use contradiction, since I think that's the quickest route, but I can't seem to figure it out.
This is part of a larger proof (bijection), but I have already solved for the opposite direction.

[Daniel Weber]

Do you have a #mwe?

[Julian Berman]

Can you perhaps write out the statement you're trying to prove in Lean, rather than LaTeX? Besides making it a bit easier for others to help, it also can help make precise things like "what type is x in what you want to prove"?

[Ruben Van de Velde]

rintro rfl; norm_num should do it

[Daniel Weber]

Why do you want to do a proof by contradiction? Is something wrong with

example (x : Int) : x = 4 → x * (x * x) - x * x * 5 - (x + x) = -24 := by
  intro a
  rw [a]
  rfl

[Mohammed]

@Daniel Weber Since it's part of a larger proof, I think I can write something out but I'm not sure if it'll be entirely accurate.

example (x : ℝ) (h1 : x * (x * x) - x * x * 5 - (x + x) = -24): x = 4 := by sorry

This should be a replication of where I am at in the proof.
(The previous steps separated the iff into both directions.)

[Daniel Weber]

Ah, that's the opposite of the direction you've written in LaTeX

[Mohammed]

Oh my apologies, I didn't realize.

[Daniel Weber]

In any case, that's not true - x could also be 3, for instance

[Mohammed]

Yes it could be -2, 3 or 4.

[Edward van de Meent]

or even -2

[Daniel Weber]

theorem factor (x : ℝ) : x * (x * x) - x * x * 5 - (x + x) = (x + 2) * (x - 3) * (x - 4) - 24 := by ring

example (x : ℝ) (h1 : x * (x * x) - x * x * 5 - (x + x) = -24) : x = -2 ∨ x = 3 ∨ x = 4 := by
  simpa [factor, sub_eq_zero, add_eq_zero_iff_eq_neg, or_assoc] using h1

[Mohammed]

Thank you, I will try it out.

[Mohammed]

Is it normal to come up with a theorem for a specific proof? I usually always try to keep my proofs within the example/indentation level for superficial reasons.

[Daniel Weber]

You can also do

import Mathlib

example (x : ℝ) (h1 : x * (x * x) - x * x * 5 - (x + x) = -24) : x = -2 ∨ x = 3 ∨ x = 4 := by
  have factor : x * (x * x) - x * x * 5 - (x + x) = (x + 2) * (x - 3) * (x - 4) - 24 := by ring
  simpa [factor, sub_eq_zero, add_eq_zero_iff_eq_neg, or_assoc] using h1

if you prefer

[Mohammed]

Thanks, I haven't used have before so I will use this as an example.
Although these solutions worked, I would like to know how they are applied in Lean? I have tried to go through the line but it is not very human readable.

[Ruben Van de Velde]

The point is that you "manually" factor the expression, and then simpa uses mul_eq_zero to go from (x - a)(x - b) = 0 to x - a = 0 \or x - b = 0 and then sub_eq_zero to get to x = a \or x = b

[Mohammed]

Okay I see now, thank you Ruben.

[Mohammed]

I cannot mark this as completed, I must complete the rest of my proofs after a short break.
Thank you to everyone who assisted me.