awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (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
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : polarSpace K
⊢ normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) =
    normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1)
have 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
Tactic: ext w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : polarSpace K
w : InfinitePlace K
⊢ normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) w =
    normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1) w
have 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
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ normAtComplexPlaces ((↑(OpenPartialHomeomorph.symm (polarSpaceCoord K)) : polarSpace K → mixedSpace K) x) w =
    normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x.1) w
have 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
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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 ≤ normAtComplexPlaces x w
have rw : 0 ≤ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
Tactic: rw [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (hypothesis)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
⊢ 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
have h : ∀ (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 _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ 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
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
have 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
Tactic: refine ⟨?_, fun ⟨hx₁, hx₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ 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
have 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
Tactic: refine ⟨?_, fun ⟨hx₁, hx₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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))
    ((⇑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)
have h₁ : Membership.mem (γ := Set (realSpace K)) ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A)
  (normAtComplexPlaces a)
Tactic: refine ⟨?_, by simpa using h a⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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)) ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A)
    (normAtComplexPlaces a)
have h₁ : normAtComplexPlaces a ∈ normAtComplexPlaces '' A
Tactic: rw [Set.mem_preimage, ← hA, Set.mem_preimage, normAtComplexPlaces_mixedSpaceOfRealSpace (h a)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ x ∈ normAtComplexPlaces '' A
have 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
Tactic: rwa [Set.mem_preimage, ← hA, Set.mem_preimage, normAtComplexPlaces_mixedSpaceOfRealSpace] at hx₁
Cleared hypotheses: hx₁, hx₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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))
have simp_rw : Eq (α := ℝ≥0∞) (A.indicator 1 x)
  ((normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A).indicator (1 ∘ normAtComplexPlaces) x)
Tactic: simp_rw [← Set.indicator_comp_right, Function.comp_def, Pi.one_def, hA]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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)
⊢ Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
have simp_rw₁ : Eq (α := ℝ≥0∞) (A.indicator 1 x)
  ((normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A).indicator (fun (x : mixedSpace K) ↦ 1 (normAtComplexPlaces x)) x)
Tactic: simp_rw [← Set.indicator_comp_right, Function.comp_def, Pi.one_def, hA]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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)
⊢ Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
have simp_rw₂ : Eq (α := ℝ≥0∞) (A.indicator (fun (x : mixedSpace K) ↦ 1) x)
  ((normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A).indicator (fun (x : mixedSpace K) ↦ 1) x)
Tactic: simp_rw [← Set.indicator_comp_right, Function.comp_def, Pi.one_def, hA]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (hypothesis)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
⊢ ((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))
have hA' : ∀ {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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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))
⊢ ((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))
have 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))
Tactic: rw [← lintegral_indicator_one hm, ← lintegral_comp_polarSpaceCoord_symm, polarSpaceCoord_target',
    Measure.volume_eq_prod, setLIntegral_prod]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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))
⊢ ((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))
have 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 (-π) π)))
Tactic: rw [← lintegral_indicator_one hm, ← lintegral_comp_polarSpaceCoord_symm, polarSpaceCoord_target',
    Measure.volume_eq_prod, setLIntegral_prod]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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))
⊢ ∫⁻ (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))
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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))
⊢ (∫⁻ (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
have 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
Tactic: rw [lintegral_mul_const' _ _ (ne_of_beq_false rfl).symm, mul_comm]