-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ 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 (-π) π)
have 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
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]