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

State before:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(piSplitAt α i)
Tactic:
rw [piSplitAt_eq_trans]
State after:
ι : 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))))

State before:
ι : 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))))
Tactic:
refine MeasurePreserving.trans (measurePreserving_piEquivPiSubtypeProd _ _) ?_
State after:
ι : 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)))

State before:
ι : 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)))
Tactic:
simp [prodCongr]
State after:
ι : 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) }

State before:
ι : 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) }
Tactic:
refine MeasurePreserving.prod ?_ (MeasurePreserving.id _)
State after:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(piUnique fun i_1 => α ↑i_1).toEquiv

State before:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(piUnique fun i_1 => α ↑i_1).toEquiv
Tactic:
exact measurePreserving_piUnique _
State after:
no goals