awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
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
h_eq : w = w₀
⊢ (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have pos : ∀
  (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 (β := ℕ) (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B) : ℝ) 2)
  (w : InfinitePlace K) (h_eq : w = w₀), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
Tactic: rw [if_pos rfl] at h_le₀
Cleared hypotheses: h_le₀, w, h_eq
-- 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
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 ((w₀.embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
    |Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))| <
      HPow.hPow (β := ℕ) (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B) : ℝ) 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have pos : HPow.hPow (β := ℕ) (Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 +
    HPow.hPow (β := ℕ) (Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 <
  1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2
Tactic: 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)]
-- 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
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 ((w₀.embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
    |Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))| <
      HPow.hPow (β := ℕ) (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B) : ℝ) 2
w : InfinitePlace K
h_eq : w = w₀
⊢ HPow.hPow (β := ℕ) (Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 +
      HPow.hPow (β := ℕ) (Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 <
    1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2
have pos : HPow.hPow (β := ℕ) (Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 < 1
Tactic: refine add_lt_add ?_ ?_
-- 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
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 ((w₀.embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
    |Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))| <
      HPow.hPow (β := ℕ) (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B) : ℝ) 2
w : InfinitePlace K
h_eq : w = w₀
pos : HPow.hPow (β := ℕ) (Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 < 1
⊢ HPow.hPow (β := ℕ) (Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 +
      HPow.hPow (β := ℕ) (Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 <
    1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2
have pos₁ : HPow.hPow (β := ℕ) (Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 < HPow.hPow (β := ℕ) (↑B : ℝ) 2
Tactic: refine add_lt_add ?_ ?_
-- 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
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 ((w₀.embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
    |Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))| <
      HPow.hPow (β := ℕ) (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B) : ℝ) 2
w : InfinitePlace K
h_eq : w = w₀
⊢ HPow.hPow (β := ℕ) (Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 < 1
have pos : |Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))| < 1
Tactic: rw [← sq_abs, sq_lt_one_iff₀ (abs_nonneg _)]
-- 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
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 ((w₀.embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
    |Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))| <
      HPow.hPow (β := ℕ) (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B) : ℝ) 2
w : InfinitePlace K
h_eq : w = w₀
⊢ HPow.hPow (β := ℕ) (Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 < HPow.hPow (β := ℕ) (↑B : ℝ) 2
have pos : |Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))| <
  (↑(HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) 2) : ℝ)
Tactic: rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]
-- 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
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
h_eq : ¬w = w₀
⊢ (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have neg : (↑1 : ℝ) ≤ √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
Tactic: refine lt_of_lt_of_le (if_neg h_eq ▸ h_le w h_eq) ?_
-- 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
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
h_eq : ¬w = w₀
⊢ (↑1 : ℝ) ≤ √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have neg : 1 ≤ 1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2
Tactic: rw [NNReal.coe_one, Real.le_sqrt' zero_lt_one, one_pow]
-- 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have 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₀))
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
-- 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₀.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₀))
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
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)
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
⊢ 0 ≤ B
have contrapose! : ∀ (h : B < 0),
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) < minkowskiBound K I
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : B < 0
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) < minkowskiBound K I
have rw : 0 < minkowskiBound K I
Tactic: rw [convexBodySum_volume_eq_zero_of_le_zero K (le_of_lt h)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
have hB : 0 ≤ B
Tactic: have hB : 0 ≤ B := by
    contrapose! h
    rw [convexBodySum_volume_eq_zero_of_le_zero K (le_of_lt h)]
    exact minkowskiBound_pos K I
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
hB : 0 ≤ B
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
have h1 : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹
Tactic: have h1 : 0 < (finrank ℚ K : ℝ)⁻¹ := inv_pos.mpr (Nat.cast_pos.mpr finrank_pos)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
hB : 0 ≤ B
h1 : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
have h2 : 0 ≤ B / (↑(finrank ℚ K) : ℝ)
Tactic: have h2 : 0 ≤ B / (finrank ℚ K) := div_nonneg hB (Nat.cast_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
hB : 0 ≤ B
h1 : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹
h2 : 0 ≤ B / (↑(finrank ℚ K) : ℝ)
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
have h_fund : IsAddFundamentalDomain.{u_1, u_1}
  ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
      (span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                  (mixedSpace K)) :
            (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
  (α := mixedSpace K)
  (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
    (fractionalIdealLatticeBasis K I))
  volume
Tactic: have h_fund := ZSpan.isAddFundamentalDomain' (fractionalIdealLatticeBasis K I) volume
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
hB : 0 ≤ B
h1 : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹
h2 : 0 ≤ B / (↑(finrank ℚ K) : ℝ)
h_fund :
  IsAddFundamentalDomain.{u_1, u_1}
    ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
        (span ℤ
          (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(fractionalIdealLatticeBasis K I :
                  Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                    (mixedSpace K)) :
              (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
    (α := mixedSpace K)
    (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
      (fractionalIdealLatticeBasis K I))
    volume
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
have this : Countable.{u_1 + 1}
  ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
      (span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                  (mixedSpace K)) :
            (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
Tactic: have : Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I))).toAddSubgroup := by
    change Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I)))
    infer_instance
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
have obtain : ∀ (w : K) (h_mem : Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K) w)
  (h_nz : w ≠ 0) (h_bd : (↑|(Algebra.norm ℚ : (a : K) → ℚ) w| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K),
  ∃ (a : 𝓞 K), a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
Tactic: obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_of_norm_le K ↑1 h