Is there a way to "name" the arguments to a theorem?

Stream: new members

[kvanvels]

I am trying prove the following (rather trivial) statement. Let $A$ and $B$ be sets. Then the sets $A\setminus B$, $A\cap B$, and $B\setminus A$ are pairwise disjoint and their union is $A \cup B$.

If I was doing this on pen and paper, I would name the sets something like $P_1 = A \setminus B$, $P_2 = A \cap B$ and $P_3 = B\setminus A$. And show that $P_1\cap P_2 = \emptyset$, $P_1\cap P_3 = \emptyset$, $P_2\cap P_3 = \emptyset$ and $P_1\cup P_2\cup P_3 = A\cup B$. Is there a way to do this (name the arguments in this way) in lean? Is there a tactic/best practice of which I should know about regarding disjoint sets?

I appreciate any help and direction.

[Yaël Dillies]

docs#tactic.interactive.set is what you want if you're talking about naming the sets within the proofs. If you want to name the sets within the statement, you will instead need let bindings.

[kvanvels]

Thank you, I will follow up if I have more questions.