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 : mixedSpace K → ℝ≥0∞
rw :
  ∫⁻ (a : realMixedSpace K) in
      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),
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          ENNReal.ofReal
            (((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) a).1 (↑w : InfinitePlace K))) *
        f
          ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K)
            ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) a)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in
      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),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x)
⊢ ∫⁻ (x : polarSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarSpaceCoord K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.1 (↑w : InfinitePlace K))) *
        f ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) =
    ∫⁻ (x : mixedSpace K), f x

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

Premises used: NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, NumberField.mixedEmbedding.polarSpaceCoord_target, Homeomorph.measurableEmbedding, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace, NumberField.mixedEmbedding.polarCoord_target, Homeomorph.image_eq_preimage_symm, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, Homeomorph.preimage_image, MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : polarSpace K
h :
  ∀ (w : InfinitePlace K),
    normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) w =
      normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1) w
⊢ normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) =
    normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1)

Tactic:
ext w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : polarSpace K
w : InfinitePlace K
h :
  ∀ (hw : w.IsReal),
    normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) w =
      normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1) w
h₁ :
  ∀ (hw : w.IsComplex),
    normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) w =
      normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1) w
⊢ normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) w =
    normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1) w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : polarSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) w =
    normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1) w

Tactic:
simp [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]

Premises used: Subtype.mk, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isReal, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : polarSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) w =
    normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1) w

Tactic:
simp [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]

Premises used: Subtype.mk, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isComplex, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
rw : 0 ≤ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
⊢ 0 ≤ normAtComplexPlaces x w

Tactic:
rw [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]

Premises used: Subtype.mk, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ 0 ≤ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ 0 ≤ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖

Tactic:
exact norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
⊢ ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w

Tactic:
have h : ∀ (x : mixedSpace K), ∀ w, IsComplex w → 0 ≤ normAtComplexPlaces x w := by
    intro x w hw
    rw [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]
    exact norm_nonneg _
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
h₁ :
  ∀ (x : realSpace K),
    x ∈ normAtComplexPlaces '' A ↔
      Membership.mem (γ := Set (realSpace K))
        ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
          Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ici 0)
        x
⊢ normAtComplexPlaces '' A =
    (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
      Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ici 0

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
⊢ x ∈ normAtComplexPlaces '' A ↔
    Membership.mem (γ := Set (realSpace K))
      ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ici 0)
      x

Tactic:
⟨?_, fun ⟨hx₁, hx₂⟩ ↦ ?_⟩

Premises used: Membership.mem, Iff.intro, Set.image, _private.0.NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral_aux.match_1, NumberField.mixedEmbedding.normAtComplexPlaces
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
h₁ :
  x ∈ normAtComplexPlaces '' A →
    Membership.mem (γ := Set (realSpace K))
      ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ici 0)
      x
h₂ :
  Membership.mem (γ := Set (realSpace K))
      ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ici 0)
      x →
    ∀
      (hx₁ :
        Membership.mem (γ := Set (realSpace K)) ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A) x)
      (hx₂ :
        Membership.mem (γ := Set (realSpace K))
          (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ici 0)
          x),
      x ∈ normAtComplexPlaces '' A
⊢ x ∈ normAtComplexPlaces '' A ↔
    Membership.mem (γ := Set (realSpace K))
      ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ici 0)
      x

Tactic:
refine ⟨?_, fun ⟨hx₁, hx₂⟩ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ Membership.mem (γ := Set (realSpace K))
    (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w.IsReal then Set.univ else Set.Ici 0)
    (normAtComplexPlaces a)

Tactic:
simpa using h a
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
h₁ :
  Membership.mem (γ := Set (realSpace K)) ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A)
    (normAtComplexPlaces a)
⊢ Membership.mem (γ := Set (realSpace K))
    ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
      Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ici 0)
    (normAtComplexPlaces a)

Tactic:
refine ⟨?_, by simpa using h a⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
h₁ : normAtComplexPlaces a ∈ normAtComplexPlaces '' A
⊢ Membership.mem (γ := Set (realSpace K)) ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A)
    (normAtComplexPlaces a)

Tactic:
rw [Set.mem_preimage, ← hA, Set.mem_preimage, normAtComplexPlaces_mixedSpaceOfRealSpace (h a)]

Premises used: NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, Set.mem_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ normAtComplexPlaces a ∈ normAtComplexPlaces '' A

Tactic:
Set.mem_image_of_mem _ ha

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ normAtComplexPlaces a ∈ normAtComplexPlaces '' A

Tactic:
exact Set.mem_image_of_mem _ ha

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
h_1 :
  Membership.mem (γ := Set (realSpace K))
    ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
      Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ici 0)
    x
hx₁ : Membership.mem (γ := Set (realSpace K)) ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A) x
hx₂ :
  Membership.mem (γ := Set (realSpace K))
    (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w.IsReal then Set.univ else Set.Ici 0)
    x
h₁ :
  ∀
    (hx₁ :
      normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) ∈ normAtComplexPlaces '' A)
    (hx₂ :
      Membership.mem (γ := Set (realSpace K))
        (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ici 0)
        x)
    (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
⊢ x ∈ normAtComplexPlaces '' A

Tactic:
rwa [Set.mem_preimage, ← hA, Set.mem_preimage, normAtComplexPlaces_mixedSpaceOfRealSpace] at hx₁

Premises used: NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, Set.mem_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
h_1 :
  Membership.mem (γ := Set (realSpace K))
    ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
      Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ici 0)
    x
