Which exercise does iProd_equiv_tuples correspond to?

Stream: Analysis I

[Dan Abramov]

Asking about this equivalence:

noncomputable abbrev SetTheory.Set.iProd_equiv_tuples (n:ℕ) (X: Fin n → Set) :
    iProd X ≃ { t:Tuple n // ∀ i, (t.x i:Object) ∈ X i } where

I assume it's considered part of Exercise 3.5.2 — is that correct?

Would it be accurate to say it corresponds to this part?

Screenshot 2025-08-12 at 00.56.54.png

If yes, is the book's suggestion to rely on Exercise 3.4.7 (SetTheory.Set.partial_functions) still relevant here? Or is the reader meant to follow a different approach?

For reference, my solution, which does not use partial_functions, (but is very similar to @Rado Kirov's) ended up being:

noncomputable abbrev SetTheory.Set.iProd_equiv_tuples (n:ℕ) (X: Fin n → Set) :
    iProd X ≃ { t:Tuple n // ∀ i, (t.x i:Object) ∈ X i } where
  toFun := fun t ↦
    let hx := (mem_iProd _).mp t.property
    let x := hx.choose
    ⟨{
      X := iUnion _ fun i ↦ {((x i): Object)},
      x := fun i ↦ ⟨x i, by rw [mem_iUnion]; use i; simp⟩,
      surj := by
        rintro ⟨o, ho⟩
        rw [mem_iUnion] at ho
        obtain ⟨i, hi⟩ := ho
        rw [mem_singleton] at hi
        subst hi
        use i
    }, by intro i; use (x i).property⟩
  invFun := fun t ↦
    let x := fun i ↦ (⟨t.val.x i, t.property i⟩: X i)
    ⟨tuple x, by rw [mem_iProd]; use x⟩
  left_inv := by
    intro t
    let hx := (mem_iProd _).mp t.property
    simp [←hx.choose_spec]
  right_inv := by
    intro ⟨t, _⟩
    ext xi
    · simp only [mem_iUnion, mem_singleton]
      generalize_proofs hx
      have := hx.choose_spec
      rw [tuple_inj] at this
      simp only [←this]
      obtain ⟨x, hx⟩ := hx
      constructor
      · rintro ⟨i, rfl⟩
        use (t.x i).property
      intro hxi
      obtain ⟨i, hi⟩ := t.surj ⟨xi, hxi⟩
      use i
      rw [hi]
    dsimp only []
    generalize_proofs hx
    have := hx.choose_spec
    rw [tuple_inj] at this
    rw [←this]

Thanks!

[Terence Tao]

Not exactly; the Lean implementation of Definition 3.5.6 already gives iProd X the type of Set, and in general it's a bit hard to directly translate "show that something is indeed a set" into a strongly typed language, short of asking the reader to supply a definition that type-checks. But that definition used a different notion of a tuple than the one used in Exercise 3.5.2, so I instead added this exercise to demonstrate compatibility (but within Mathlib's framework of set theory and equivalences, rather than try to embed this new version of a tuple and product inside the Chapter 3 set theory (which one could also do, but I feel it more important to transition towards Mathlib's set theory at this point)).