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 : 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)
⊢ (∏ 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)
have 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)
Tactic: simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦ abs_nonneg _), abs_of_mem_polarCoordReal_target K hx]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K))))
      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)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ f x)
have rw : Eq.{u_2 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K))))
    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)))
  (@integral _ _ _ _ Prod.instMeasurableSpace (volume : Measure (realMixedSpace K)) fun (x : realMixedSpace K) ↦
    f ((Homeomorph.symm (mixedSpaceToRealMixedSpace K) : (a : realMixedSpace K) → mixedSpace K) x))
Tactic: rw [← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).integral_comp
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding, ← integral_comp_polarCoordReal_symm,
    polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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 _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K))))
      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)))
    (@integral _ _ _ _ Prod.instMeasurableSpace (volume : Measure (realMixedSpace K)) fun (x : realMixedSpace K) ↦
      f ((Homeomorph.symm (mixedSpaceToRealMixedSpace K) : (a : realMixedSpace K) → mixedSpace K) x))
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K))))
      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)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : mixedSpace K) ↦ f x)
have rw₁ : Eq.{u_2 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K))))
    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)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (restrict volume (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarCoordReal K))))
    fun (x : realMixedSpace K) ↦
    HSMul.hSMul (α := ℝ) (∏ w : { w : InfinitePlace K // w.IsComplex }, (x.2 w).1)
      (f
        ((Homeomorph.symm (mixedSpaceToRealMixedSpace K) : (a : realMixedSpace K) → mixedSpace K)
          ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x))))
Tactic: rw [← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).integral_comp
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding, ← integral_comp_polarCoordReal_symm,
    polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq, Function.comp_def]
-- 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 : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x) =
    ∫⁻ (x : mixedSpace K), f x
have rw : ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K)),
    (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x) =
  ∫⁻ (a : realMixedSpace K),
    f
      ((Homeomorph.symm (mixedSpaceToRealMixedSpace K) : (a : realMixedSpace K) → mixedSpace K)
        a) ∂(volume : Measure (realMixedSpace K))
Tactic: rw [← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).lintegral_comp_emb
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding, ← lintegral_comp_polarCoordReal_symm,
    polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq, Function.comp_def]
-- 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∞
rw :
  ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x) =
    ∫⁻ (a : realMixedSpace K),
      f
        ((Homeomorph.symm (mixedSpaceToRealMixedSpace K) : (a : realMixedSpace K) → mixedSpace K)
          a) ∂(volume : Measure (realMixedSpace K))
⊢ ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x) =
    ∫⁻ (x : mixedSpace K), f x
have rw₁ : ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K)),
    (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
      f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace 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
        ((Homeomorph.symm (mixedSpaceToRealMixedSpace K) : (a : realMixedSpace K) → mixedSpace K)
          ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x))
Tactic: rw [← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).lintegral_comp_emb
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding, ← lintegral_comp_polarCoordReal_symm,
    polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq, Function.comp_def]
-- 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∞
rw :
  ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x) =
    ∫⁻ (a : realMixedSpace K),
      f
        ((Homeomorph.symm (mixedSpaceToRealMixedSpace K) : (a : realMixedSpace K) → mixedSpace K)
          a) ∂(volume : Measure (realMixedSpace K))
rw₁ :
  ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace 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
          ((Homeomorph.symm (mixedSpaceToRealMixedSpace K) : (a : realMixedSpace K) → mixedSpace K)
            ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x))
⊢ ∫⁻ (x : realMixedSpace K) in PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (mixedEmbedding.polarCoord K)),
      (∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x.2 w).1) *
        f ((↑(OpenPartialHomeomorph.symm (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace K) x) =
    ∫⁻ (x : mixedSpace K), f x
have 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 (mixedEmbedding.polarCoord K)) : realMixedSpace K → mixedSpace 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
        ((Homeomorph.symm (mixedSpaceToRealMixedSpace K) : (a : realMixedSpace K) → mixedSpace K)
          ((↑(OpenPartialHomeomorph.symm (polarCoordReal K)) : realMixedSpace K → realMixedSpace K) x))
Tactic: rw [← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).lintegral_comp_emb
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding, ← lintegral_comp_polarCoordReal_symm,
    polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
⊢ 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)
have 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 sorry)).1
Tactic: refine .prodMk (continuous_pi fun w ↦ ?_) (by fun_prop)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
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
have pos : ∀ (h : w.IsReal),
  Continuous (Y := ℝ) fun (a : realMixedSpace K) ↦ a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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)
⊢ 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
have neg : ∀ (h : ¬w.IsReal),
  Continuous (Y := ℝ) fun (a : realMixedSpace K) ↦
    (a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)).1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
x : realMixedSpace K
w : { w : InfinitePlace K // w.IsReal }
⊢ ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).1 (↑w : InfinitePlace K) = x.1 w
have 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) sorry)).1) =
  x.1 w
Tactic: simp_rw [homeoRealMixedSpacePolarSpace_apply, dif_pos w.prop]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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).1 (↑w : InfinitePlace K) = (x.2 w).1
have 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) sorry)).1) =
  (x.2 w).1
Tactic: simp_rw [homeoRealMixedSpacePolarSpace_apply, dif_neg (not_isReal_iff_isComplex.mpr w.prop)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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 (-π) π)
have 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 (-π) π)
Tactic: ext
-- 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
⊢ 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 (-π) π)
have h : Membership.mem (γ := Set (polarSpace K))
    ((⇑(Homeomorph.symm (homeoRealMixedSpacePolarSpace K)) : (a : polarSpace K) → realMixedSpace K) ⁻¹'
      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))
    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 (-π) π)
Tactic: simp_rw [polarSpaceCoord_target, Set.mem_preimage, homeoRealMixedSpacePolarSpace_symm_apply,
    Set.mem_prod, Set.mem_univ, true_and, Set.mem_univ_pi, Set.mem_ite_univ_left,
    not_isReal_iff_isComplex, Subtype.forall, Complex.polarCoord_target, Set.mem_prod, forall_and]
-- 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
h :
  Membership.mem (γ := Set (polarSpace K))
      ((⇑(Homeomorph.symm (homeoRealMixedSpacePolarSpace K)) : (a : polarSpace K) → realMixedSpace K) ⁻¹'
        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))
      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 (-π) π)
⊢ 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 (-π) π)
have h₁ : Membership.mem (α := realMixedSpace K)
    (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))
    ((Homeomorph.symm (homeoRealMixedSpacePolarSpace K) : (a : polarSpace K) → realMixedSpace K) x : realMixedSpace K) ↔
  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 (-π) π)
Tactic: simp_rw [polarSpaceCoord_target, Set.mem_preimage, homeoRealMixedSpacePolarSpace_symm_apply,
    Set.mem_prod, Set.mem_univ, true_and, Set.mem_univ_pi, Set.mem_ite_univ_left,
    not_isReal_iff_isComplex, Subtype.forall, Complex.polarCoord_target, Set.mem_prod, forall_and]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ 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)
have 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)))
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]