-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem lintegral_comp_polarCoord_symm (f : ℝ × ℝ → ℝ≥0∞) :
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) =
      ∫⁻ (p : ℝ × ℝ), f p

Proof state:
f : ℝ × ℝ → ℝ≥0∞
a✝ : ℝ × ℝ
hx : a✝ ∈ polarCoord.target
⊢ ENNReal.ofReal |a✝.1| • f (↑polarCoord.symm a✝) = ENNReal.ofReal a✝.1 • f (↑polarCoord.symm a✝)

Tactic:
rw [abs_of_pos hx.1]

Result:
no goals

Proof state:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑polarCoord.symm p) = ∫⁻ (p : ℝ × ℝ), f p

Tactic:
symm

Result:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑polarCoord.symm p)

Proof state:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑polarCoord.symm p)

Tactic:
refine setLIntegral_congr_fun polarCoord.open_target.measurableSet ?_

Result:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∀ᵐ (x : ℝ × ℝ),
    x ∈ polarCoord.target → ENNReal.ofReal |x.1| • f (↑polarCoord.symm x) = ENNReal.ofReal x.1 • f (↑polarCoord.symm x)

Proof state:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f (↑polarCoord.symm x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p)

Tactic:
simp_rw [det_fderivPolarCoordSymm]

Result:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |x.1| * f (↑polarCoord.symm x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p)

Proof state:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∀ᵐ (x : ℝ × ℝ),
    x ∈ polarCoord.target → ENNReal.ofReal |x.1| • f (↑polarCoord.symm x) = ENNReal.ofReal x.1 • f (↑polarCoord.symm x)

Tactic:
filter_upwards with _ hx using by rw [abs_of_pos hx.1]

Result:
no goals

Proof state:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |x.1| * f (↑polarCoord.symm x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p)

Tactic:
rfl

Result:
no goals

Proof state:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in ↑polarCoord.symm '' polarCoord.target, f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p)

Tactic:
rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
  (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]

Result:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f (↑polarCoord.symm x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p)

case hf
f : ℝ × ℝ → ℝ≥0∞
⊢ InjOn (↑polarCoord.symm) polarCoord.target

f : ℝ × ℝ → ℝ≥0∞
⊢ MeasurableSet polarCoord.target

Proof state:
case hf
f : ℝ × ℝ → ℝ≥0∞
⊢ InjOn (↑polarCoord.symm) polarCoord.target

f : ℝ × ℝ → ℝ≥0∞
⊢ MeasurableSet polarCoord.target

Tactic:
exacts [polarCoord.symm.injOn, measurableSet_Ioi.prod measurableSet_Ioo]

Result:
no goals

Proof state:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in ↑polarCoord.symm '' polarCoord.target, f p

Tactic:
rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
  polarCoord.symm_image_target_eq_source ]

Result:
no goals