-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem Complex.integral_comp_pi_polarCoord_symm {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] (f : (ι → ℂ) → E) :
    (∫ p in (Set.univ.pi fun _ : ι ↦ Complex.polarCoord.target),
      (∏ i, (p i).1) • f (fun i ↦ Complex.polarCoord.symm (p i))) = ∫ p, f p

Proof state:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℂ) → E
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 : ι, (p i).1) • f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫ (x : ι → ℝ × ℝ), f fun i => measurableEquivRealProd.symm (x i) ∂volume

Tactic:
exact integral_comp_pi_polarCoord_symm (f ∘ e)

Result:
no goals

Proof state:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℂ) → E
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 : ι, (p i).1) • f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫ (p : ι → ℂ), f p

Tactic:
rw [← MeasurePreserving.integral_comp this e.measurableEmbedding f]

Result:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℂ) → E
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 : ι, (p i).1) • f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫ (x : ι → ℝ × ℝ), f fun i => measurableEquivRealProd.symm (x i) ∂volume

Proof state:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℂ) → E
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x => measurableEquivRealProd.symm
⊢ (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, (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 ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℂ) → E
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 : ι, (p i).1) • f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫ (p : ι → ℂ), f p

Proof state:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℂ) → E
⊢ (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, (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 ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℂ) → E
e : (ι → ℝ × ℝ) ≃ᵐ (ι → ℂ) := MeasurableEquiv.piCongrRight fun x => measurableEquivRealProd.symm
⊢ (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i : ι, (p i).1) • f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫ (p : ι → ℂ), f p