-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
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
simp_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
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦
            ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).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) x).1 (↑w : InfinitePlace K),
                ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).2 w))))
    (@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)))
simp_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
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦
            ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).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) x).1 (↑w : InfinitePlace K),
                ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).2 w))))
    (@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
          (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₂ :
  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
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x.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) x).1 (↑w : InfinitePlace K),
                ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).2 w))))
    (@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
          (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₃ :
  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 (α := ℝ) (∏ x_1 : { w : InfinitePlace K // w.IsComplex }, (x.2 x_1).1)
        (f
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x.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 }) ↦
              ((x.2 w).1, ((homeoRealMixedSpacePolarSpace K : (a : realMixedSpace K) → polarSpace K) x).2 w))))
    (@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
          (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)))
⊢ 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:
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