-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem measurePreserving_piUnique {π : ι → Type*} [Unique ι] {m : ∀ i, MeasurableSpace (π i)}
    (μ : ∀ i, Measure (π i)) :
    MeasurePreserving (MeasurableEquiv.piUnique π) (Measure.pi μ) (μ default) where
  measurable := (MeasurableEquiv.piUnique π).measurable
  map_eq

Proof state:
case h.h.e_6.h
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
s : Set ((i : ι) → π i)
⊢ eval default '' s = ⇑e.symm ⁻¹' s

Tactic:
exact e.toEquiv.image_eq_preimage s

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
⊢ Measure.map (⇑(MeasurableEquiv.piUnique π)) (Measure.pi μ) = μ default

Tactic:
set e := MeasurableEquiv.piUnique π

Result:
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
⊢ Measure.map (⇑e) (Measure.pi μ) = μ default

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
this : (piPremeasure fun i => (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))
⊢ Measure.map (⇑e) (Measure.pi μ) = μ default

Tactic:
simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
  toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
⊢ (piPremeasure fun i => (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))

Tactic:
ext1 s

Result:
case h
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
s : Set ((i : ι) → π i)
⊢ piPremeasure (fun i => (μ i).toOuterMeasure) s = (Measure.map (⇑e.symm) (μ default)) s

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
⊢ Measure.map (⇑e) (Measure.pi μ) = μ default

Tactic:
have : (piPremeasure fun i => (μ i).toOuterMeasure) = Measure.map e.symm (μ default) := by
  ext1 s
  rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply, coe_toOuterMeasure]
  congr 1; exact e.toEquiv.image_eq_preimage s

Result:
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
this : (piPremeasure fun i => (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))
⊢ Measure.map (⇑e) (Measure.pi μ) = μ default

Proof state:
case h
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
s : Set ((i : ι) → π i)
⊢ (μ default) (eval default '' s) = (μ default) (⇑e.symm ⁻¹' s)

Tactic:
congr 1

Result:
case h.h.e_6.h
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
s : Set ((i : ι) → π i)
⊢ eval default '' s = ⇑e.symm ⁻¹' s

Proof state:
case h
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
s : Set ((i : ι) → π i)
⊢ piPremeasure (fun i => (μ i).toOuterMeasure) s = (Measure.map (⇑e.symm) (μ default)) s

Tactic:
rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply, coe_toOuterMeasure]

Result:
case h
ι : Type u_1
inst✝¹ : Fintype ι
π : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (π i)
μ : (i : ι) → Measure (π i)
e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π
s : Set ((i : ι) → π i)
⊢ (μ default) (eval default '' s) = (μ default) (⇑e.symm ⁻¹' s)