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₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor 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 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
pos : w = w₀ → (↑B : ℝ) ≤ (↑(max B 1) : ℝ)
neg : ¬w = w₀ → (↑1 : ℝ) ≤ (↑(max B 1) : ℝ)
⊢ (↑(if w = w₀ then B else 1) : ℝ) ≤ (↑(max B 1) : ℝ)

Tactic:
split_ifs
-- 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∞)
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
h : w = w₀
⊢ (↑B : ℝ) ≤ (↑(max B 1) : ℝ)

Tactic:
simp
-- 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∞)
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
h : ¬w = w₀
⊢ (↑1 : ℝ) ≤ (↑(max B 1) : ℝ)

Tactic:
simp
-- 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∞)
rw :
  minkowskiBound K 1 <
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) *
      (↑((∏ x ∈ Finset.erase Finset.univ w₀,
              HPow.hPow (α := ℝ≥0) (if x = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1 : ℝ≥0) x.mult) *
            HPow.hPow (α := ℝ≥0) (if w₀ = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1 : ℝ≥0) w₀.mult) :
        ℝ≥0∞)
⊢ 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:
rw [convexBodyLT'_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]

Premises used: Finset.mem_univ, Finset.prod_erase_mul, NumberField.mixedEmbedding.convexBodyLT'_volume
-- 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∞)
simp_rw :
  minkowskiBound K 1 <
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) *
      (↑((∏ x ∈ Finset.erase Finset.univ w₀,
              if x = w₀ then HPow.hPow (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) x.mult else 1) *
            if True then HPow.hPow (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) w₀.mult else 1) :
        ℝ≥0∞)
⊢ minkowskiBound K 1 <
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) *
      (↑((∏ x ∈ Finset.erase Finset.univ w₀,
              HPow.hPow (α := ℝ≥0) (if x = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1 : ℝ≥0) x.mult) *
            HPow.hPow (α := ℝ≥0) (if w₀ = w₀ then (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B else 1 : ℝ≥0) w₀.mult) :
        ℝ≥0∞)

Tactic:
simp_rw [ite_pow, one_pow]

Premises used: one_pow, ite_pow
-- 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∞)
rw :
  minkowskiBound K 1 <
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) *
      (↑((if w₀ ∈ Finset.erase Finset.univ w₀ then
              HPow.hPow (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) w₀.mult
            else 1) *
            if True then HPow.hPow (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) w₀.mult else 1) :
        ℝ≥0∞)
⊢ minkowskiBound K 1 <
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) *
      (↑((∏ x ∈ Finset.erase Finset.univ w₀,
              if x = w₀ then HPow.hPow (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) x.mult else 1) *
            if True then HPow.hPow (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) w₀.mult else 1) :
        ℝ≥0∞)

Tactic:
rw [Finset.prod_ite_eq']

Premises used: Finset.prod_ite_eq'
-- 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 simp_rw : minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
⊢ minkowskiBound K 1 <
    (↑(convexBodyLT'Factor K) : ℝ≥0∞) *
      (↑((if w₀ ∈ Finset.erase Finset.univ w₀ then
              HPow.hPow (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) w₀.mult
            else 1) *
            if True then HPow.hPow (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) B : ℝ≥0) w₀.mult else 1) :
        ℝ≥0∞)

Tactic:
simp_rw [Finset.notMem_erase, ite_false, mult, not_isReal_iff_isComplex.mpr hw₀,
      ite_true, ite_false, one_mul, NNReal.sq_sqrt]

Premises used: Iff.mpr, ite_false, NumberField.InfinitePlace.mult, ite_true, NumberField.InfinitePlace.not_isReal_iff_isComplex, Finset.notMem_erase, one_mul, 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∞)
⊢ minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)

Tactic:
hB
-- 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∞)
⊢ minkowskiBound K 1 < (↑(convexBodyLT'Factor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)

Tactic:
exact hB
-- 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∞)
⊢ 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:
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
-- 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₀))
obtain :
  ∀ (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),
    ∃ (a : 𝓞 K),
      Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
        ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)

Tactic:
obtain ⟨a, h_nz, h_le, h_le₀⟩ := exists_ne_zero_mem_ringOfIntegers_lt' K ⟨w₀, hw₀⟩ this

Premises used: NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt', Subtype.mk
-- 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
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)

Tactic:
⟨a, ?_, fun w ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- 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
refine_1 : Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤
refine_2 : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)

Tactic:
refine ⟨a, ?_, fun w ↦ ?_⟩
-- 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_ne : w ≠ (↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w₀ hw₀) : InfinitePlace K)
⊢ LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)

Tactic:
convert! if_neg h_ne ▸ h_le w h_ne
-- 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
⊢ Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤

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

Premises used: NumberField.is_primitive_element_of_infinitePlace_lt, And.left, Or.inr
-- 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
pos : ∀ (h_eq : w = w₀), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
neg : ∀ (h_eq : ¬w = w₀), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
⊢ (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)

Tactic:
by_cases h_eq : w = w₀
-- 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₀
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)
⊢ (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)

Tactic:
rw [if_pos rfl] at h_le₀

Premises used: if_pos, rfl
-- 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₀
⊢ 0 ≤
    HPow.hPow (β := ℕ) (Complex.re ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 +
      HPow.hPow (β := ℕ) (Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2

Tactic:
positivity
-- 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 +
      HPow.hPow (β := ℕ) (Complex.im ((w₀.embedding : (a : K) → ℂ) (↑a : K))) 2 <
    1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2
⊢ (w : (a : K) → ℝ) (↑a : K) < √(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)]

Premises used: NumberField.InfinitePlace.norm_embedding_eq, Real.sq_sqrt, NumberField.InfinitePlace.embedding, Complex.norm_add_mul_I, Real.lt_sqrt, Complex.re_add_im, DFunLike.coe, norm_nonneg
-- 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₀
⊢ 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:
add_lt_add ?_ ?_

Premises used: add_lt_add