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

Goal state before:
pp: case pos
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₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ √((w₀.embedding ↑a).re ^ 2 + (w₀.embedding ↑a).im ^ 2) ^ 2 < 1 + ↑B ^ 2

Tactic:
Real.sq_sqrt (by positivity)

Goal state after:
case pos
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₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).re ^ 2 + (w₀.embedding ↑a).im ^ 2 < 1 + ↑B ^ 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos.refine_1
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₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).re ^ 2 < 1

pp: case pos.refine_2
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₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).im ^ 2 < ↑B ^ 2

Tactic:
·

Goal state after:
case pos.refine_1
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₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).re ^ 2 < 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos.refine_2
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₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).im ^ 2 < ↑B ^ 2

Tactic:
·

Goal state after:
case pos.refine_2
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₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).im ^ 2 < ↑B ^ 2
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₀
⊢ w ↑a < √(1 + ↑B ^ 2)

Tactic:
·

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₀
⊢ w ↑a < √(1 + ↑B ^ 2)
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 (↑((fun i ↦ ↑((fun w ↦ if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) i)) w)).toAddHom.1
    volume volume

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 (↑((fun i ↦ ↑((fun w ↦ if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) i)) w)).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 (↑((fun i ↦ ↑((fun w ↦ if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) i)) w)).toAddHom.1
    volume volume
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 (↑((fun i ↦ ↑((fun w ↦ if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) i)) w)).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 (↑((fun i ↦ ↑((fun w ↦ if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) i)) w)).toAddHom.1
    volume volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

pp: case inr
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ (normAtPlace w) ((negAt s) x) = (normAtPlace w) x

Tactic:
·

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ (normAtPlace w) ((negAt s) x) = (normAtPlace w) x

Tactic:
·

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

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

pp: case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsComplex }
⊢ ((negAt s).symm x).2 w = ((negAt s) x).2 w

Tactic:
·

Goal state after:
case fst
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
⊢ ((negAt s).symm x).1 w = ((negAt s) 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 }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∈ s
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

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

Tactic:
·

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

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

Tactic:
·

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

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

Tactic:
rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]

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

Goal state before:
pp: case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsComplex }
⊢ ((negAt s).symm x).2 w = ((negAt s) x).2 w

Tactic:
·

Goal state after:
case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsComplex }
⊢ ((negAt s).symm x).2 w = ((negAt s) x).2 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ↑|(Algebra.norm ℚ) a| ^ (∑ x, ↑x.mult)⁻¹ ≤ (∏ i, ↑i a ^ ↑i.mult) ^ (∑ i, ↑i.mult)⁻¹

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ 0 < ∑ i, ↑i.mult

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ↑|(Algebra.norm ℚ) a| ^ (∑ x, ↑x.mult)⁻¹ ≤ (∏ i, ↑i a ^ ↑i.mult) ^ (∑ i, ↑i.mult)⁻¹
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = ‖x.1 w‖

pp: case neg
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : ¬x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = ‖x.1 w‖

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = ‖x.1 w‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : ¬x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = ‖x.1 w‖

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : ¬x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = ‖x.1 w‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ 0 < ∑ i, ↑i.mult

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ 0 < ∑ i, ↑i.mult
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ s ∧ w ∉ t
⊢ False

pp: case inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ t ∧ w ∉ s
⊢ False

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ s ∧ w ∉ t
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ t ∧ w ∉ s
⊢ False

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ t ∧ w ∉ s
⊢ False
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case pos
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : 0 ∈ M
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)

pp: case neg
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : 0 ∉ M
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
·

Goal state after:
case pos
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : 0 ∈ M
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case fst
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsReal }
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).1 w = x.1 w

pp: case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsComplex }
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).2 w = x.2 w

Tactic:
·

Goal state after:
case fst
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsReal }
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).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 }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsReal }
hw : w ∈ s
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).1 w = x.1 w

pp: case neg
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).1 w = x.1 w

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsReal }
hw : w ∈ s
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).1 w = x.1 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).1 w = x.1 w

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).1 w = x.1 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsComplex }
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).2 w = x.2 w

Tactic:
·

Goal state after:
case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsComplex }
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).2 w = x.2 w