hx₁ : normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) ∈ normAtComplexPlaces '' A
hx₂ :
  Membership.mem (γ := Set (realSpace K))
    (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w.IsReal then Set.univ else Set.Ici 0)
    x
w : InfinitePlace K
hw : w.IsComplex
⊢ 0 ≤ x w

Tactic:
simpa [if_neg (not_isReal_iff_isComplex.mpr hw)] using hx₂ w (Set.mem_univ w)

Premises used: Iff.mpr, Set.mem_univ, NumberField.InfinitePlace.not_isReal_iff_isComplex, if_neg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
x : mixedSpace K
simp_rw :
  Eq (α := ℝ≥0∞) (A.indicator 1 x)
    ((normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A).indicator (1 ∘ normAtComplexPlaces) x)
simp_rw₁ :
  Eq (α := ℝ≥0∞) (A.indicator 1 x)
    ((normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A).indicator (fun (x : mixedSpace K) ↦ 1 (normAtComplexPlaces x))
      x)
simp_rw₂ :
  Eq (α := ℝ≥0∞) (A.indicator (fun (x : mixedSpace K) ↦ 1) x)
    ((normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A).indicator (fun (x : mixedSpace K) ↦ 1) x)
⊢ Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))

Tactic:
simp_rw [← Set.indicator_comp_right, Function.comp_def, Pi.one_def, hA]

Premises used: Set.indicator_comp_right, Function.comp_def, Pi.one_def
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
⊢ ∀ {x : mixedSpace K},
    Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))

Tactic:
have hA' {x} : (A.indicator 1 x : ℝ≥0∞) =
      (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x) := by
    simp_rw [← Set.indicator_comp_right, Function.comp_def, Pi.one_def, hA]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' :
  ∀ {x : mixedSpace K},
    Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
rw :
  ∫⁻ (x : InfinitePlace K → ℝ) in
      Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ioi 0,
      ∫⁻ (y : { w : InfinitePlace K // w.IsComplex } → ℝ) in
        Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π,
        HMul.hMul (α := ℝ≥0∞)
          (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal ((x, y).1 (↑w : InfinitePlace K)))
          (A.indicator 1 ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) (x, y))) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
hf :
  AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (fun (x : polarSpace K) ↦
      HMul.hMul (α := ℝ≥0∞) (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.1 (↑w : InfinitePlace K)))
        (A.indicator 1 ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x)))
    (restrict (Measure.prod volume volume)
      (SProd.sprod (α := Set (InfinitePlace K → ℝ)) (β := Set ({ 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 (-π) π)))
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) A =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))

Tactic:
rw [← lintegral_indicator_one hm, ← lintegral_comp_polarSpaceCoord_symm, polarSpaceCoord_target',
    Measure.volume_eq_prod, setLIntegral_prod]

Premises used: MeasureTheory.Measure.volume_eq_prod, NumberField.mixedEmbedding.polarSpaceCoord_target', MeasureTheory.lintegral_indicator_one, MeasureTheory.setLIntegral_prod, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' :
  ∀ {x : mixedSpace K},
    Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
simp_rw :
  (∫⁻ (x : InfinitePlace K → ℝ) in
      Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ioi 0,
      Set.indicator
          ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹'
            normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A)
          (fun (x_1 : InfinitePlace K → ℝ) ↦
            ∏ x_2 : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑x_2 : InfinitePlace K)))
          x *
        ENNReal.ofReal (2 * π) ^
          Fintype.card.{u_1}
            { w : InfinitePlace K //
              w.IsComplex } ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex },
          ENNReal.ofReal
            (x
              (↑w :
                InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
⊢ ∫⁻ (x : InfinitePlace K → ℝ) in
      Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ioi 0,
      ∫⁻ (y : { w : InfinitePlace K // w.IsComplex } → ℝ) in
        Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π,
        HMul.hMul (α := ℝ≥0∞)
          (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal ((x, y).1 (↑w : InfinitePlace K)))
          (A.indicator 1 ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) (x, y))) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))

Tactic:
simp_rw [hA', normAtComplexPlaces_polarSpaceCoord_symm, lintegral_const, restrict_apply
      MeasurableSet.univ, Set.univ_inter, volume_pi, Measure.pi_pi, volume_Ioo, sub_neg_eq_add,
      ← two_mul, Finset.prod_const, Finset.card_univ, ← Set.indicator_const_mul,
      ← Set.indicator_comp_right, Function.comp_def, Pi.one_apply, mul_one]

Premises used: Finset.card_univ, MeasureTheory.lintegral_const, MeasureTheory.volume_pi, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, Pi.one_apply, MeasureTheory.Measure.restrict_apply, two_mul, Set.indicator_comp_right, Finset.prod_const, Set.univ_inter, Function.comp_def, Set.indicator_const_mul, mul_one, Real.volume_Ioo, MeasureTheory.Measure.pi_pi, sub_neg_eq_add, MeasurableSet.univ