-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : polarSpace K
h :
  Membership.mem (γ := Set (polarSpace K))
      ((⇑(Homeomorph.symm (homeoRealMixedSpacePolarSpace K)) : (a : polarSpace K) → realMixedSpace K) ⁻¹'
        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 ↔
    x ∈
      SProd.sprod (α := Set ((i : InfinitePlace K) → ℝ)) (β := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0)
        (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π)
h₁ :
  Membership.mem (α := realMixedSpace K)
      (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))
      ((Homeomorph.symm (homeoRealMixedSpacePolarSpace K) : (a : polarSpace K) → realMixedSpace K) x :
        realMixedSpace K) ↔
    x ∈
      SProd.sprod (α := Set ((i : InfinitePlace K) → ℝ)) (β := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0)
        (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π)
h₂ :
  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x.1 (↑w : InfinitePlace K),
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x.1 (↑w : InfinitePlace K), x.2 w)) ∈
      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 ∈
      SProd.sprod (α := Set ((i : InfinitePlace K) → ℝ)) (β := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0)
        (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π)
h₃ :
  ((Membership.mem (γ := Set ({ w : InfinitePlace K // w.IsReal } → ℝ)) Set.univ
        fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x.1 (↑w : InfinitePlace K)) ∧
      Membership.mem (γ := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ))
        (Set.pi (α := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) Set.univ
          fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ Complex.polarCoord.target)
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x.1 (↑w : InfinitePlace K), x.2 w)) ↔
    Membership.mem (γ := Set ((i : InfinitePlace K) → ℝ))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0)
        x.1 ∧
      Membership.mem (γ := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ))
        (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π)
        x.2
h₄ :
  (True ∧
      Membership.mem (γ := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ))
        (Set.pi (α := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) Set.univ
          fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ Complex.polarCoord.target)
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x.1 (↑w : InfinitePlace K), x.2 w)) ↔
    Membership.mem (γ := Set ((i : InfinitePlace K) → ℝ))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0)
        x.1 ∧
      Membership.mem (γ := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ))
        (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π)
        x.2
h₅ :
  (Membership.mem (γ := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ × ℝ))
      (Set.pi (α := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ × ℝ) Set.univ
        fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ Complex.polarCoord.target)
      fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x.1 (↑w : InfinitePlace K), x.2 w)) ↔
    Membership.mem (γ := Set ((i : InfinitePlace K) → ℝ))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0)
        x.1 ∧
      Membership.mem (γ := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ))
        (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π)
        x.2
h₆ :
  (∀ (i : { w : InfinitePlace K // w.IsComplex }), (x.1 (↑i : InfinitePlace K), x.2 i) ∈ Complex.polarCoord.target) ↔
    (∀ (i : InfinitePlace K), Membership.mem (γ := Set ℝ) (if i.IsReal then Set.univ else Set.Ioi 0) (x.1 i)) ∧
      ∀ (i : { w : InfinitePlace K // w.IsComplex }), x.2 i ∈ Set.Ioo (-π) π
h₇ :
  (∀ (i : { w : InfinitePlace K // w.IsComplex }), (x.1 (↑i : InfinitePlace K), x.2 i) ∈ Complex.polarCoord.target) ↔
    (∀ (i : InfinitePlace K), ¬i.IsReal → Membership.mem (γ := Set ℝ) (Set.Ioi 0) (x.1 i)) ∧
      ∀ (i : { w : InfinitePlace K // w.IsComplex }), x.2 i ∈ Set.Ioo (-π) π
h₈ :
  (∀ (i : { w : InfinitePlace K // w.IsComplex }), (x.1 (↑i : InfinitePlace K), x.2 i) ∈ Complex.polarCoord.target) ↔
    (∀ (i : InfinitePlace K), i.IsComplex → Membership.mem (γ := Set ℝ) (Set.Ioi 0) (x.1 i)) ∧
      ∀ (i : { w : InfinitePlace K // w.IsComplex }), x.2 i ∈ Set.Ioo (-π) π
h₉ :
  (∀ (a : InfinitePlace K) (b : a.IsComplex),
      (x.1 a, x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)) ∈ Complex.polarCoord.target) ↔
    (∀ (i : InfinitePlace K), i.IsComplex → Membership.mem (γ := Set ℝ) (Set.Ioi 0) (x.1 i)) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex),
        x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b) ∈ Set.Ioo (-π) π
h₁₀ :
  (∀ (a : InfinitePlace K) (b : a.IsComplex),
      (x.1 a, x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)) ∈
        SProd.sprod (α := Set ℝ) (Set.Ioi 0) (Set.Ioo (-π) π)) ↔
    (∀ (i : InfinitePlace K), i.IsComplex → Membership.mem (γ := Set ℝ) (Set.Ioi 0) (x.1 i)) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex),
        x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b) ∈ Set.Ioo (-π) π
h₁₁ :
  (∀ (a : InfinitePlace K) (b : a.IsComplex),
      Membership.mem (γ := Set ℝ) (Set.Ioi 0) (x.1 a) ∧
        x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b) ∈ Set.Ioo (-π) π) ↔
    (∀ (i : InfinitePlace K), i.IsComplex → Membership.mem (γ := Set ℝ) (Set.Ioi 0) (x.1 i)) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex),
        x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b) ∈ Set.Ioo (-π) π
⊢ Membership.mem (γ := Set (polarSpace K))
      (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (polarSpaceCoord K))) x ↔
    x ∈
      SProd.sprod (α := Set ((i : InfinitePlace K) → ℝ)) (β := Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℝ))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0)
        (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ Set.Ioo (-π) π)

Tactic:
simp_rw [polarSpaceCoord_target, Set.mem_preimage, homeoRealMixedSpacePolarSpace_symm_apply,
    Set.mem_prod, Set.mem_univ, true_and, Set.mem_univ_pi, Set.mem_ite_univ_left,
    not_isReal_iff_isComplex, Subtype.forall, Complex.polarCoord_target, Set.mem_prod, forall_and]

Premises used: NumberField.mixedEmbedding.polarSpaceCoord_target, Subtype.forall, Set.mem_prod, Set.mem_univ, Set.mem_ite_univ_left, NumberField.InfinitePlace.not_isReal_iff_isComplex, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_symm_apply, Complex.polarCoord_target, Set.mem_univ_pi, Set.mem_preimage, true_and, forall_and