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
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
  Fintype.equivOfCardEq ⋯
⊢ Eq (α := (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)
    (⇑(Basis.reindex (fractionalIdealLatticeBasis K I) e) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)
    (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
      (Function.comp (β := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(basisOfFractionalIdeal K I :
              Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
          (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
        (⇑e.symm :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) →
            Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))))
have h : ∀ (x : Free.ChooseBasisIndex ℤ (𝓞 K)),
  Eq (α := mixedSpace K)
    ((Basis.reindex (fractionalIdealLatticeBasis K I) e : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K) x :
      mixedSpace K)
    (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
        (Function.comp (β := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(basisOfFractionalIdeal K I :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
            (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
          (⇑e.symm :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) →
              Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))
        x :
      mixedSpace K)
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
  Fintype.equivOfCardEq ⋯
⊢ HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal
        |((Basis.det (latticeBasis K) : mixedSpace K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
            (⇑(Basis.reindex (fractionalIdealLatticeBasis K I) e) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → mixedSpace K)|)
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
        ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
        ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞)
    (ENNReal.ofReal
      |((Basis.det (latticeBasis K) : mixedSpace K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
          (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
            (Function.comp (β := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
              (⇑e.symm :
                (a : Free.ChooseBasisIndex ℤ (𝓞 K)) →
                  Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))))|)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
      ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞)
    (ENNReal.ofReal
      (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
      ℝ≥0∞)
Tactic: rw [show (fractionalIdealLatticeBasis K I).reindex e = (mixedEmbedding K) ∘
        (basisOfFractionalIdeal K I) ∘ e.symm by
      ext1; simp only [Basis.coe_reindex, Function.comp_apply, fractionalIdealLatticeBasis_apply]]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
  Fintype.equivOfCardEq ⋯
⊢ HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal
        |((Basis.det (latticeBasis K) : mixedSpace K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K) → mixedSpace K) → ℝ)
            (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
              (Function.comp (β := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
                (⇑(basisOfFractionalIdeal K I :
                      Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                  (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
                (⇑e.symm :
                  (a : Free.ChooseBasisIndex ℤ (𝓞 K)) →
                    Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))))|)
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
        ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
        ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞)
    (ENNReal.ofReal
      (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
      ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞)
    (ENNReal.ofReal
      (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
      ℝ≥0∞)
Tactic: rw [mixedEmbedding.det_basisOfFractionalIdeal_eq_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f)
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) a < (↑(f w) : ℝ)
have h_fund : IsAddFundamentalDomain.{u_1, u_1}
  ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
      (span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                  (mixedSpace K)) :
            (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
  (α := mixedSpace K)
  (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
    (fractionalIdealLatticeBasis K I))
  volume
Tactic: have h_fund := ZSpan.isAddFundamentalDomain' (fractionalIdealLatticeBasis K I) volume
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f)
h_fund :
  IsAddFundamentalDomain.{u_1, u_1}
    ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
        (span ℤ
          (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(fractionalIdealLatticeBasis K I :
                  Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                    (mixedSpace K)) :
              (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
    (α := mixedSpace K)
    (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
      (fractionalIdealLatticeBasis K I))
    volume
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) a < (↑(f w) : ℝ)
have this : Countable.{u_1 + 1}
  ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
      (span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                  (mixedSpace K)) :
            (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
Tactic: have : Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I))).toAddSubgroup := by
    change Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I)))
    infer_instance
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
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₀)
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) a < (↑(f w) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) a)| < 1 ∧
          |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) a)| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
have h_fund : IsAddFundamentalDomain.{u_1, u_1}
  ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
      (span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                  (mixedSpace K)) :
            (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
  (α := mixedSpace K)
  (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
    (fractionalIdealLatticeBasis K I))
  volume
Tactic: have h_fund := ZSpan.isAddFundamentalDomain' (fractionalIdealLatticeBasis K I) volume
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) a < (↑(f w) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) a)| < 1 ∧
          |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) a)| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
have this : Countable.{u_1 + 1}
  ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
      (span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                  (mixedSpace K)) :
            (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
Tactic: have : Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I))).toAddSubgroup := by
    change Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I)))
    infer_instance
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f)
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)
have 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) : ℝ)
Tactic: obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt K ↑1 h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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) : ℝ)
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(f w) : ℝ)
have 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) : ℝ)
Tactic: obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
Cleared hypotheses: w, h_mem, h_nz, h_bd
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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),
    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
have 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
Tactic: obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt' K ↑1 w₀ h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
Cleared hypotheses: w, h_mem, h_nz, h_bd
-- 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∞)
⊢ 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 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∞)
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₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑B : ℝ≥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∞)
have 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∞)
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₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑B : ℝ≥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∞)
have 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∞)
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₀.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 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)
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
-- 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),
    Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤ ∧
      ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑a : K) < (↑(max B 1) : ℝ)
have 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) : ℝ)
Tactic: obtain ⟨a, h_nz, h_le⟩ := exists_ne_zero_mem_ringOfIntegers_lt K this