awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
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
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℝ × ℝ → ℝ≥0∞
⊢ InjOn (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) polarCoord.target

Tactic:
polarCoord.symm.injOn

Premises used: polarCoord, OpenPartialHomeomorph.injOn, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℝ × ℝ → ℝ≥0∞
⊢ MeasurableSet polarCoord.target

Tactic:
measurableSet_Ioi.prod measurableSet_Ioo

Premises used: MeasurableSet.prod, measurableSet_Ioi, measurableSet_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℝ × ℝ → ℝ≥0∞
⊢ InjOn (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) polarCoord.target

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

Premises used: MeasurableSet.prod, measurableSet_Ioi, polarCoord, measurableSet_Ioo, OpenPartialHomeomorph.injOn, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
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:
setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun, IsOpen.measurableSet, polarCoord, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℝ × ℝ → ℝ≥0∞
refine :
  ∀ (x : ℝ × ℝ) (hx : x ∈ polarCoord.target),
    ENNReal.ofReal |x.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
      ENNReal.ofReal x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
⊢ ∫⁻ (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 (fun x hx ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun, IsOpen.measurableSet, polarCoord, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℝ × ℝ → ℝ≥0∞
x : ℝ × ℝ
hx : x ∈ polarCoord.target
rw rw₁ :
  ENNReal.ofReal x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
    ENNReal.ofReal x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)
⊢ ENNReal.ofReal |x.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x) =
    ENNReal.ofReal x.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) x)

Tactic:
rw [abs_of_pos hx.1]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℝ × ℝ → ℝ≥0∞
_ : ∫⁻ (p : ℝ × ℝ), f p = ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p
_₁ :
  ∫⁻ (p : ℝ × ℝ) in (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) '' polarCoord.target, f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
_₂ :
  ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)
⊢ ∫⁻ (p : ℝ × ℝ), f p =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)

Tactic:
calc
    _ = ∫⁻ p in polarCoord.symm '' polarCoord.target, f p := by
      rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (polarCoord.symm p) := by
      rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
        (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
      · simp_rw [det_fderivPolarCoordSymm]; rfl
      exacts [polarCoord.symm.injOn, measurableSet_Ioi.prod measurableSet_Ioo]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) := by
      refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
      rw [abs_of_pos hx.1]

Premises used: PartialEquiv.target, polarCoord, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
a : ℂ
simp_rw : (↑Complex.polarCoord : ℂ → ℝ × ℝ) a = (√(HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.im 2), a.arg)
⊢ (↑Complex.polarCoord : ℂ → ℝ × ℝ) a = (‖a‖, a.arg)

Tactic:
simp_rw [Complex.norm_def, Complex.normSq_apply, ← pow_two]

Premises used: pow_two, Complex.norm_def, Complex.normSq_apply
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
a : ℂ
⊢ (↑Complex.polarCoord : ℂ → ℝ × ℝ) a = (√(HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.im 2), a.arg)

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
⊢ Complex.polarCoord.source = slitPlane

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Set.preimage, Not, Complex.slitPlane, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
⊢ Complex.polarCoord.target = SProd.sprod (α := Set ℝ) (Set.Ioi 0) (Set.Ioo (-π) π)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
⊢ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p = (↑p.1 : ℂ) * ((↑(Real.cos p.2) : ℂ) + (↑(Real.sin p.2) : ℂ) * I)

Tactic:
simp [Complex.polarCoord, equivRealProdCLM_symm_apply, mul_add, mul_assoc]

Premises used: mul_assoc, Complex.equivRealProdCLM_symm_apply, Complex.polarCoord, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
⊢ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p) =
    (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
⊢ ‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p‖ = |p.1|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
rw :
  Eq.{u_1 + 1} (α := E)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p))
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)))
⊢ Eq.{u_1 + 1} (α := E)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p))
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.volume fun (p : ℂ) ↦
      f p)

Tactic:
rw [← (Complex.volume_preserving_equiv_real_prod.symm).integral_comp
    measurableEquivRealProd.symm.measurableEmbedding, ← integral_comp_polarCoord_symm]

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.integral_comp, MeasureTheory.MeasurePreserving.symm, Complex.measurableEquivRealProd, MeasurableEquiv.symm, integral_comp_polarCoord_symm, Complex.volume_preserving_equiv_real_prod
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
⊢ Eq.{u_1 + 1} (α := E)
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p))
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 • f ((measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p)))

Tactic:
simp_rw [measurableEquivRealProd_symm_polarCoord_symm_apply]

