Moetrash 2x

Stream: new members

[Moetrash 2x]

hi can i get some help with a couple of lean problems?

[Moetrash 2x]

if anyone is willing to help me learn and understand please DM me. Thank you!

[Eric Rodriguez]

feel free to ask in #new members!

[Moetrash 2x]

got it thank you so much!

[Moetrash 2x]

Hi can someone please guide me step by step with this problem I have really been struggling with it?

[Moetrash 2x]

import data.set
open set

-- 1. Replace "sorry" in these examples.
section
variable {U : Type}
variables A B C : set U

example : ∀ x, x ∈ A ∩ C → x ∈ A ∪ B :=
sorry

example : ∀ x, x ∈ (A ∪ B)ᶜ → x ∈ Aᶜ :=
sorry
end

[Eric Wieser]

That problem looks the same as this homework question: https://www.chegg.com/homework-help/questions-and-answers/write-code-following-proofs-using-lean-theorem-prover-import-dataset-open-set-1-replace-so-q104337641.

[Notification Bot]

4 messages were moved here from #general > Lean in the wild by Eric Wieser.

[Notification Bot]

3 messages were moved here from #new members > How to check element is in set by Eric Wieser.

[Moetrash 2x]

it is but no answer is provided :C

[Eric Wieser]

Also here from two years ago

[Eric Wieser]

Is this a problem from a course, or from a text"book" / lean tutorial?

[Moetrash 2x]

hey it is from lean textbook example problem

[Arien Malec]

On this one

example : ∀ x, x ∈ A ∩ C → x ∈ A ∪ B :=
sorry

a logical first step is to pull out the premises, which in tactics mode is done via

example : ∀ x, x ∈ A ∩ C → x ∈ A ∪ B :=
begin
   intros x h,
   sorry
end

and in term is done

example : ∀ x, x ∈ A ∩ C → x ∈ A ∪ B :=
   λ x, λ h: x ∈ A ∩ C, sorry

The actual proving is going to go from the hypothesis (that x ∈ A ∩ C) and allow you to construct the conclusion. I'd highly recommend you look at the docs for data.set.basic, particularly the theorems about intersections and unions. In general you want to use the the hypothesis to prove something the helps you construct the conclusion.

[Arien Malec]

I'm sure if you have a pen and pencil proof, or some sense for how you want the proof to go in Lean, and are struggling with syntax, you'd get plenty of help.

[Yaël Dillies]

I'm not sure that will help, @Arien Malec, those lemmas are almost all proved from lattice lemmas

[Arien Malec]

This is OP’s homework…