where to ask for code error?

Stream: new members

[Bo Qin]

where do I ask question why my code shows error even if it looks fine? Maybe I'm using the wrong tactics? I'm new to using lean

[Bo Qin]

lean_learning_error.png

[Bo Qin]

Can you do

(x + 3) / (x + 3)

as by ring?

[Bo Qin]

is it because of possibility of being 0?

[Bo Qin]

that's probably it

[Ruben Van de Velde]

ring isn't expected to handle division; field_simp might help

[Damiano Testa]

Also, you are right about 0 being special-cased: a / a can be equal to 0, when a = 0.

[Daniel Weber]

polyrith would probably also work here

[Daniel Weber]

import Mathlib.Tactic

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 := by
  polyrith says linear_combination (-(1 / 2 * y) + 1) * h1 + -1 * h2 / 2