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

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (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 (lintegral_image_eq_lintegral_abs_det_fderiv_mul 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 ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (p i).1) * f fun i => ↑polarCoord.symm (p i)) =
    ∫⁻ (x : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun i => ↑polarCoord.symm (x i)

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

Tactic:
refine setLIntegral_congr_fun measurableSet_pi_polarCoord_target ?_

Result:
case h.e'_2
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ ∀ᵐ (x : ι → ℝ × ℝ),
    (x ∈ Set.univ.pi fun x => polarCoord.target) →
      ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun i => ↑polarCoord.symm (x i)) =
        ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun i => ↑polarCoord.symm (x i)

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

Tactic:
rw [← setLIntegral_univ f, ← setLIntegral_congr pi_polarCoord_symm_target_ae_eq_univ]

Result:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      (∏ i : ι, ENNReal.ofReal (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.h
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x => polarCoord.target
⊢ ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun i => ↑polarCoord.symm (x i)) =
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun i => ↑polarCoord.symm (x i)

Tactic:
simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦
  abs_nonneg _), abs_fst_of_mem_pi_polarCoord_target hx]

Result:
no goals

Proof state:
case h.e'_2
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ ∀ᵐ (x : ι → ℝ × ℝ),
    (x ∈ Set.univ.pi fun x => polarCoord.target) →
      ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun i => ↑polarCoord.symm (x i)) =
        ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun i => ↑polarCoord.symm (x i)

Tactic:
filter_upwards with x hx

Result:
case h.e'_2.h
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x => polarCoord.target
⊢ ((∏ i : ι, ENNReal.ofReal (x i).1) * f fun i => ↑polarCoord.symm (x i)) =
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun i => ↑polarCoord.symm (x i)