-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem integral_comp_polarCoord_symm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : ℝ × ℝ → E) :
    (∫ p in polarCoord.target, p.1 • f (polarCoord.symm p)) = ∫ p, f p

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p)

Tactic:
calc
  ∫ p, f p = ∫ p in polarCoord.source, f p := by
    rw [← setIntegral_univ]
    apply setIntegral_congr_set
    exact polarCoord_source_ae_eq_univ.symm
  _ = ∫ p in polarCoord.target, |p.1| • f (polarCoord.symm p) := by
    rw [← PartialHomeomorph.symm_target, integral_target_eq_integral_abs_det_fderiv_smul volume
    (fun p _ ↦ hasFDerivAt_polarCoord_symm p), PartialHomeomorph.symm_source]
    simp_rw [det_fderivPolarCoordSymm]
  _ = ∫ p in polarCoord.target, p.1 • f (polarCoord.symm p) := by
    apply setIntegral_congr_fun polarCoord.open_target.measurableSet fun x hx => ?_
    rw [abs_of_pos hx.1]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
x : ℝ × ℝ
hx : x ∈ polarCoord.target
⊢ |x.1| • f (↑polarCoord.symm x) = x.1 • f (↑polarCoord.symm x)

Tactic:
rw [abs_of_pos hx.1]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (x : ℝ × ℝ) in univ, f x = ∫ (p : ℝ × ℝ) in polarCoord.source, f p

Tactic:
apply setIntegral_congr_set

Result:
case hst
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ univ =ᶠ[ae volume] polarCoord.source

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.source, f p = ∫ (p : ℝ × ℝ) in polarCoord.target, |p.1| • f (↑polarCoord.symm p)

Tactic:
rw [← PartialHomeomorph.symm_target, integral_target_eq_integral_abs_det_fderiv_smul volume
(fun p _ ↦ hasFDerivAt_polarCoord_symm p), PartialHomeomorph.symm_source]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (x : ℝ × ℝ) in polarCoord.target, |(fderivPolarCoordSymm x).det| • f (↑polarCoord.symm x) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, |p.1| • f (↑polarCoord.symm p)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p) = ∫ (p : ℝ × ℝ), f p

Tactic:
symm

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, |p.1| • f (↑polarCoord.symm p) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p)

Tactic:
apply setIntegral_congr_fun polarCoord.open_target.measurableSet fun x hx => ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
x : ℝ × ℝ
hx : x ∈ polarCoord.target
⊢ |x.1| • f (↑polarCoord.symm x) = x.1 • f (↑polarCoord.symm x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (x : ℝ × ℝ) in polarCoord.target, |(fderivPolarCoordSymm x).det| • f (↑polarCoord.symm x) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, |p.1| • f (↑polarCoord.symm p)

Tactic:
simp_rw [det_fderivPolarCoordSymm]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.source, f p

Tactic:
rw [← setIntegral_univ]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (x : ℝ × ℝ) in univ, f x = ∫ (p : ℝ × ℝ) in polarCoord.source, f p

Proof state:
case hst
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ univ =ᶠ[ae volume] polarCoord.source

Tactic:
exact polarCoord_source_ae_eq_univ.symm

Result:
no goals