-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
x : K
simp_rw :
  Membership.mem (α := mixedSpace K) (convexBodyLT K f)
      ((RingHom.prod
              (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal ⋯)
              (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding) :
            (a : K) → mixedSpace K)
          x :
        mixedSpace K) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₁ :
  Membership.mem (α := mixedSpace K) (convexBodyLT K f)
      (((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal ⋯ :
              (a : K) → { w : InfinitePlace K // w.IsReal } → ℝ)
            x,
          (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding :
              (a : K) → { w : InfinitePlace K // w.IsComplex } → ℂ)
            x) :
        ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
⊢ Membership.mem (α := mixedSpace K) (convexBodyLT K f) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
have simp_rw₂ : Membership.mem (α := (i : { w : InfinitePlace K // w.IsReal }) → ℝ) (γ :=
      Set ((i : { w : InfinitePlace K // w.IsReal }) → ℝ))
      (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) Set.univ
        fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ball 0 (↑(f (↑w : InfinitePlace K)) : ℝ))
      ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
              fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal sorry :
            (a : K) → { w : InfinitePlace K // w.IsReal } → ℝ)
          x :
        { w : InfinitePlace K // w.IsReal } → ℝ) ∧
    Membership.mem (α := (i : { w : InfinitePlace K // w.IsComplex }) → ℂ) (γ :=
      Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℂ))
      (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ) Set.univ
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ ball 0 (↑(f (↑w : InfinitePlace K)) : ℝ))
      ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
              fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding :
            (a : K) → { w : InfinitePlace K // w.IsComplex } → ℂ)
          x :
        { w : InfinitePlace K // w.IsComplex } → ℂ) ↔
  ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
Tactic: simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ,
    forall_true_left, mem_ball_zero_iff, Pi.ringHom_apply, ← Complex.norm_real,
    embedding_of_isReal_apply, Subtype.forall, ← forall₂_or_left, ← not_isReal_iff_isComplex, em,
    forall_true_left, norm_embedding_eq]