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

Proof state:
case h.e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      (∏ i : ι, (p i).1) • f fun i => ↑polarCoord.symm (p i)) =
    ∫ (x : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      |(fderivPiPolarCoordSymm x).det| • f fun i => ↑polarCoord.symm (x i)

Tactic:
refine setIntegral_congr_fun measurableSet_pi_polarCoord_target fun x hx ↦ ?_

Result:
case h.e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x => polarCoord.target
⊢ ((∏ i : ι, (x i).1) • f fun i => ↑polarCoord.symm (x i)) =
    |(fderivPiPolarCoordSymm x).det| • f fun i => ↑polarCoord.symm (x i)

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 => polarCoord.target,
      (∏ i : ι, (p i).1) • f fun i => ↑polarCoord.symm (p i)) =
    ∫ (p : ι → ℝ × ℝ), f p

Tactic:
rw [← setIntegral_univ (f := f), ← setIntegral_congr_set pi_polarCoord_symm_target_ae_eq_univ]

Result:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      (∏ i : ι, (p i).1) • f fun i => ↑polarCoord.symm (p i)) =
    ∫ (x : ι → ℝ × ℝ) in (Pi.map fun x => ↑polarCoord.symm) '' Set.univ.pi fun x => polarCoord.target, f x

Proof state:
case h.e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x => polarCoord.target
⊢ ((∏ i : ι, (x i).1) • f fun i => ↑polarCoord.symm (x i)) =
    |(fderivPiPolarCoordSymm x).det| • f fun i => ↑polarCoord.symm (x i)

Tactic:
simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, abs_fst_of_mem_pi_polarCoord_target hx]

Result:
no goals

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 => polarCoord.target,
      (∏ i : ι, (p i).1) • f fun i => ↑polarCoord.symm (p i)) =
    ∫ (x : ι → ℝ × ℝ) in (Pi.map fun x => ↑polarCoord.symm) '' Set.univ.pi fun x => polarCoord.target, f x

Tactic:
convert (integral_image_eq_integral_abs_det_fderiv_smul volume measurableSet_pi_polarCoord_target
  (fun p _ ↦ (hasFDerivAt_pi_polarCoord_symm p).hasFDerivWithinAt)
    injOn_pi_polarCoord_symm f).symm using 1

Result:
case h.e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      (∏ i : ι, (p i).1) • f fun i => ↑polarCoord.symm (p i)) =
    ∫ (x : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      |(fderivPiPolarCoordSymm x).det| • f fun i => ↑polarCoord.symm (x i)