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
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
w₀ : { w : InfinitePlace K // w.IsComplex }
h : minkowskiBound K I < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀)
⊢ 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
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
w₀ : { w : InfinitePlace K // w.IsComplex }
h : minkowskiBound K I < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀)
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
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
w₀ : { w : InfinitePlace K // w.IsComplex }
h : minkowskiBound K I < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀)
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
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f)
obtain :
  ∀ (w : K) (h_mem : Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K) w)
    (h_nz : w ≠ 0) (h_bd : ∀ (w_1 : InfinitePlace K), (w_1 : (a : K) → ℝ) w < (↑(f w_1) : ℝ)),
    ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)

Tactic:
obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt K ↑1 h

Premises used: NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f)
w : K
h_mem : Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K) w
h_nz : w ≠ 0
h_bd : ∀ (w_1 : InfinitePlace K), (w_1 : (a : K) → ℝ) w < (↑(f w_1) : ℝ)
obtain :
  ∀ (a : 𝓞 K)
    (h_mem :
      Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
    (h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K))
    (h_bd : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) < (↑(f w) : ℝ)),
    ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)

Tactic:
obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem

Premises used: FractionalIdeal.mem_one_iff, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f)
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_bd : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) < (↑(f w) : ℝ)
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)

Tactic:
⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩

Premises used: And.intro, Exists.intro, Iff.mp, NumberField.RingOfIntegers.coe_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f)
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_bd : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) < (↑(f w) : ℝ)
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)

Tactic:
exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
h : minkowskiBound K 1 < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀)
obtain :
  ∀ (w : K) (h_mem : Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K) w)
    (h_nz : w ≠ 0)
    (h_bd :
      (∀ (w_1 : InfinitePlace K), w_1 ≠ (↑w₀ : InfinitePlace K) → (w_1 : (a : K) → ℝ) w < (↑(f w_1) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) w)| < 1 ∧
          |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) w)| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2),
    ∃ (a : 𝓞 K),
      a ≠ 0 ∧
        (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)) ∧
          |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
            |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| <
              HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
          |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2

Tactic:
obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt' K ↑1 w₀ h

Premises used: NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt', OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
h : minkowskiBound K 1 < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀)
w : K
h_mem : Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K) w
h_nz : w ≠ 0
h_bd :
  (∀ (w_1 : InfinitePlace K), w_1 ≠ (↑w₀ : InfinitePlace K) → (w_1 : (a : K) → ℝ) w < (↑(f w_1) : ℝ)) ∧
    |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) w)| < 1 ∧
      |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) w)| <
        HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
obtain :
  ∀ (a : 𝓞 K)
    (h_mem :
      Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
    (h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K))
    (h_bd :
      (∀ (w : InfinitePlace K),
          w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) < (↑(f w) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))| <
            1 ∧
          |Complex.im
                (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2),
    ∃ (a : 𝓞 K),
      a ≠ 0 ∧
        (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)) ∧
          |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
            |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| <
              HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
          |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2

Tactic:
obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem

Premises used: FractionalIdeal.mem_one_iff, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
h : minkowskiBound K 1 < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀)
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_bd :
  (∀ (w : InfinitePlace K),
      w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) < (↑(f w) : ℝ)) ∧
    |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))| < 1 ∧
      |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))| <
        HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
          |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2

Tactic:
⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩

Premises used: And.intro, Exists.intro, Iff.mp, NumberField.RingOfIntegers.coe_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
h : minkowskiBound K 1 < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀)
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_bd :
  (∀ (w : InfinitePlace K),
      w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) < (↑(f w) : ℝ)) ∧
    |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))| < 1 ∧
      |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))| <
        HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| < 1 ∧
          |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) (↑a : K))| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2

Tactic:
exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩
-- 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∞)
rw :
  minkowskiBound K 1 <
    (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      (↑((∏ x ∈ Finset.erase Finset.univ w₀, (if x = w₀ then B else 1) ^ x.mult) *
            (if w₀ = w₀ then B else 1) ^ 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 B else 1)

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₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
simp_rw :
  minkowskiBound K 1 <
    (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      (↑((∏ x ∈ Finset.erase Finset.univ w₀, if x = w₀ then B ^ x.mult else 1) * if True then B ^ w₀.mult else 1) :
        ℝ≥0∞)
⊢ minkowskiBound K 1 <
    (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      (↑((∏ x ∈ Finset.erase Finset.univ w₀, (if x = w₀ then B else 1) ^ x.mult) *
            (if w₀ = w₀ then B else 1) ^ 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₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
rw :
  minkowskiBound K 1 <
    (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      (↑((if w₀ ∈ Finset.erase Finset.univ w₀ then B ^ w₀.mult else 1) * if True then B ^ w₀.mult else 1) : ℝ≥0∞)
⊢ minkowskiBound K 1 <
    (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      (↑((∏ x ∈ Finset.erase Finset.univ w₀, if x = w₀ then B ^ x.mult else 1) * if True then B ^ 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₀.IsReal
B : ℝ≥0
hB simp_rw : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
⊢ minkowskiBound K 1 <
    (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      (↑((if w₀ ∈ Finset.erase Finset.univ w₀ then B ^ w₀.mult else 1) * if True then B ^ w₀.mult else 1) : ℝ≥0∞)

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

Premises used: ite_false, NumberField.InfinitePlace.mult, ite_true, pow_one, Finset.notMem_erase, one_mul
-- 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∞)
⊢ minkowskiBound K 1 < (↑(convexBodyLTFactor 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₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
⊢ minkowskiBound K 1 < (↑(convexBodyLTFactor 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₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor 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 B else 1)

Tactic:
have : minkowskiBound K ↑1 < volume (convexBodyLT K (fun w ↦ if w = w₀ then B else 1)) := by
    rw [convexBodyLT_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
    simp_rw [ite_pow, one_pow]
    rw [Finset.prod_ite_eq']
    simp_rw [Finset.notMem_erase, ite_false, mult, hw₀, ite_true, one_mul, pow_one]
    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₀.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)
obtain :
  ∀ (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) : ℝ)

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

Premises used: NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt
-- 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) : ℝ)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)

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

Premises used: And.intro, Exists.intro, 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₀.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)⟯ ⊤
refine_2 : ∀ (w : InfinitePlace K), (↑(if w = w₀ then B else 1) : ℝ) ≤ (↑(max B 1) : ℝ)
⊢ ∃ (a : 𝓞 K),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)

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

Tactic:
convert! (if_neg h_ne) ▸ h_le w
-- 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) : ℝ)
⊢ 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) (Or.inl hw₀)

Premises used: NumberField.is_primitive_element_of_infinitePlace_lt, Or.inl