-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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)⟯ ⊤
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)
have 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) : ℝ)
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