help

Stream: lean4

[kctron sub]

someone pls help me on discord with my little lean problems. My discord is DiamondJinxMain#1729 please add me. I could pay you too

[Henrik Böving]

Just ask here, nobody needs to be paid to help you here, unless its an academic assignment in which case you will have even less success here than on Discord most likely

[kctron sub]

can you help me are you good at solving problems

[kctron sub]

it is not for school or anything

[Henrik Böving]

Again, what is your issue?

[kctron sub]

solving problems in general i dont know how to go about it. here is an example:

section
variable A : Type
variable f : A → A
variable P : A → Prop
variable h : ∀x, P x → P (f x)

example : ∀y, P y → P (f (f y)) :=

sorry
end

[Mario Carneiro]

You should give some more context. (also #backticks) Have you looked at #tpil ? This covers a lot of the basics for how to write proof terms in lean.

[Mario Carneiro]

Do you understand the problem statement? Do know how to solve the problem informally? Do you know the syntax for writing proofs?

[kctron sub]

nope nope nope

[kctron sub]

sum1 add me on discord so i can screenshare my problems
DiamondJinxMain#1729

[Mario Carneiro]

I encourage you to start with #tpil then

[Mario Carneiro]

or the natural number game

[Mario Carneiro]

This is a good place to get help on specific questions, but if you need a tutorial from scratch then you are better off trying a book like #tpil and coming back once you get stuck on something

[Notification Bot]

This topic was moved to #new members > help by Mario Carneiro.