How can I prove properties of Cartesian products in Lean?

Stream: new members

[Andrew Lubrino]

I'm trying to prove the below goal:

section

  open set

  -- Proof Designer Suggested Problems - 46

  variables {U : Type}
  variables A B C : set U

  example : A × (B ∩ C) = (A × B) ∩ (A × C) := sorry

end

When I type this goal into Lean, it gives me the below error:

type mismatch at application
  ⁇ ∩ (↥A × ↥C)
term
  ↥A × ↥C
has type
  Type : Type 1
but is expected to have type
  set U : Type

I've looked in Theorem Proving in Lean, Logic and Proof in Lean, and the mathlib docs, but I wasn't able to find anything that would allow me to prove properties of Cartesian products. Can someone point me in the right direction?

[Kevin Buzzard]

You are using the wrong kind of product, that's the problem.

[Kevin Buzzard]

× is product of types, not product of subsets. I'm pretty sure that there are products of subsets somewhere; let's try docs#set.prod

[Kevin Buzzard]

Aah, according to docs#set.mem_prod you should be using ×ˢ

[Andrew Lubrino]

Awesome, thanks for the reply. When I type if I replace all my \times by \x, I'm still getting an error. How do I type the x with the small s above?

[Andrew Lubrino]

I got it and it's working. Thank you!

[Yaël Dillies]

Type \tim\^s

[Julian Berman]

Andrew Lubrino said:

Awesome, thanks for the reply. When I type if I replace all my \times by \x, I'm still getting an error. How do I type the x with the small s above?

It's also helpful to know VSCode will tell you what Yaël shared -- if you paste the symbol into your file and then hold your mouse over it it will say: Type × using \x or \times or \multiplication and Type ˢ using \^s

[Yaël Dillies]

Note however that VScode won't tell you the smallest number of characters to get away with.

[Yaël Dillies]

I learned them through sweat and blood I tried \t, \ti, \tim and oh! it works

[Andrew Lubrino]

oh man, I've been using Lean in the web editor this entire time and just downloading and uploading files back when I want to stop or continue working. Maybe I should really switch to using VS code if there really is some benefit to doing so.

[Yaël Dillies]

Yes please, for your own sake!

[Kevin Buzzard]

There are many many benefits to doing so! Not least that you can just do stuff like #check set.mem_prod and then right click on it and jump to definition and then you're right there in mathlib and can see all the API for set products. Follow instructions here https://leanprover-community.github.io/get_started.html to install Lean and the community tools, and then make a new project and open it with VS Code.

[Andrew Lubrino]

Haha, I'm sold. I'm going to switch over this morning. Thanks!

[Eric Wieser]

Kevin Buzzard said:

Furthermore you didn't need to start a new thread to discuss this -- it's just as easy to resurrect an old thread, and more convenient too.

I merged together the three threads