simp [prodCongr]
ι : 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)))
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving
    ⇑{
        toEquiv :=
          Equiv.prodCongr (piUnique fun i_1 => α ↑i_1).toEquiv (Equiv.refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1)),
        measurable_toFun :=
          (_ :
            Measurable
              ⇑(Equiv.prodCongr (piUnique fun i_1 => α ↑i_1).toEquiv
                  (Equiv.refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1)))),
        measurable_invFun :=
          (_ :
            Measurable
              ⇑(Equiv.prodCongr (piUnique fun i_1 => α ↑i_1).toEquiv
                    (Equiv.refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1))).symm) }