Fill in SetTheory.Set.iProd_equiv_pi

[gaearon]

Since this isn't a part of the book, let's fill it in. It's a bit hard to guess how to produce an element satisfying ↑(Set.univ.pi fun i ↦ {x | x ∈ X i}) anyway.

I haven't filled other equivalences because the text is a bit ambiguous on whether they're all "why" or not.

[gaearon]

Unrelated but this one is computable (maybe the only one?)

For example:

abbrev SetTheory.Set.empty_iProd_equiv (X: (∅:Set) → Set) : iProd X ≃ Unit where
  toFun := fun t ↦ ()
  invFun := fun x ↦ ⟨tuple fun e ↦ False.elim (not_mem_empty _ e.property), by apply tuple_mem_iProd⟩
  left_inv := by
    intro t
    have h := (mem_iProd _).mp t.property
    obtain ⟨x, ht⟩ := h
    ext
    rw [ht, tuple_inj]
    ext e
    have := not_mem_empty e
    contradiction
  right_inv := by
    intro
    simp

Not included because the book has a "why" seemingly for a related question: