awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
      ∫⁻ (a : 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 : InfinitePlace K → ℝ) ↦
            ∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)))
          a ∂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,
      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

Tactic:
rw [lintegral_mul_const' _ _ (ne_of_beq_false rfl).symm, mul_comm]

Premises used: ne_of_beq_false, Ne.symm, mul_comm, MeasureTheory.lintegral_mul_const'
-- 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))
⊢ MeasurableSet (α := realSpace K) ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A)

Tactic:
hm.preimage mixedSpaceOfRealSpace.measurable

Premises used: MeasurableSet.preimage, ContinuousLinearMap.measurable
-- 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))
⊢ MeasurableSet (α := InfinitePlace K → ℝ)
    ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A)

Tactic:
convert! hm.preimage mixedSpaceOfRealSpace.measurable

Premises used: MeasurableSet.preimage, ContinuousLinearMap.measurable
-- 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))
erw :
  (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹'
            normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A ∩
          Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ioi 0,
        (fun (x : InfinitePlace K → ℝ) ↦
            (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
          a ∂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
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
      ∫⁻ (a : 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 : InfinitePlace K → ℝ) ↦
            ∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)))
          a ∂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

Tactic:
erw [setLIntegral_indicator (by convert! hm.preimage mixedSpaceOfRealSpace.measurable)]

Premises used: MeasureTheory.setLIntegral_indicator
-- 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 :
  (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
          Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ioi 0,
        (fun (x : InfinitePlace K → ℝ) ↦
            (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
          a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in
        (⇑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,
        ∏ w : { w : InfinitePlace K // w.IsComplex },
          ENNReal.ofReal
            (x
              (↑w :
                InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹'
            normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A ∩
          Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ioi 0,
        (fun (x : InfinitePlace K → ℝ) ↦
            (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
          a ∂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

Tactic:
rw [hA, volume_eq_two_pi_pow_mul_integral_aux hA]

Premises used: _private.0.NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral_aux
-- 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))
e_a :
  (∫⁻ (a : InfinitePlace K → ℝ) in
      (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0,
      (fun (x : InfinitePlace K → ℝ) ↦
          (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
        a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
    ∫⁻ (x : realSpace K) in
      (⇑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,
      ∏ w : { w : InfinitePlace K // w.IsComplex },
        ENNReal.ofReal
          (x (↑w : InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
          Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ioi 0,
        (fun (x : InfinitePlace K → ℝ) ↦
            (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
          a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in
        (⇑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,
        ∏ w : { w : InfinitePlace K // w.IsComplex },
          ENNReal.ofReal
            (x
              (↑w :
                InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume

Tactic:
congr 1
-- 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))
⊢ (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹'
      A =ᶠ[ae (F := Measure (InfinitePlace K → ℝ))
      (Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume)]
    (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A

Tactic:
rfl
-- 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))
e_a :
  ∀ (w : InfinitePlace K),
    Membership.mem (γ := Set (InfinitePlace K)) Set.univ w →
      (if w.IsReal then Set.univ else Set.Ioi 0) =ᶠ[ae (F := Measure ℝ) volume] if w.IsReal then Set.univ else Set.Ici 0
⊢ (∫⁻ (a : InfinitePlace K → ℝ) in
      (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0,
      (fun (x : InfinitePlace K → ℝ) ↦
          (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
        a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
    ∫⁻ (x : realSpace K) in
      (⇑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,
      ∏ w : { w : InfinitePlace K // w.IsComplex },
        ENNReal.ofReal
          (x (↑w : InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume

Tactic:
refine setLIntegral_congr (ae_eq_set_inter (by rfl) (Measure.ae_eq_set_pi fun w _ ↦ ?_))

Premises used: MeasureTheory.ae_eq_set_inter, MeasureTheory.Measure.ae_eq_set_pi, MeasureTheory.setLIntegral_congr
-- 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))
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
pos : w.IsReal → Set.univ =ᶠ[ae (F := Measure ℝ) volume] Set.univ
neg : ¬w.IsReal → Set.Ioi 0 =ᶠ[ae (F := Measure ℝ) volume] Set.Ici 0
⊢ (if w.IsReal then Set.univ else Set.Ioi 0) =ᶠ[ae (F := Measure ℝ) volume] if w.IsReal then Set.univ else Set.Ici 0

Tactic:
split_ifs
-- 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))
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
h_1 : w.IsReal
⊢ Set.univ =ᶠ[ae (F := Measure ℝ) volume] Set.univ

Tactic:
ae_eq_rfl

Premises used: MeasureTheory.ae_eq_rfl
-- 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))
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
h_1 : ¬w.IsReal
⊢ Set.Ioi 0 =ᶠ[ae (F := Measure ℝ) volume] Set.Ici 0

Tactic:
Ioi_ae_eq_Ici

Premises used: MeasureTheory.Ioi_ae_eq_Ici
-- 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))
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
h_1 : w.IsReal
⊢ Set.univ =ᶠ[ae (F := Measure ℝ) volume] Set.univ

Tactic:
exacts [ae_eq_rfl, Ioi_ae_eq_Ici]

Premises used: MeasureTheory.ae_eq_rfl, MeasureTheory.Ioi_ae_eq_Ici
-- 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))
⊢ Measurable (β := ℝ≥0∞) fun (x : polarSpace K) ↦
    ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.1 (↑w : InfinitePlace K))

Tactic:
fun_prop
-- 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))
⊢ 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 (-π) π)))

Tactic:
exact (Measurable.mul (by fun_prop)
      <| measurable_const.indicator <| hm.preimage (measurable_polarSpaceCoord_symm K)).aemeasurable

Premises used: MeasurableSet.preimage, Measurable.mul, Measurable.aemeasurable, Measurable.indicator, measurable_const, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
h :
  ∀ (x : realSpace K),
    x ∈
        normAtAllPlaces '' A ∩
          ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} ↔
      x ∈ normAtComplexPlaces '' plusPart A
⊢ normAtAllPlaces '' A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} =
    normAtComplexPlaces '' plusPart A

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
x : realSpace K
⊢ x ∈
      normAtAllPlaces '' A ∩
        ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} ↔
    x ∈ normAtComplexPlaces '' plusPart A

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
x : realSpace K
h :
  x ∈
      normAtAllPlaces '' A ∩
        ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} →
    x ∈ normAtComplexPlaces '' plusPart A
h₁ :
  x ∈ normAtComplexPlaces '' plusPart A →
    x ∈
      normAtAllPlaces '' A ∩
        ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}
⊢ x ∈
      normAtAllPlaces '' A ∩
        ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} ↔
    x ∈ normAtComplexPlaces '' plusPart A

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ :
  Membership.mem (γ := Set (realSpace K))
    (⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}) (normAtAllPlaces a)
⊢ normAtAllPlaces a ∈ normAtComplexPlaces '' plusPart A

Tactic:
⟨mixedSpaceOfRealSpace (normAtAllPlaces a), ⟨?_, ?_⟩, ?_⟩

Premises used: Set.Mem, setOf, NumberField.mixedEmbedding.mixedSpaceOfRealSpace, NumberField.mixedEmbedding.normAtAllPlaces, And.intro, Exists.intro, Set.image, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ :
  Membership.mem (γ := Set (realSpace K))
    (⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}) (normAtAllPlaces a)
h :
  Membership.mem (α := mixedSpace K) A
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a) : mixedSpace K)
h₁ :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K))
    {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w}
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a) : mixedSpace K)
h₂ :
  normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a)) =
    normAtAllPlaces a
