-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor 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 B else 1)
have₁ :
  ∀
    (this :
      minkowskiBound K 1 <
        ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (convexBodyLT K fun (w : InfinitePlace K) ↦ if w = w₀ then B else 1)),
    ∃ (a : 𝓞 K),
      Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
        ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)
have₂ :
  minkowskiBound K 1 <
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (convexBodyLT K fun (w : InfinitePlace K) ↦ if w = w₀ then B else 1)
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 B else 1)),
    ∃ (a : 𝓞 K),
      Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
        ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)
have₅ :
  ∀
    (this :
      minkowskiBound K 1 <
        ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (convexBodyLT K fun (w : InfinitePlace K) ↦ if w = w₀ then B else 1))
    (a : 𝓞 K) (h_nz : a ≠ 0)
    (h_le : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(if w = w₀ then B else 1) : ℝ)),
    ∃ (a : 𝓞 K),
      Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
        ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)
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 B else 1))
    (a : 𝓞 K) (h_nz : a ≠ 0)
    (h_le : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(if w = w₀ then B else 1) : ℝ)),
    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 B else 1))
    (a : 𝓞 K) (h_nz : a ≠ 0)
    (h_le : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(if w = w₀ then B else 1) : ℝ))
    (w : InfinitePlace K), (↑(if w = w₀ then B else 1) : ℝ) ≤ (↑(max B 1) : ℝ)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)

Tactic:
classical
  have : minkowskiBound K ↑1 < volume (convexBodyLT K (fun w ↦ if w = w₀ then B else 1)) := 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, hw₀, ite_true, one_mul, pow_one]
    exact hB
  obtain ⟨a, h_nz, h_le⟩ := exists_ne_zero_mem_ringOfIntegers_lt K this
  refine ⟨a, ?_, fun w ↦ lt_of_lt_of_le (h_le w) ?_⟩
  · exact is_primitive_element_of_infinitePlace_lt h_nz
      (fun w h_ne ↦ by convert! (if_neg h_ne) ▸ h_le w) (Or.inl hw₀)
  · split_ifs <;> simp