-- 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) : ℝ)
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 ⋯ :
              (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) : ℝ)
simp_rw₃ :
  ((∀ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set { w : InfinitePlace K // w.IsReal }) Set.univ i →
          Membership.mem (γ := Set ℝ) (ball 0 (↑(f (↑i : InfinitePlace K)) : ℝ))
            ((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 i)) ∧
      ∀ (i : { w : InfinitePlace K // w.IsComplex }),
        Membership.mem (γ := Set { w : InfinitePlace K // w.IsComplex }) Set.univ i →
          Membership.mem (γ := Set ℂ) (ball 0 (↑(f (↑i : 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 i)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₄ :
  ((∀ (i : { w : InfinitePlace K // w.IsReal }),
        True →
          Membership.mem (γ := Set ℝ) (ball 0 (↑(f (↑i : InfinitePlace K)) : ℝ))
            ((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 i)) ∧
      ∀ (i : { w : InfinitePlace K // w.IsComplex }),
        True →
          Membership.mem (γ := Set ℂ) (ball 0 (↑(f (↑i : 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 i)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₅ :
  ((∀ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set ℝ) (ball 0 (↑(f (↑i : InfinitePlace K)) : ℝ))
          ((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 i)) ∧
      ∀ (i : { w : InfinitePlace K // w.IsComplex }),
        Membership.mem (γ := Set ℂ) (ball 0 (↑(f (↑i : 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 i)) ↔
    ∀ (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₆ : ((∀ (i : { w : InfinitePlace K // w.IsReal }),
      norm (E := ℝ)
          ((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 i) <
        (↑(f (↑i : InfinitePlace K)) : ℝ)) ∧
    ∀ (i : { w : InfinitePlace K // w.IsComplex }),
      norm (E := ℂ)
          ((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 i) <
        (↑(f (↑i : InfinitePlace K)) : ℝ)) ↔
  ∀ (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]