-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem exists_primitive_element_lt_of_isReal {w₀ : InfinitePlace K} (hw₀ : IsReal w₀) {B : ℝ≥0}
    (hB : minkowskiBound K ↑1 < convexBodyLTFactor K * B) :
    ∃ a : 𝓞 K, ℚ⟮(a : K)⟯ = ⊤ ∧
      ∀ w : InfinitePlace K, w a < max B 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(B ⊔ 1)

Tactic:
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.not_mem_erase, ite_false, mult, hw₀, ite_true, one_mul, pow_one]
  exact hB

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(B ⊔ 1)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)

Tactic:
rw [convexBodyLT_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, (if x = w₀ then B else 1) ^ x.mult) * (if w₀ = w₀ then B else 1) ^ w₀.mult)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(B ⊔ 1)

Tactic:
obtain ⟨a, h_nz, h_le⟩ := exists_ne_zero_mem_ringOfIntegers_lt K this

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(B ⊔ 1)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B

Tactic:
exact hB

Result:
no goals

Proof state:
case intro.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)
⊢ ℚ⟮↑a⟯ = ⊤

Tactic:
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₀)

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(B ⊔ 1)

Tactic:
refine ⟨a, ?_, fun w ↦ lt_of_lt_of_le (h_le w) ?_⟩

Result:
case intro.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)
⊢ ℚ⟮↑a⟯ = ⊤

case intro.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)
w : InfinitePlace K
⊢ ↑(if w = w₀ then B else 1) ≤ ↑(B ⊔ 1)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)
w : InfinitePlace K
h_ne : w ≠ w₀
⊢ w ↑a < 1

Tactic:
convert (if_neg h_ne) ▸ h_le w

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((if w₀ ∈ Finset.univ.erase w₀ then B ^ w₀.mult else 1) * if True then B ^ w₀.mult else 1)

Tactic:
simp_rw [Finset.not_mem_erase, ite_false, mult, hw₀, ite_true, one_mul, pow_one]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, (if x = w₀ then B else 1) ^ x.mult) * (if w₀ = w₀ then B else 1) ^ w₀.mult)

Tactic:
simp_rw [ite_pow, one_pow]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, if x = w₀ then B ^ x.mult else 1) * if True then B ^ w₀.mult else 1)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, if x = w₀ then B ^ x.mult else 1) * if True then B ^ w₀.mult else 1)

Tactic:
rw [Finset.prod_ite_eq']

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((if w₀ ∈ Finset.univ.erase w₀ then B ^ w₀.mult else 1) * if True then B ^ w₀.mult else 1)

Proof state:
case intro.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w => if w = w₀ then B else 1)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)
w : InfinitePlace K
⊢ ↑(if w = w₀ then B else 1) ≤ ↑(B ⊔ 1)

Tactic:
split_ifs <;> simp

Result:
no goals