second degree equation

Stream: maths

[Diego Cerrillo]

Hello! I am new to Lean. To try and learn a bit more on the language, I am trying to demonstrate the 2nd degree equation solution.
For the second step, I need to multiply 4*a to both sides.
I am trying to use the mul_left_cancel lemma, but it does not work and I do not understand the error.
Thank you very much!

import data.real.basic
import data.real.sqrt

noncomputable theory

theorem demo (a b c : ℝ)(x : ℝ)(h1: x = (-b + real.sqrt(b*b - 4*a*c))/(2*a)) :
 a*x^2 + b*x + c = 0:=
  begin
    rw add_eq_zero_iff_eq_neg,
    rw ←mul_left_cancel (a * x ^ 2 + b * x) (-c) (4*a),
    sorry

  end

[Diego Cerrillo]

poly-real.lean:10:8
type mismatch at application
mul_left_cancel (a * x ^ 2 + b * x)
term
a * x ^ 2 + b * x
has type
ℝ : Type
but is expected to have type
?m_3 * ?m_4 = ?m_3 * ?m_5 : Prop
state:
a b c x : ℝ,
h1 : x = (-b + real.sqrt (b * b - 4 * a * c)) / (2 * a)
⊢ a * x ^ 2 + b * x = -c

[Riccardo Brasca]

You can use #backticks even for the error, it will be more readable. Looking at docs#mul_left_cancel you can see that the first argument must be an equality (the one you want to simplify), and this is what the error is saying.

[Riccardo Brasca]

But for ℝ it will not work, since ℝ is not a group under multiplication.

[Riccardo Brasca]

You have to use docs#mul_left_cancel₀

[Kevin Buzzard]

Can we do something about this docs# bug? Riccardo means docs#mul_left_cancel₀

[Kevin Buzzard]

The line you want next is apply mul_left_cancel₀ (show 4*a ≠ 0, from _),, but you have not assumed $4a\not=0$ so Lean throws it in as an extra goal. Your theorem is false in general e.g. if a=b=0 and c=1. Lean is completely happy to do things like real.sqrt (-1) (and it will return a real number), or 1 / 0 (and again it will return a real number). Lean works using a "garbage in, garbage out" procedure, so if you don't put in these hypotheses it will happily return things which you can't prove anything about (all you know is that real.sqrt(-1) is a real number, you don't know which one it is, and all theorems about real.sqrt x have 0 <= x as a hypothesis so you can't apply them to real.sqrt (-1)).

[Diego Cerrillo]

Thanks! Did not notice that