-- 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))
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))
⊢ ∫⁻ (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
        (((⇑(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 (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]