⊢ normAtAllPlaces a ∈ normAtComplexPlaces '' plusPart A

Tactic:
refine ⟨mixedSpaceOfRealSpace (normAtAllPlaces a), ⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ :
  Membership.mem (γ := Set (realSpace K))
    (⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}) (normAtAllPlaces a)
h : normAtAllPlaces a ∈ normAtAllPlaces '' A
⊢ Membership.mem (α := mixedSpace K) A
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a) : mixedSpace K)

Tactic:
rw [← hA, Set.mem_preimage, normAtAllPlaces_normAtAllPlaces]

Premises used: Set.mem_preimage, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ :
  Membership.mem (γ := Set (realSpace K))
    (⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}) (normAtAllPlaces a)
⊢ normAtAllPlaces a ∈ normAtAllPlaces '' A

Tactic:
Set.mem_image_of_mem normAtAllPlaces ha

Premises used: NumberField.mixedEmbedding.normAtAllPlaces, Set.mem_image_of_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ :
  Membership.mem (γ := Set (realSpace K))
    (⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}) (normAtAllPlaces a)
⊢ normAtAllPlaces a ∈ normAtAllPlaces '' A

Tactic:
exact Set.mem_image_of_mem normAtAllPlaces ha

Premises used: NumberField.mixedEmbedding.normAtAllPlaces, Set.mem_image_of_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ :
  Membership.mem (γ := Set (realSpace K))
    (⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}) (normAtAllPlaces a)
w : { w : InfinitePlace K // w.IsReal }
⊢ LT.lt (α := ℝ) 0 (((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a)).1 w)

Tactic:
lt_of_le_of_ne' (normAtPlace_nonneg _ _) (Set.mem_iInter.mp ha₂ w)

Premises used: Set.mem_iInter, lt_of_le_of_ne', NumberField.mixedEmbedding.normAtPlace_nonneg, Iff.mp