## Stream: new members

### Topic: mathematics in Lean: sets

#### Alexandre Rademaker (Oct 13 2020 at 13:55):

example : s ∩ t = t ∩ s :=
subset.antisymm sorry sorry


The book asks to complete the proof term! I was able to complete using two begin/end  blocks but I am not sure if it counts as a solution or a pure proof term must be provided. Anyway, I am blocked by the error in

example : s ∩ t = t ∩ s :=
subset.antisymm (λ x h1, and.intro h1.2 h1.1) sorry


From the previous comment at the beginning of the chapter, it seems that we can't have a solution in proof term?

Due to a quirk of how Lean processes its input, the first example fails if we replace theorem foo with example.

#### Johan Commelin (Oct 13 2020 at 14:05):

example {α : Type} (s t : set α) : s ∩ t = t ∩ s :=
subset.antisymm (λ x h1, and.intro (and.right h1) (and.left h1))
sorry


#### Alexandre Rademaker (Oct 13 2020 at 14:08):

I just found out that

example : s ∩ t = t ∩ s :=
subset.antisymm
(λ x ⟨hs, ht⟩, and.intro ht hs)
sorry


also works. I wonder if we have any explicit way to deconstruct the set.mem

Last updated: May 15 2021 at 23:13 UTC