awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : realMixedSpace K → ℝ≥0∞
rw :
  ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
⊢ ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ∫⁻ (x : realMixedSpace K), f x

Tactic:
rw [← setLIntegral_univ f, ← setLIntegral_congr (polarCoordReal_symm_target_ae_eq_univ K),
    lintegral_image_eq_lintegral_abs_det_fderiv_mul volume
      (polarCoordReal K).open_target.measurableSet
      (fun x _ ↦ (hasFDerivAt_polarCoordReal_symm K x).hasFDerivWithinAt)
      (polarCoordReal K).symm.injOn f]

Premises used: NumberField.mixedEmbedding.polarCoordReal, HasFDerivAt.hasFDerivWithinAt, IsOpen.measurableSet, MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, MeasureTheory.MeasureSpace.volume, OpenPartialHomeomorph.injOn, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, OpenPartialHomeomorph.open_target, MeasureTheory.setLIntegral_congr, OpenPartialHomeomorph.symm, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : realMixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)

Tactic:
setLIntegral_congr_fun (polarCoordReal K).open_target.measurableSet (fun x hx ↦ ?_)

Premises used: NumberField.mixedEmbedding.polarCoordReal, MeasureTheory.setLIntegral_congr_fun, IsOpen.measurableSet, OpenPartialHomeomorph.open_target
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : realMixedSpace K → ℝ≥0∞
refine :
  ∀ (x : realMixedSpace K)
    (hx :
      Membership.mem (γ := Set (realMixedSpace K))
        (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))) x),
    (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
      ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
⊢ ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)),
      ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
        f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)

Tactic:
refine setLIntegral_congr_fun (polarCoordReal K).open_target.measurableSet (fun x hx ↦ ?_)

Premises used: NumberField.mixedEmbedding.polarCoordReal, MeasureTheory.setLIntegral_congr_fun, IsOpen.measurableSet, OpenPartialHomeomorph.open_target
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : realMixedSpace K → ℝ≥0∞
x : realMixedSpace K
hx :
  Membership.mem (γ := Set (realMixedSpace K))
    (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))) x
simp_rw :
  (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ENNReal.ofReal |∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1| *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
simp_rw₁ :
  (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ENNReal.ofReal (∏ x_1 : { w : InfinitePlace K // w.IsComplex }, |(x.2 x_1).1|) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
simp_rw₂ :
  (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    (∏ i : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal |(x.2 i).1|) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)
⊢ (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x) =
    ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| *
      f ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x)

Tactic:
simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦ abs_nonneg _), abs_of_mem_polarCoordReal_target K hx]

Premises used: ENNReal.ofReal_prod_of_nonneg, _private.0.NumberField.mixedEmbedding.abs_of_mem_polarCoordReal_target, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, abs_nonneg, Finset.abs_prod
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (realMixedSpace K))
    (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K)))
    (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K)))

Tactic:
rfl

Premises used: Homeomorph.transOpenPartialHomeomorph, PartialEquiv.copy, Pi.map, Complex.polarCoord, polarCoord, PartialEquiv.pi, rfl, Equiv.transPartialEquiv
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := realMixedSpace K → mixedSpace K)
    (↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K)
    ((⇑(Homeomorph.symm (mixedSpaceToRealMixedSpace K)) : (a : realMixedSpace K) → mixedSpace K) ∘
      (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K))

Tactic:
rfl

Premises used: Prod.map, Pi.map, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Measurable (α := realMixedSpace K) (β := mixedSpace K)
    ((⇑(Homeomorph.symm (mixedSpaceToRealMixedSpace K)) : (a : realMixedSpace K) → mixedSpace K) ∘
      (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K))

Tactic:
(Homeomorph.measurable _).comp (measurable_polarCoordReal_symm K)

Premises used: NumberField.mixedEmbedding.measurable_polarCoordReal_symm, Measurable.comp, Homeomorph.measurable
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Measurable (α := realMixedSpace K) (β := mixedSpace K)
    ((⇑(Homeomorph.symm (mixedSpaceToRealMixedSpace K)) : (a : realMixedSpace K) → mixedSpace K) ∘
      (↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K))

Tactic:
exact (Homeomorph.measurable _).comp (measurable_polarCoordReal_symm K)

Premises used: NumberField.mixedEmbedding.measurable_polarCoordReal_symm, Measurable.comp, Homeomorph.measurable
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x) =
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖

