-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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) : ℝ)
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 ⋯ :
                (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) : ℝ)
simp_rw₇ :
  ((∀ (i : { w : InfinitePlace K // w.IsReal }),
        norm (E := ℝ) ((embedding_of_isReal ⋯ : (a : K) → ℝ) x : ℝ) < (↑(f (↑i : InfinitePlace K)) : ℝ)) ∧
      ∀ (i : { w : InfinitePlace K // w.IsComplex }),
        norm (E := ℂ) (((↑i : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ) < (↑(f (↑i : InfinitePlace K)) : ℝ)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₈ :
  ((∀ (i : { w : InfinitePlace K // w.IsReal }),
        ‖(↑((embedding_of_isReal ⋯ : (a : K) → ℝ) x) : ℂ)‖ < (↑(f (↑i : InfinitePlace K)) : ℝ)) ∧
      ∀ (i : { w : InfinitePlace K // w.IsComplex }),
        norm (E := ℂ) (((↑i : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ) < (↑(f (↑i : InfinitePlace K)) : ℝ)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₉ :
  ((∀ (i : { w : InfinitePlace K // w.IsReal }),
        norm (E := ℂ) (((↑i : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ) < (↑(f (↑i : InfinitePlace K)) : ℝ)) ∧
      ∀ (i : { w : InfinitePlace K // w.IsComplex }),
        norm (E := ℂ) (((↑i : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ) < (↑(f (↑i : InfinitePlace K)) : ℝ)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₁₀ :
  ((∀ (a : InfinitePlace K) (b : a.IsReal), norm (E := ℂ) ((a.embedding : (a : K) → ℂ) x : ℂ) < (↑(f a) : ℝ)) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex), norm (E := ℂ) ((a.embedding : (a : K) → ℂ) x : ℂ) < (↑(f a) : ℝ)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₁₁ :
  (∀ (x_1 : InfinitePlace K),
      x_1.IsReal ∨ x_1.IsComplex → norm (E := ℂ) ((x_1.embedding : (a : K) → ℂ) x : ℂ) < (↑(f x_1) : ℝ)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₁₂ :
  (∀ (x_1 : InfinitePlace K),
      x_1.IsReal ∨ ¬x_1.IsReal → norm (E := ℂ) ((x_1.embedding : (a : K) → ℂ) x : ℂ) < (↑(f x_1) : ℝ)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₁₃ :
  (∀ (x_1 : InfinitePlace K), True → norm (E := ℂ) ((x_1.embedding : (a : K) → ℂ) x : ℂ) < (↑(f x_1) : ℝ)) ↔
    ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
simp_rw₁₄ :
  (∀ (x_1 : InfinitePlace K), norm (E := ℂ) ((x_1.embedding : (a : K) → ℂ) x : ℂ) < (↑(f x_1) : ℝ)) ↔
    ∀ (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) : ℝ)

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]

Premises used: forall_true_left, NumberField.mixedEmbedding, NumberField.InfinitePlace.norm_embedding_eq, forall₂_or_left, em, Subtype.forall, Set.mem_pi, Complex.norm_real, NumberField.InfinitePlace.embedding_of_isReal_apply, Set.mem_prod, Set.mem_univ, Pi.ringHom_apply, NumberField.InfinitePlace.not_isReal_iff_isComplex, RingHom.prod_apply, mem_ball_zero_iff