rw [piSplitAt_toEquiv]
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : (j : ι) → MeasurableSpace (α j)
x : α i × ((j : { j // j ≠ i }) → α ↑j)
⊢ (piSplitAt α i).symm x = (Equiv.piSplitAt i α).symm x
no goals