-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem measurePreserving_pi {ι : Type*} [Fintype ι] {α : ι → Type v} {β : ι → Type*}
    [∀ i, MeasurableSpace (α i)] [∀ i, MeasurableSpace (β i)]
    (μ : (i : ι) → Measure (α i)) (ν : (i : ι) → Measure (β i))
    {f : (i : ι) → (α i) → (β i)} [∀ i, SigmaFinite (ν i)]
    (hf : ∀ i, MeasurePreserving (f i) (μ i) (ν i)) :
    MeasurePreserving (fun a i ↦ f i (a i)) (Measure.pi μ) (Measure.pi ν) where
  measurable :=
    measurable_pi_iff.mpr <| fun i ↦ (hf i).measurable.comp (measurable_pi_apply i)
  map_eq

Proof state:
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
⊢ Measure.map (fun a i => f i (a i)) (Measure.pi μ) = Measure.pi ν

Tactic:
haveI : ∀ i, SigmaFinite (μ i) := fun i ↦ (hf i).sigmaFinite

Result:
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ Measure.map (fun a i => f i (a i)) (Measure.pi μ) = Measure.pi ν

Proof state:
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ Measure.map (fun a i => f i (a i)) (Measure.pi μ) = Measure.pi ν

Tactic:
refine (Measure.pi_eq fun s hs ↦ ?_).symm

Result:
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (β i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.map (fun a i => f i (a i)) (Measure.pi μ)) (univ.pi s) = ∏ i : ι, (ν i) (s i)

Proof state:
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (β i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i : ι, (μ i) (f i ⁻¹' s i) = ∏ i : ι, (ν i) (s i)

Tactic:
simp_rw [← MeasurePreserving.measure_preimage (hf _) (hs _).nullMeasurableSet]

Result:
no goals

Proof state:
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (β i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.map (fun a i => f i (a i)) (Measure.pi μ)) (univ.pi s) = ∏ i : ι, (ν i) (s i)

Tactic:
rw [Measure.map_apply, Set.preimage_pi, Measure.pi_pi]

Result:
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (β i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i : ι, (μ i) (f i ⁻¹' s i) = ∏ i : ι, (ν i) (s i)

case hf
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (β i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable fun a i => f i (a i)

case hs
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (β i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (univ.pi s)

Proof state:
case hf
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (β i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable fun a i => f i (a i)

Tactic:
exact measurable_pi_iff.mpr <| fun i ↦ (hf i).measurable.comp (measurable_pi_apply i)

Result:
no goals

Proof state:
case hs
ι : Type u_4
inst✝³ : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝² : (i : ι) → MeasurableSpace (α i)
inst✝¹ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (β i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (univ.pi s)

Tactic:
exact MeasurableSet.univ_pi hs

Result:
no goals