Premises used: Complex.measurableEquivRealProd_symm_polarCoord_symm_apply
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℂ → ℝ≥0∞
rw :
  ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target,
      ENNReal.ofReal p.1 • f ((measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p) =
    ∫⁻ (p : ℂ), f p

Tactic:
rw [← (volume_preserving_equiv_real_prod.symm).lintegral_comp_emb
    measurableEquivRealProd.symm.measurableEmbedding, ← lintegral_comp_polarCoord_symm]

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.symm, Complex.measurableEquivRealProd, MeasureTheory.MeasurePreserving.lintegral_comp_emb, MeasurableEquiv.symm, Complex.volume_preserving_equiv_real_prod, lintegral_comp_polarCoord_symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f ((↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target,
      ENNReal.ofReal p.1 • f ((measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) ((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p))

Tactic:
simp_rw [measurableEquivRealProd_symm_polarCoord_symm_apply]

Premises used: Complex.measurableEquivRealProd_symm_polarCoord_symm_apply
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
⊢ Set.InjOn (β := (i : ι) → ℝ × ℝ) (fun (p : (i : ι) → ℝ × ℝ) (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i))
    (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target)

Tactic:
fun _ hx _ hy h ↦ funext fun i ↦ polarCoord.symm.injOn (hx i trivial) (hy i trivial)
    ((funext_iff.mp h) i)

Premises used: trivial, funext_iff, funext, polarCoord, OpenPartialHomeomorph.injOn, Iff.mp, Set.InjOn, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
p : ι → ℝ × ℝ
hp :
  Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
    (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) p
i : ι
⊢ |(p i).1| = (p i).1

Tactic:
abs_of_pos ((Set.mem_univ_pi.mp hp) i).1

Premises used: And.left, Iff.mp, abs_of_pos, Set.mem_univ_pi
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Finite ι
p : ι → ℝ × ℝ
have :
  ∀ (this : Fintype ι),
    HasFDerivAt (fun (x : ι → ℝ × ℝ) (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) (fderivPiPolarCoordSymm p) p
⊢ HasFDerivAt (fun (x : ι → ℝ × ℝ) (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) (fderivPiPolarCoordSymm p) p

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Finite ι
p : ι → ℝ × ℝ
this : Fintype ι
rw :
  ∀ (i : ι),
    HasFDerivAt (fun (x : ι → ℝ × ℝ) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
      (fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj (φ := fun (a : ι) ↦ ℝ × ℝ) i) p
⊢ HasFDerivAt (fun (x : ι → ℝ × ℝ) (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) (fderivPiPolarCoordSymm p) p

Tactic:
rw [fderivPiPolarCoordSymm, hasFDerivAt_pi]

Premises used: fderivPiPolarCoordSymm, hasFDerivAt_pi
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Finite ι
p : ι → ℝ × ℝ
this : Fintype ι
⊢ ∀ (i : ι),
    HasFDerivAt (fun (x : ι → ℝ × ℝ) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
      (fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj (φ := fun (a : ι) ↦ ℝ × ℝ) i) p

Tactic:
fun i ↦ HasFDerivAt.comp _ (hasFDerivAt_polarCoord_symm _) (hasFDerivAt_apply i _)

Premises used: setOf, hasFDerivAt_apply, OpenPartialHomeomorph.toFun', hasFDerivAt_polarCoord_symm, HasFDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Finite ι
p : ι → ℝ × ℝ
this : Fintype ι
⊢ ∀ (i : ι),
    HasFDerivAt (fun (x : ι → ℝ × ℝ) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
      (fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj (φ := fun (a : ι) ↦ ℝ × ℝ) i) p

Tactic:
exact fun i ↦ HasFDerivAt.comp _ (hasFDerivAt_polarCoord_symm _) (hasFDerivAt_apply i _)

Premises used: hasFDerivAt_polarCoord_symm, HasFDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Finite ι
⊢ MeasurableSet.{u_1} (α := (i : ι) → ℝ × ℝ)
    (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target)

Tactic:
MeasurableSet.univ_pi fun _ ↦ polarCoord.open_target.measurableSet

Premises used: IsOpen.measurableSet, polarCoord, OpenPartialHomeomorph.open_target, MeasurableSet.univ_pi
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
p : ι → ℝ × ℝ
simp_rw :
  Eq (α := ℝ)
    (ContinuousLinearMap.det.{0, u_1} (M := ι → ℝ × ℝ)
      (ContinuousLinearMap.pi (φ := fun (a : ι) ↦ ℝ × ℝ) fun (i : ι) ↦
        fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj (φ := fun (a : ι) ↦ ℝ × ℝ) i))
    (∏ i : ι, (p i).1)
simp_rw₁ : Eq (α := ℝ) (∏ i : ι, (fderivPolarCoordSymm (p i)).det) (∏ i : ι, (p i).1)
⊢ (fderivPiPolarCoordSymm p).det = ∏ i : ι, (p i).1

Tactic:
simp_rw [fderivPiPolarCoordSymm, ContinuousLinearMap.det_pi, det_fderivPolarCoordSymm]

Premises used: det_fderivPolarCoordSymm, fderivPiPolarCoordSymm, ContinuousLinearMap.det_pi
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
rw :
  (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (i : ι) ↦
      polarCoord.source) =ᶠ[ae (F := Measure ((i : ι) → ℝ × ℝ))
      (Measure.pi (α := fun (i : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ volume)]
    Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (i : ι) ↦ Set.univ
rw₁ : Set ι
⊢ Set.image (α := (i : ι) → ℝ × ℝ)
      (Pi.map (α := fun (x : ι) ↦ ℝ × ℝ) (β := fun (x : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
      (Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦
        polarCoord.target) =ᶠ[ae (F := Measure ((i : ι) → ℝ × ℝ)) volume]
    Set.univ

Tactic:
rw [Set.piMap_image_univ_pi, polarCoord.symm_image_target_eq_source, volume_pi, ← Set.pi_univ]

Premises used: MeasureTheory.volume_pi, OpenPartialHomeomorph.symm_image_target_eq_source, Set.piMap_image_univ_pi, polarCoord, Set.pi_univ
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
⊢ (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (i : ι) ↦
      polarCoord.source) =ᶠ[ae (F := Measure ((i : ι) → ℝ × ℝ))
      (Measure.pi (α := fun (i : ι) ↦ ℝ × ℝ) fun (x : ι) ↦ volume)]
    Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (i : ι) ↦ Set.univ

Tactic:
ae_eq_set_pi fun _ _ ↦ polarCoord_source_ae_eq_univ

Premises used: polarCoord_source_ae_eq_univ, MeasureTheory.Measure.ae_eq_set_pi
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
rw :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume
        (Set.image (α := (i : ι) → ℝ × ℝ)
          (Pi.map (α := fun (x : ι) ↦ ℝ × ℝ) (β := fun (x : ι) ↦ ℝ × ℝ) fun (x : ι) ↦
            (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
          (Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target)))
      fun (x : (i : ι) → ℝ × ℝ) ↦ f x)
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ι → ℝ × ℝ) ↦ f p)

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

Premises used: MeasureTheory.setIntegral_congr_set, pi_polarCoord_symm_target_ae_eq_univ, MeasureTheory.setIntegral_univ
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (x : ι → ℝ × ℝ) ↦ |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume
        ((fun (p : (i : ι) → ℝ × ℝ) (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)) ''
          Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (x : ι → ℝ × ℝ) ↦ f x)

Tactic:
(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

Premises used: MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, MeasureTheory.MeasureSpace.volume, injOn_pi_polarCoord_symm, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
h :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (x : ι → ℝ × ℝ) ↦ |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume
        (Set.image (α := (i : ι) → ℝ × ℝ)
          (Pi.map (α := fun (x : ι) ↦ ℝ × ℝ) (β := fun (x : ι) ↦ ℝ × ℝ) fun (x : ι) ↦
            (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ))
          (Set.pi (α := fun (i : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target)))
      fun (x : (i : ι) → ℝ × ℝ) ↦ 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

Premises used: MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, MeasureTheory.MeasureSpace.volume, injOn_pi_polarCoord_symm, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (x : ι → ℝ × ℝ) ↦ |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))

Tactic:
setIntegral_congr_fun measurableSet_pi_polarCoord_target fun x hx ↦ ?_

Premises used: measurableSet_pi_polarCoord_target, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
h :
  ∀ (x : (i : ι) → ℝ × ℝ)
    (hx :
      Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
        (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) x),
    HSMul.hSMul (α := ℝ) (∏ i : ι, (x i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
      |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (p : (i : ι) → ℝ × ℝ) ↦
      HSMul.hSMul (α := ℝ) (∏ i : ι, (p i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (p i)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target))
      fun (x : ι → ℝ × ℝ) ↦ |(fderivPiPolarCoordSymm x).det| • f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))

Tactic:
refine setIntegral_congr_fun measurableSet_pi_polarCoord_target fun x hx ↦ ?_

Premises used: measurableSet_pi_polarCoord_target, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : (i : ι) → ℝ × ℝ
hx :
  Membership.mem (γ := Set ((i : ι) → ℝ × ℝ))
    (Set.pi (α := fun (x : ι) ↦ ℝ × ℝ) Set.univ fun (x : ι) ↦ polarCoord.target) x
h :
  HSMul.hSMul (α := ℝ) (∏ i : ι, (x i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    HSMul.hSMul (α := ℝ) |∏ i : ι, (x i).1| (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
h₁ :
  HSMul.hSMul (α := ℝ) (∏ i : ι, (x i).1) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i)) =
    HSMul.hSMul (α := ℝ) (∏ x_1 : ι, |(x x_1).1|) (f fun (i : ι) ↦ (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) (x i))
⊢ HSMul.hSMul (α := ℝ) (∏ 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]

Premises used: abs_fst_of_mem_pi_polarCoord_target, det_fderivPiPolarCoordSymm, Finset.abs_prod
-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : (ι → ℂ) → E
e : ((a : ι) → ℝ × ℝ) ≃ᵐ ((a : ι) → ℂ) :=
  MeasurableEquiv.piCongrRight (π := fun (x : ι) ↦ ℝ × ℝ) (π' := fun (x : ι) ↦ ℂ) fun (x : ι) ↦
    measurableEquivRealProd.symm
⊢ MeasurePreserving (β := (i : ι) → ℂ)
    (fun (a : (i : ι) → ℝ × ℝ) (i : ι) ↦ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) (a i))
    (volume : Measure ((i : ι) → ℝ × ℝ)) (volume : Measure ((i : ι) → ℂ))

Tactic:
have := volume_preserving_pi (fun _ : ι ↦ Complex.volume_preserving_equiv_real_prod.symm)