Theorem: MeasurableEquiv.piSplitAt_symm_apply (ForML/PiEquiv.lean)

State before:
ι : 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
Tactic:
rw [piSplitAt_toEquiv]
State after:
no goals