Zulip Chat Archive

Stream: mathlib4

Topic: A problem with lean

tsuki hao (Jul 14 2023 at 07:37):

屏幕截图-2023-07-14-153631.png
Can someone tell me how to prove the third theorem using the first two self-written theorems

Floris van Doorn (Jul 14 2023 at 07:41):

Is your first type supposed to be ℝ and the remaining two R?

Floris van Doorn (Jul 14 2023 at 07:42):

You should be able to write either/all of exact (add_right_inj a).mp h or simp at h; exact h or simpa at h.

Floris van Doorn (Jul 14 2023 at 07:43):

And in ℝ the tactic linarith would also work

tsuki hao (Jul 14 2023 at 07:51):

Floris van Doorn said:

Is your first type supposed to be ℝ and the remaining two R?

Thank you for the reminder, I have a problem with R, and I have successfully solved this problem with your reminder

tsuki hao (Jul 14 2023 at 07:54):

image.png
Does anyone know why there is an error in add_zero here?

Johan Commelin (Jul 14 2023 at 07:56):

It is a lot easier for us if you paste your code directly using #backticks (read this link for an explanation)

Johan Commelin (Jul 14 2023 at 07:57):

My guess is that the error is there because there is nothing of the form _ + 0 in your goal at that point.

Notification Bot (Jul 14 2023 at 08:00):

This topic was moved here from #lean4 > A problem with lean by Floris van Doorn.

tsuki hao (Jul 14 2023 at 08:08):

Johan Commelin said:

It is a lot easier for us if you paste your code directly using #backticks (read this link for an explanation)

Thank you for reminding! I also managed to find my bug!

Last updated: Dec 20 2023 at 11:08 UTC