-- 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∞
⊢ ∫⁻ (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)
have simp_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
        (fun (w : { w : InfinitePlace K // w.IsReal }) ↦
          ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) a).1 (↑w : InfinitePlace K),
          Pi.map (α := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) (β :=
            fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
            (fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ (↑Complex.polarCoord.symm : ℝ × ℝ → ℂ))
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦
            (((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) a).1 (↑w : InfinitePlace K),
              ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) a).2 w)) ∂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: simp_rw [polarSpaceCoord_symm_apply, mixedEmbedding.polarCoord_symm_apply,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, homeoRealMixedSpacePolarSpace_apply_snd]