Deciding on membership in Chapter 3

Stream: Analysis I

[Rado Kirov]

For some of the problems, we need to construct actual functions that need to do different things depending on a set membership in Chapter 3. I don't fully understand Decidable at this point, so when I get an error when writing if h: x \in X then ... else ... I just add open Classical in at the top of the example.

Here is a longer example of what I mean:

open Classical in
theorem SetTheory.Set.pow_prod_pow_EqualCard_pow_union (A B C:Set) (hd: Disjoint B C) :
    EqualCard ((A ^ B) ×ˢ (A ^ C)) (A ^ (B ∪ C)) := by
  rw [EqualCard]
  use fun p ↦ fn_to_powerset (fun bc ↦ if h: bc.val ∈ B then
    let f := Classical.choose ((powerset_axiom (fst p)).mp (fst p).property)
    f ⟨bc, h⟩
  else
    let f := Classical.choose ((powerset_axiom (snd p)).mp (snd p).property)
    f ⟨bc, by aesop⟩)

Is this recommended? Is there a better approach?