Tactic:
simp [normAtPlace_apply_of_isReal hw]

Premises used: NumberField.mixedEmbedding.normAtPlace_apply_of_isReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realMixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x) =
    ‖(x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)).1‖

Tactic:
simp [normAtPlace_apply_of_isComplex hw]

Premises used: NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
⊢ Continuous (Y := (w : { w : InfinitePlace K // w.IsComplex }) → ℝ)
    fun (x : realMixedSpace K) (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x.2 w).2

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
refine :
  ∀ (w : InfinitePlace K),
    Continuous (Y := ℝ) fun (a : realMixedSpace K) ↦
      if hw : w.IsReal then a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)
      else (a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)).1
⊢ Continuous (Y := ((w : InfinitePlace K) → ℝ) × ((w : { w : InfinitePlace K // w.IsComplex }) → ℝ))
    fun (x : realMixedSpace K) ↦
    (fun (w : InfinitePlace K) ↦
      if hw : w.IsReal then x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)
      else (x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)).1,
      fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x.2 w).2)

Tactic:
refine .prodMk (continuous_pi fun w ↦ ?_) (by fun_prop)
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
pos :
  ∀ (h : w.IsReal),
    Continuous (Y := ℝ) fun (a : realMixedSpace K) ↦ a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)
neg :
  ∀ (h : ¬w.IsReal),
    Continuous (Y := ℝ) fun (a : realMixedSpace K) ↦
      (a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)).1
⊢ Continuous (Y := ℝ) fun (a : realMixedSpace K) ↦
    if hw : w.IsReal then a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)
    else (a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)).1

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
h : w.IsReal
⊢ Continuous (Y := ℝ) fun (a : realMixedSpace K) ↦ a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
h : ¬w.IsReal
⊢ Continuous (Y := ℝ) fun (a : realMixedSpace K) ↦
    (a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)).1

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
⊢ Continuous (Y := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ))
    fun (x : polarSpace K) ↦
    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x.1 (↑w : InfinitePlace K),
      fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x.1 (↑w : InfinitePlace K), x.2 w))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
x : realMixedSpace K
⊢ Eq (α := polarSpace K) ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x : polarSpace K)
    ((fun (w : InfinitePlace K) ↦
        if hw : w.IsReal then x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)
        else (x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)).1,
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x.2 w).2) :
      (InfinitePlace K → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℝ))

Tactic:
rfl

Premises used: Prod.map, dite, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
x : realMixedSpace K
w : { w : InfinitePlace K // w.IsReal }
simp_rw :
  (if hw : (↑w : InfinitePlace K).IsReal then
      x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (↑w : InfinitePlace K) hw)
    else (x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (↑w : InfinitePlace K) ⋯)).1) =
    x.1 w
⊢ ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).1 (↑w : InfinitePlace K) = x.1 w

Tactic:
simp_rw [homeoRealMixedSpacePolarSpace_apply, dif_pos w.prop]

Premises used: dif_pos, Subtype.prop, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
x : realMixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
simp_rw :
  (if hw : (↑w : InfinitePlace K).IsReal then
      x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (↑w : InfinitePlace K) hw)
    else (x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (↑w : InfinitePlace K) ⋯)).1) =
    (x.2 w).1
⊢ ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).1 (↑w : InfinitePlace K) = (x.2 w).1

Tactic:
simp_rw [homeoRealMixedSpacePolarSpace_apply, dif_neg (not_isReal_iff_isComplex.mpr w.prop)]

Premises used: Iff.mpr, dif_neg, Subtype.prop, NumberField.InfinitePlace.not_isReal_iff_isComplex, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
x : realMixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
⊢ ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).2 w = (x.2 w).2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
x : polarSpace K
⊢ Eq (α := realMixedSpace K)
    ((Homeomorph.symm (homeoRealMixedSpacePolarSpace K) : (a : polarSpace K) → realMixedSpace K) x : realMixedSpace K)
    ((fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x.1 (↑w : InfinitePlace K),
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x.1 (↑w : InfinitePlace K), x.2 w)) :
      ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ))

Tactic:
rfl

Premises used: NumberField.InfinitePlace.IsComplex, Prod.map, Not, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurePreserving (α := realMixedSpace K) (β := polarSpace K)
    (⇑(homeoRealMixedSpacePolarSpace K) : (a : realMixedSpace K) → polarSpace K) (volume : Measure (realMixedSpace K))
    (volume : Measure (polarSpace K))

