mathematics in Lean: sets

Stream: new members

[Alexandre Rademaker]

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]

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

[Alexandre Rademaker]

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