awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
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
pos₁ : HPow.hPow (β := ℕ) (Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 < HPow.hPow (β := ℕ) (↑B : ℝ) 2
⊢ 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:
refine add_lt_add ?_ ?_

Premises used: add_lt_add
-- 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∞)
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 : |Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))| < 1
⊢ HPow.hPow (β := ℕ) (Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 < 1

Tactic:
rw [← sq_abs, sq_lt_one_iff₀ (abs_nonneg _)]

Premises used: sq_lt_one_iff₀, sq_abs
-- 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∞)
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₀
⊢ |Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))| < 1

Tactic:
h_le₀.1

Premises used: And.left
-- 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∞)
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₀
⊢ |Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))| < 1

Tactic:
exact h_le₀.1

Premises used: And.left
-- 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∞)
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 :
  |Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))| <
    (↑(HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) 2) : ℝ)
⊢ HPow.hPow (β := ℕ) (Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 < HPow.hPow (β := ℕ) (↑B : ℝ) 2

Tactic:
rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]

Premises used: sq_lt_sq, NNReal.abs_eq, NNReal.sq_sqrt
-- 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∞)
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₀
⊢ |Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))| <
    (↑(HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) 2) : ℝ)

Tactic:
h_le₀.2

Premises used: And.right, NNReal.toReal
-- 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∞)
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₀
⊢ |Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))| <
    (↑(HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) 2) : ℝ)

Tactic:
exact h_le₀.2

Premises used: And.right
-- 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∞)
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)

Tactic:
lt_of_lt_of_le (if_neg h_eq ▸ h_le w h_eq) ?_

Premises used: lt_of_lt_of_le
-- 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∞)
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₀
neg : (↑1 : ℝ) ≤ √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
⊢ (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)

Tactic:
refine lt_of_lt_of_le (if_neg h_eq ▸ h_le w h_eq) ?_

Premises used: lt_of_lt_of_le
-- 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∞)
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₀
neg : 1 ≤ 1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2
⊢ (↑1 : ℝ) ≤ √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)

Tactic:
rw [NNReal.coe_one, Real.le_sqrt' zero_lt_one, one_pow]

Premises used: one_pow, Real.le_sqrt', zero_lt_one, NNReal.coe_one
-- 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∞)
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

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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)
contrapose! :
  ∀ (h : B < 0),
    ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) < minkowskiBound K I
⊢ 0 ≤ B

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : B < 0
rw : 0 < minkowskiBound K I
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B) < minkowskiBound K I

Tactic:
rw [convexBodySum_volume_eq_zero_of_le_zero K (le_of_lt h)]

Premises used: NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, le_of_lt
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : B < 0
⊢ 0 < minkowskiBound K I

Tactic:
minkowskiBound_pos K I

Premises used: NumberField.mixedEmbedding.minkowskiBound_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : B < 0
⊢ 0 < minkowskiBound K I

Tactic:
exact minkowskiBound_pos K I

Premises used: NumberField.mixedEmbedding.minkowskiBound_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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

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
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
⊢ LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹

Tactic:
have h1 : 0 < (finrank ℚ K : ℝ)⁻¹ := inv_pos.mpr (Nat.cast_pos.mpr finrank_pos)
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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) : ℝ)⁻¹
⊢ 0 ≤ B / (↑(finrank ℚ K) : ℝ)

Tactic:
have h2 : 0 ≤ B / (finrank ℚ K) := div_nonneg hB (Nat.cast_nonneg _)
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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) : ℝ)
⊢ 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
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
⊢ Countable.{u_1 + 1}
    ↥(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:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
⊢ 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
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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)
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
⊢ ∃ (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

Premises used: NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, OfNat.ofNat