Tactic:
((MeasurePreserving.id volume).prod
    (volume_measurePreserving_arrowProdEquivProdArrow ℝ ℝ _)).trans <|
      (volume_preserving_prodAssoc.symm).trans <|
        (((MeasurePreserving.id volume).prod (volume_preserving_arrowCongr' _
          (MeasurableEquiv.refl ℝ) (.id volume))).prod (.id volume)).trans <|
            ((volume_preserving_piEquivPiSubtypeProd
              (fun _ : InfinitePlace K ↦ ℝ) (fun w ↦ IsReal w)).symm).prod (.id volume)

Premises used: Real, MeasureTheory.MeasurePreserving.prod, MeasureTheory.MeasurePreserving.symm, MeasureTheory.volume_preserving_prodAssoc, NumberField.InfinitePlace.IsReal, MeasureTheory.MeasureSpace.volume, MeasureTheory.MeasurePreserving.id, MeasureTheory.volume_preserving_piEquivPiSubtypeProd, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Measurable (α := polarSpace K) (β := mixedSpace K)
    ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) ∘
      (⇑(Homeomorph.symm (homeoRealMixedSpacePolarSpace K)) : (a : polarSpace K) → realMixedSpace K))

Tactic:
(measurable_polarCoord_symm K).comp (Homeomorph.measurable _)

Premises used: Measurable.comp, NumberField.mixedEmbedding.measurable_polarCoord_symm, Homeomorph.measurable
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Measurable (α := polarSpace K) (β := mixedSpace K)
    ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) ∘
      (⇑(Homeomorph.symm (homeoRealMixedSpacePolarSpace K)) : (a : polarSpace K) → realMixedSpace K))

Tactic:
exact (measurable_polarCoord_symm K).comp (Homeomorph.measurable _)

Premises used: Measurable.comp, NumberField.mixedEmbedding.measurable_polarCoord_symm, Homeomorph.measurable
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : polarSpace K),
    Membership.mem (γ := Set (polarSpace K))
        (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarSpaceCoord K))) x ↔
      x ∈
        SProd.sprod (α := Set ((i : InfinitePlace K) → ℝ)) (β := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ))
          (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ioi 0)
          (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
            fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π)
⊢ PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarSpaceCoord K)) =
    SProd.sprod (α := Set ((i : InfinitePlace K) → ℝ)) (β := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ))
      (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ioi 0)
      (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
        fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : mixedSpace K → E
rw :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (restrict volume
          (SProd.sprod (α := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) (β :=
            Set ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) Set.univ
            (Set.pi (α := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) Set.univ
              fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ Complex.polarCoord.target)) :
        Measure (realMixedSpace K))
      fun (x : realMixedSpace K) ↦
      HSMul.hSMul (α := ℝ)
        (∏ w : { w : InfinitePlace K // w.IsComplex },
          ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).1 (↑w : InfinitePlace K))
        (f
          ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K)
            ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume
        (SProd.sprod (α := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) (β :=
          Set ({ w : InfinitePlace K // w.IsComplex } → ℝ × ℝ)) Set.univ
          (Set.pi (α := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) Set.univ
            fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ Complex.polarCoord.target)))
      fun (x : realMixedSpace K) ↦
      HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
        (f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x)))
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarSpaceCoord K))))
      fun (x : polarSpace K) ↦
      HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, x.1 (↑w : InfinitePlace K))
        (f ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ f x)

Tactic:
rw [← (volume_preserving_homeoRealMixedSpacePolarSpace K).setIntegral_preimage_emb
    (homeoRealMixedSpacePolarSpace K).measurableEmbedding,
    ← mixedEmbedding.integral_comp_polarCoord_symm, polarSpaceCoord_target,
    ← Homeomorph.image_eq_preimage_symm, Homeomorph.preimage_image,
    mixedEmbedding.polarCoord_target]

Premises used: NumberField.mixedEmbedding.polarSpaceCoord_target, Homeomorph.measurableEmbedding, MeasureTheory.MeasurePreserving.setIntegral_preimage_emb, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace, NumberField.mixedEmbedding.polarCoord_target, Homeomorph.image_eq_preimage_symm, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, Homeomorph.preimage_image, NumberField.mixedEmbedding.integral_comp_polarCoord_symm