mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ mixedEmbedding.norm ((mixedEmbedding K) x) = ↑|(Algebra.norm ℚ) x|

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ mixedEmbedding.norm ((mixedEmbedding K) x) = ↑|(Algebra.norm ℚ) x|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ univ
⊢ Continuous fun a ↦ (normAtPlace x✝¹) a ^ x✝¹.mult

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ univ
⊢ Continuous fun a ↦ (normAtPlace x✝¹) a ^ x✝¹.mult
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ univ
⊢ Continuous fun a ↦
    { toFun := fun x ↦ if hw : x✝¹.IsReal then ‖x.1 ⟨x✝¹, hw⟩‖ else ‖x.2 ⟨x✝¹, ⋯⟩‖, map_zero' := ⋯ } a ^ x✝¹.mult

Tactic:
ZeroHom.coe_mk,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ univ
⊢ Continuous fun a ↦ (if hw : x✝¹.IsReal then ‖a.1 ⟨x✝¹, hw⟩‖ else ‖a.2 ⟨x✝¹, ⋯⟩‖) ^ x✝¹.mult
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) =
    (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) =
    (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (∫ (x : ℝ), rexp (-‖x‖)) ^ card { w // w.IsReal } * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ card { w // w.IsComplex } =
    (∫ (x : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (∫ (x : ℝ), rexp (-‖x‖)) ^ card { w // w.IsReal } * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ card { w // w.IsComplex } =
    (∫ (x : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr ((commMap K) x)) c) = (matrixToStdBasis K *ᵥ x ∘ ⇑(indexEquiv K)) c

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr ((commMap K) x)) c) = (matrixToStdBasis K *ᵥ x ∘ ⇑(indexEquiv K)) c
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K =
    (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x ^ 1)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖ ^ 1)) ^ nrComplexPlaces K

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K =
    (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x ^ 1)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖ ^ 1)) ^ nrComplexPlaces K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K * (π * 2 ^ (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K =
    2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K * (π * 2 ^ (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K =
    2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) (Sum.inl w)) =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inl w) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
[

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) (Sum.inl w)) =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inl w) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
j : Fin 2
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) (Sum.inr (w, j))) =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inr (w, j)) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, j)) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, j)) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
fin_cases j

Goal state after:
case inr.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) (Sum.inr (w, (fun i ↦ i) ⟨0, ⋯⟩))) =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inr (w, (fun i ↦ i) ⟨0, ⋯⟩)) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, (fun i ↦ i) ⟨0, ⋯⟩)) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, (fun i ↦ i) ⟨0, ⋯⟩)) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

case inr.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) (Sum.inr (w, (fun i ↦ i) ⟨1, ⋯⟩))) =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inr (w, (fun i ↦ i) ⟨1, ⋯⟩)) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, (fun i ↦ i) ⟨1, ⋯⟩)) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, (fun i ↦ i) ⟨1, ⋯⟩)) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, (if x = w₀ then B else 1) ^ x.mult) * (if True then B else 1) ^ w₀.mult)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, (if x = w₀ then B else 1) ^ x.mult) * (if True then B else 1) ^ w₀.mult)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((if w₀ ∈ Finset.univ.erase w₀ then B ^ w₀.mult else 1) * if True then B ^ w₀.mult else 1)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((if w₀ ∈ Finset.univ.erase w₀ then B ^ w₀.mult else 1) * if True then B ^ w₀.mult else 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLT'Factor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, (if x = w₀ then NNReal.sqrt B else 1) ^ x.mult) *
          (if True then NNReal.sqrt B else 1) ^ w₀.mult)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLT'Factor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, (if x = w₀ then NNReal.sqrt B else 1) ^ x.mult) *
          (if True then NNReal.sqrt B else 1) ^ w₀.mult)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsZLattice ℝ (mixedEmbedding.integerLattice K)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsZLattice ℝ (mixedEmbedding.integerLattice K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1, (mixedEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1, (mixedEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLT'Factor K) *
      ↑((if w₀ ∈ Finset.univ.erase w₀ then NNReal.sqrt B ^ w₀.mult else 1) *
          if True then NNReal.sqrt B ^ w₀.mult else 1)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLT'Factor K) *
      ↑((if w₀ ∈ Finset.univ.erase w₀ then NNReal.sqrt B ^ w₀.mult else 1) *
          if True then NNReal.sqrt B ^ w₀.mult else 1)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * ↑(2 ^ nrRealPlaces K * (pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * ↑(2 ^ nrRealPlaces K * (pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
this : f ((integralBasis K) i) = (Basis.restrictScalars ℚ (latticeBasis K)) i
⊢ (↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) =
    ↑(integralBasis K).repr ((integralBasis K) i)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
this : f ((integralBasis K) i) = (Basis.restrictScalars ℚ (latticeBasis K)) i
⊢ (↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) =
    ↑(integralBasis K).repr ((integralBasis K) i)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹ =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹ =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
i j : ChooseBasisIndex ℤ (𝓞 K)
⊢ (latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) i j =
    (algebraMap ℚ ℝ).mapMatrix ((integralBasis K).toMatrix (⇑(basisOfFractionalIdeal K I) ∘ ⇑e)) i j

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
i j : ChooseBasisIndex ℤ (𝓞 K)
⊢ (latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) i j =
    (algebraMap ℚ ℝ).mapMatrix ((integralBasis K).toMatrix (⇑(basisOfFractionalIdeal K I) ∘ ⇑e)) i j
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ :
  |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : ¬w = w₀
⊢ 1 ≤ √(1 + ↑B ^ 2)

Tactic:
Real.le_sqrt' zero_lt_one,

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ :
  |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : ¬w = w₀
⊢ 1 ^ 2 ≤ 1 + ↑B ^ 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ IsZLattice ℝ (idealLattice K I)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ IsZLattice ℝ (idealLattice K I)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsZLattice ℝ (euclidean.integerLattice K)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsZLattice ℝ (euclidean.integerLattice K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∈ s
⊢ ((negAt s) x).1 w = -x.1 w

Tactic:
[

Goal state after:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∈ s
⊢ ((negAt s) x).1 w = -x.1 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s) x).1 w = x.1 w

Tactic:
[

Goal state after:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s) x).1 w = x.1 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∈ s
⊢ MeasurePreserving (↑↑(if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)).toAddHom.1 volume volume

Tactic:
[

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∈ s
⊢ MeasurePreserving (↑↑(if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)).toAddHom.1 volume volume
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑1) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
⊢ ↑|(Algebra.norm ℚ) ↑a| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑1) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
⊢ ↑|(Algebra.norm ℚ) ↑a| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∉ s
⊢ MeasurePreserving (↑↑(if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)).toAddHom.1 volume volume

Tactic:
[

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∉ s
⊢ MeasurePreserving (↑↑(if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)).toAddHom.1 volume volume