refine MeasurePreserving.trans (measurePreserving_piEquivPiSubtypeProd _ _) ?_
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving
    ⇑((piEquivPiSubtypeProd (fun j => α j) fun j => j = i).trans
        (prodCongr (piUnique fun i_1 => α ↑i_1) (refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1))))
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(prodCongr (piUnique fun i_1 => α ↑i_1) (refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1)))