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₀.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) : ℝ)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)
have refine_1 : Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤
Tactic: refine ⟨a, ?_, fun w ↦ lt_of_lt_of_le (h_le w) ?_⟩
-- 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∞)
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) : ℝ)
refine_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 : ∀ (w : InfinitePlace K), (↑(if w = w₀ then B else 1) : ℝ) ≤ (↑(max B 1) : ℝ)
Tactic: refine ⟨a, ?_, fun w ↦ lt_of_lt_of_le (h_le w) ?_⟩
-- 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∞)
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) : ℝ)
have pos : w = w₀ → (↑B : ℝ) ≤ (↑(max B 1) : ℝ)
Tactic: split_ifs
-- 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∞)
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) : ℝ)
⊢ (↑(if w = w₀ then B else 1) : ℝ) ≤ (↑(max B 1) : ℝ)
have neg : ¬w = w₀ → (↑1 : ℝ) ≤ (↑(max B 1) : ℝ)
Tactic: split_ifs
-- 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∞)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)
have 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)
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
-- 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)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 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) : ℝ)
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
-- 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) : ℝ)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 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) (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) : ℝ)
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
-- 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) : ℝ)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)
have 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)⟯ ⊤
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
-- 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∞)
⊢ 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₀))
have 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∞)
Tactic: rw [convexBodyLT'_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
-- 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∞)
⊢ 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∞)
have 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∞)
Tactic: simp_rw [ite_pow, 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∞)
⊢ 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∞)
have 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∞)
Tactic: rw [Finset.prod_ite_eq']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
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 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₀))
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
-- 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),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have 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)
Tactic: obtain ⟨a, h_nz, h_le, h_le₀⟩ := exists_ne_zero_mem_ringOfIntegers_lt' K ⟨w₀, hw₀⟩ this
-- 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
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have refine_1 : Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤
Tactic: refine ⟨a, ?_, fun w ↦ ?_⟩
-- 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
refine_1 : Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have refine_2 : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
Tactic: refine ⟨a, ?_, fun w ↦ ?_⟩
-- 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
⊢ (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have pos : ∀ (h_eq : w = w₀), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
Tactic: by_cases h_eq : w = w₀
-- 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
pos : ∀ (h_eq : w = w₀), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
⊢ (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
have neg : ∀ (h_eq : ¬w = w₀), (w : (a : K) → ℝ) (↑a : K) < √(1 + HPow.hPow (β := ℕ) (↑B : ℝ) 2)
Tactic: by_cases h_eq : w = w₀