-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : mixedSpace K → ℝ≥0∞
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)
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
          (x.1,
            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 : ℝ × ℝ → ℂ)) x.2)
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 }) ↦ a.1 w,
            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
          (x.1,
            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 : ℝ × ℝ → ℂ)) x.2)
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),
      (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a.2 x).1) *
        f
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ a.1 w,
            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 }) ↦
              ((a.2 w).1, ((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
          (x.1,
            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 : ℝ × ℝ → ℂ)) x.2)
⊢ ∫⁻ (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:
simp_rw [polarSpaceCoord_symm_apply, mixedEmbedding.polarCoord_symm_apply,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, homeoRealMixedSpacePolarSpace_apply_snd]

Premises used: NumberField.mixedEmbedding.polarCoord_symm_apply, NumberField.mixedEmbedding.polarSpaceCoord_symm_apply, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_snd