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
B : ℝ
hB : 0 < B
⊢ HMul.hMul (α := ℝ) 2
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (x : ℝ) ↦ rexp (-x)) ^
        nrRealPlaces K *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-2 * ‖x‖))
        (nrComplexPlaces K) =
    HMul.hMul (α := ℝ) 2
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume (Set.Ioi 0)) fun (x : ℝ) ↦
            rexp (-HPow.hPow (β := ℝ) x 1)) ^
        nrRealPlaces K *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-2 * HPow.hPow (β := ℝ) ‖x‖ 1))
        (nrComplexPlaces K)

Tactic:
simp_rw [Real.rpow_one]

Premises used: Real.rpow_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
⊢ HAdd.hAdd (α := ℝ) (-2) 1 = -1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
simp_rw :
  (2 * Gamma (HAdd.hAdd (α := ℝ) 1 1)) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * Gamma (HAdd.hAdd (α := ℝ) 2 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₁ :
  (2 * Gamma 2) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * Gamma (HAdd.hAdd (α := ℝ) 2 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₂ :
  (2 * Gamma 2) ^ nrRealPlaces K * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * (2 * Gamma 2)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₃ :
  HMul.hMul (α := ℝ) 2 1 ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * HMul.hMul (α := ℝ) 2 1) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₄ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 2) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₅ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * (HPow.hPow (α := ℝ) (β := ℝ) 2 (-2) * 2)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₆ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℝ) (-2) 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₇ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * HPow.hPow (α := ℝ) (β := ℝ) 2 (-1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
simp_rw₈ :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π * 2⁻¹) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K
⊢ (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K *
      (π * HPow.hPow (α := ℝ) 2 (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K

Tactic:
simp_rw [div_one, one_add_one_eq_two, Gamma_add_one two_ne_zero, Gamma_two, mul_one,
          mul_assoc, ← Real.rpow_add_one two_ne_zero, show (-2 : ℝ) + 1 = -1 by norm_num,
          Real.rpow_neg_one, div_eq_mul_inv]

Premises used: Real.rpow_neg_one, Real.Gamma_two, mul_assoc, Real.Gamma_add_one, one_add_one_eq_two, div_eq_mul_inv, Real.rpow_add_one, two_ne_zero, mul_one, div_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
refine :
  Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) =
    Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))
⊢ Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)

Tactic:
refine Fintype.equivOfCardEq ?_

Premises used: Fintype.equivOfCardEq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
rw :
  finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) =
    Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))
rw₁ : finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) = finrank.{0, u_1} ℤ (𝓞 K)
rw₂ rw₃ : finrank.{0, u_1} ℤ (𝓞 K) = finrank.{0, u_1} ℤ (𝓞 K)
⊢ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) =
    Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ (𝓞 K))

Tactic:
rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]

Premises used: NumberField.fractionalIdeal_rank, Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 ⋯
rw :
  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∞)
b₀ : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
        (fractionalIdealLatticeBasis K I)) =
    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 [← fundamentalDomain_reindex (fractionalIdealLatticeBasis K I) e,
    measure_fundamentalDomain ((fractionalIdealLatticeBasis K I).reindex e)]

Premises used: ZSpan.measure_fundamentalDomain, NumberField.mixedEmbedding.fractionalIdealLatticeBasis, ZSpan.fundamentalDomain_reindex, Module.Basis.reindex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 ⋯
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)
⊢ 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))))

Tactic:
ext1
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 ⋯
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:
simp only [Basis.coe_reindex, Function.comp_apply, fractionalIdealLatticeBasis_apply]

Premises used: Module.Basis.coe_reindex, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, Function.comp_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 ⋯
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∞)
⊢ 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∞)

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]]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 ⋯
rw 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∞)
⊢ 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 [mixedEmbedding.det_basisOfFractionalIdeal_eq_norm]

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

Tactic:
ENNReal.mul_lt_top (fundamentalDomain_isBounded _).measure_lt_top <|
    ENNReal.pow_lt_top ENNReal.ofNat_lt_top

Premises used: NumberField.mixedEmbedding.minkowskiBound, ENNReal.pow_lt_top, ENNReal.mul_lt_top, Bornology.IsBounded.measure_lt_top, ZSpan.fundamentalDomain_isBounded, ENNReal.ofNat_lt_top
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ minkowskiBound K I < ∞

Tactic:
exact ENNReal.mul_lt_top (fundamentalDomain_isBounded _).measure_lt_top <|
    ENNReal.pow_lt_top ENNReal.ofNat_lt_top

Premises used: ENNReal.pow_lt_top, ENNReal.mul_lt_top, Bornology.IsBounded.measure_lt_top, ZSpan.fundamentalDomain_isBounded, ENNReal.ofNat_lt_top
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ minkowskiBound K I < ∞

Tactic:
classical
  -- FIXME: Make `finiteness` work here
  exact ENNReal.mul_lt_top (fundamentalDomain_isBounded _).measure_lt_top <|
    ENNReal.pow_lt_top ENNReal.ofNat_lt_top

Premises used: ENNReal.pow_lt_top, ENNReal.mul_lt_top, Bornology.IsBounded.measure_lt_top, ZSpan.fundamentalDomain_isBounded, ENNReal.ofNat_lt_top
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ Ne (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K :=
          ℝ) (fractionalIdealLatticeBasis K I)) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
ZSpan.measure_fundamentalDomain_ne_zero _

Premises used: ZSpan.measure_fundamentalDomain_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ Ne (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K :=
          ℝ) (fractionalIdealLatticeBasis K I)) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
exact ZSpan.measure_fundamentalDomain_ne_zero _

Premises used: ZSpan.measure_fundamentalDomain_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ Ne (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K :=
          ℝ) (fractionalIdealLatticeBasis K I)) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
classical exact ZSpan.measure_fundamentalDomain_ne_zero _

Premises used: ZSpan.measure_fundamentalDomain_ne_zero
-- 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)ˣ
h : minkowskiBound K I < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f)
⊢ 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)ˣ
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
⊢ 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)ˣ
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
⊢ 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