-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
have :
  minkowskiBound K 1 <
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (convexBodyLT' K (fun (w : InfinitePlace K) ↦ if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1)
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀))
have₁ :
  ∀
    (this :
      minkowskiBound K 1 <
        ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (convexBodyLT' K (fun (w : InfinitePlace K) ↦ if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1)
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀))),
    ∃ (a : 𝓞 K),
      Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
        ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have₂ :
  minkowskiBound K 1 <
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (convexBodyLT' K (fun (w : InfinitePlace K) ↦ if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1)
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀))
have₃ have₄ :
  ∀
    (this :
      minkowskiBound K 1 <
        ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (convexBodyLT' K (fun (w : InfinitePlace K) ↦ if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1)
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀))),
    ∃ (a : 𝓞 K),
      Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
        ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have₅ :
  ∀
    (this :
      minkowskiBound K 1 <
        ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (convexBodyLT' K (fun (w : InfinitePlace K) ↦ if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1)
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀)))
    (a : 𝓞 K) (h_nz : a ≠ 0)
    (h_le :
      ∀ (w : InfinitePlace K),
        w ≠ (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K) →
          (w : (a : K) → ℝ) (↑a : K) < (↑(if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1) : ℝ))
    (h_le₀ :
      |Complex.re
              (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K).embedding :
                  (a : K) → ℂ)
                (↑a : K))| <
          1 ∧
        |Complex.im
              (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K).embedding :
                  (a : K) → ℂ)
                (↑a : K))| <
          HPow.hPow (β := ℕ)
            (↑(if (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K) = w₀ then
                  (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B
                else 1) :
              ℝ)
            2),
    ∃ (a : 𝓞 K),
      Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
        ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
refine_1 :
  ∀
    (this :
      minkowskiBound K 1 <
        ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (convexBodyLT' K (fun (w : InfinitePlace K) ↦ if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1)
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀)))
    (a : 𝓞 K) (h_nz : a ≠ 0)
    (h_le :
      ∀ (w : InfinitePlace K),
        w ≠ (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K) →
          (w : (a : K) → ℝ) (↑a : K) < (↑(if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1) : ℝ))
    (h_le₀ :
      |Complex.re
              (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K).embedding :
                  (a : K) → ℂ)
                (↑a : K))| <
          1 ∧
        |Complex.im
              (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K).embedding :
                  (a : K) → ℂ)
                (↑a : K))| <
          HPow.hPow (β := ℕ)
            (↑(if (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K) = w₀ then
                  (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B
                else 1) :
              ℝ)
            2),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤
refine_2 refine_2₁ :
  ∀
    (this :
      minkowskiBound K 1 <
        ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (convexBodyLT' K (fun (w : InfinitePlace K) ↦ if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1)
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀)))
    (a : 𝓞 K) (h_nz : a ≠ 0)
    (h_le :
      ∀ (w : InfinitePlace K),
        w ≠ (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K) →
          (w : (a : K) → ℝ) (↑a : K) < (↑(if w = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1) : ℝ))
    (h_le₀ :
      |Complex.re
              (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K).embedding :
                  (a : K) → ℂ)
                (↑a : K))| <
          1 ∧
        |Complex.im
              (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K).embedding :
                  (a : K) → ℂ)
                (↑a : K))| <
          HPow.hPow (β := ℕ)
            (↑(if (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K) = w₀ then
                  (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B
                else 1) :
              ℝ)
            2)
    (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)

Tactic:
classical
  have : minkowskiBound K ↑1 <
      volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩) := by
    rw [convexBodyLT'_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
    simp_rw [ite_pow, one_pow]
    rw [Finset.prod_ite_eq']
    simp_rw [Finset.notMem_erase, ite_false, mult, not_isReal_iff_isComplex.mpr hw₀,
      ite_true, ite_false, one_mul, NNReal.sq_sqrt]
    exact hB
  obtain ⟨a, h_nz, h_le, h_le₀⟩ := exists_ne_zero_mem_ringOfIntegers_lt' K ⟨w₀, hw₀⟩ this
  refine ⟨a, ?_, fun w ↦ ?_⟩
  · exact is_primitive_element_of_infinitePlace_lt h_nz
      (fun w h_ne ↦ by convert! if_neg h_ne ▸ h_le w h_ne) (Or.inr h_le₀.1)
  · by_cases h_eq : w = w₀
    · rw [if_pos rfl] at h_le₀
      dsimp only at h_le₀
      rw [h_eq, ← norm_embedding_eq, Real.lt_sqrt (norm_nonneg _), ← Complex.re_add_im
        (embedding w₀ _), Complex.norm_add_mul_I, Real.sq_sqrt (by positivity)]
      refine add_lt_add ?_ ?_
      · rw [← sq_abs, sq_lt_one_iff₀ (abs_nonneg _)]
        exact h_le₀.1
      · rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]
        exact h_le₀.2
    · refine lt_of_lt_of_le (if_neg h_eq ▸ h_le w h_eq) ?_
      rw [NNReal.coe_one, Real.le_sqrt' zero_lt_one, one_pow]
      norm_num

Premises used: sq_lt_one_iff₀, one_pow, NumberField.InfinitePlace.norm_embedding_eq, Real.le_sqrt', Real.sq_sqrt, if_pos, NumberField.InfinitePlace.embedding, zero_lt_one, sq_lt_sq, add_lt_add, Complex.norm_add_mul_I, NNReal.abs_eq, Real.lt_sqrt, sq_abs, NNReal.coe_one, Complex.re_add_im, DFunLike.coe, norm_nonneg, rfl, lt_of_lt_of_le, NNReal.sq_sqrt