-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem Complex.lintegral_comp_pi_polarCoord_symm (f : (ι → ℂ) → ℝ≥0∞) :
    ∫⁻ p in (Set.univ.pi fun _ : ι ↦ Complex.polarCoord.target),
      (∏ i, .ofReal (p i).1) * f (fun i ↦ Complex.polarCoord.symm (p i)) = ∫⁻ p, f p

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℂ), f p

Tactic:
let e := MeasurableEquiv.piCongrRight (fun _ : ι ↦ measurableEquivRealProd.symm)

Result:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x => measurableEquivRealProd.symm
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℂ), f p

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x => measurableEquivRealProd.symm
this : MeasurePreserving (fun a i => measurableEquivRealProd.symm (a i)) volume volume
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℂ), f p

Tactic:
rw [← MeasurePreserving.lintegral_comp_emb this e.measurableEmbedding]

Result:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x => measurableEquivRealProd.symm
this : MeasurePreserving (fun a i => measurableEquivRealProd.symm (a i)) volume volume
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (a : ι → ℝ × ℝ), f fun i => measurableEquivRealProd.symm (a i) ∂volume

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x => measurableEquivRealProd.symm
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℂ), f p

Tactic:
have := volume_preserving_pi (fun _ : ι ↦ Complex.volume_preserving_equiv_real_prod.symm)

Result:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x => measurableEquivRealProd.symm
this : MeasurePreserving (fun a i => measurableEquivRealProd.symm (a i)) volume volume
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℂ), f p

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x => measurableEquivRealProd.symm
this : MeasurePreserving (fun a i => measurableEquivRealProd.symm (a i)) volume volume
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (a : ι → ℝ × ℝ), f fun i => measurableEquivRealProd.symm (a i) ∂volume

Tactic:
exact lintegral_comp_pi_polarCoord_symm (f ∘ e)

Result:
no goals