Proofs

Stream: new members

[Mo Kakari]

w3.lean Hey can someone with a better understanding of lean, help me out with these please?

[Mo Kakari]

hey can anyone with more experience using lean, help me out with these proofs? w3.lean

[Jakub Kądziołka]

Is it just me, or does this look like homework? Also why did you double-post?
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Proofs/near/275035109

[Mo Kakari]

sorry i've never used zulipchat before, and yea it is homework but i have absolutely no idea where to start.

[Notification Bot]

A message was moved here from #general > Proofs by Kyle Miller.

[Notification Bot]

This topic was moved here from #lean4 > Proofs by Kyle Miller.

[Jakub Kądziołka]

Did they not teach you anything about Lean before assigning this homework?

[Mo Kakari]

He gave us a 20 min run down and a pdf textbook to read through. But it's about as confusing as his 20 minute breakdown on the topic.

[Kevin Buzzard]

I'm not sure I'm going to do your homework, so I'm going to give you the canonical stackexchange-like response instead: what have you tried so far?

[Jakub Kądziołka]

Don't be afraid to try things and experiment. Also, if anything in particular is unclear, you can ask here for clarification.

[Arthur Paulino]

@Mo Kakari do you know how to prove those informally (with pen and paper)?
If you do, you can ask "how do I say ... in Lean"?

[Mo Kakari]

@Arthur Paulino Yea I can prove them with pen and paper. Do you mean ask that in here? or phrase it like that on google?

[Arthur Paulino]

Ask here on Zulip. I am sure the community will gladly guide you through the process of learning how to use tactics to do what you mean on pen and paper

[Kevin Buzzard]

Ask a better question. Don't just ask "how do I do all my homework", that question stinks for all sorts of reasons. Take one of the questions in your homework. Try to solve it. Show some effort on your part because if you can't be bothered why should we be bothered? The point of the homework is to teach you something. Get a #mwe working (read the link) with just one question and your attempt at a solution. Don't upload code, I can't even see it on mobile. Post code between #backticks . Make an effort. This community has standards.

[Arthur Paulino]

Be warned, though, that you might be surprised with the level of precision that's required for this kind of work. So, as Kevin said, it will definitely require some effort on your part

[Kevin Buzzard]

I'm also teaching a Lean course right now. I make videos for my students. I see the first of your questions are about sets. here are the videos I made when I was teaching sets.

[Mo Kakari]

@Arthur Paulino @Kevin Buzzard you guys are awesome, thank you for showing me a better way. this community is wholesome, ive only been here for like 6 hours.