-- 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))
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))))
rw₂ :
  Eq.{u_2 + 1} (α := E)
    (@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 ((↑(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))))
⊢ 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 (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)))
  (@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]