awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
x : Additive (𝓞 K)ˣ
left : x ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hx :
  Membership.mem (α := logSpace K) (γ := Set (logSpace K)) (Metric.closedBall 0 r)
    ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K)
w : InfinitePlace K
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ)

Tactic:
exact pos_iff.mpr (coe_ne_zero x)

Premises used: Iff.mpr, NumberField.InfinitePlace.pos_iff, NumberField.Units.coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
x : Additive (𝓞 K)ˣ
left : x ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hx :
  Membership.mem (α := logSpace K) (γ := Set (logSpace K)) (Metric.closedBall 0 r)
    ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K)
w : InfinitePlace K
refine_2 :
  ∀
    (hx :
      norm (E := logSpace K)
          ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K) ≤
        r)
    (w : InfinitePlace K),
    Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) ≤
      (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
⊢ Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
rw [mem_closedBall_zero_iff] at hx

Premises used: mem_closedBall_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
x : Additive (𝓞 K)ˣ
left : x ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hx :
  norm (E := logSpace K)
      ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K) ≤
    r
w : InfinitePlace K
⊢ Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
(le_abs_self _).trans (log_le_of_logEmbedding_le hr hx w)

Premises used: le_abs_self, NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, LE.le.trans
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
x : Additive (𝓞 K)ˣ
left : x ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hx :
  norm (E := logSpace K)
      ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K) ≤
    r
w : InfinitePlace K
⊢ Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
exact (le_abs_self _).trans (log_le_of_logEmbedding_le hr hx w)

Premises used: le_abs_self, NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, LE.le.trans
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
inr :
  Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite

Tactic:
suffices {x : (𝓞 K)ˣ | IsIntegral ℤ (x : K) ∧
        ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ Real.exp ((Fintype.card (InfinitePlace K)) * r)}.Finite by
      refine (Set.Finite.image (logEmbedding K) this).subset ?_
      rintro _ ⟨⟨x, ⟨_, rfl⟩⟩, hx⟩
      refine ⟨x, ⟨x.val.prop, (le_iff_le _ _).mp (fun w ↦ (Real.log_le_iff_le_exp ?_).mp ?_)⟩, rfl⟩
      · exact pos_iff.mpr (coe_ne_zero x)
      · rw [mem_closedBall_zero_iff] at hx
        exact (le_abs_self _).trans (log_le_of_logEmbedding_le hr hx w)
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}

Tactic:
Set.Finite.of_finite_image ?_ (coe_injective K).injOn

Premises used: Function.Injective.injOn, NumberField.Units.coe_injective, Set.Finite.of_finite_image
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
inr :
  Set.Finite.{u_1} (α := K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) ''
      {x : (𝓞 K)ˣ |
        IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
          ∀ (φ : K →+* ℂ),
            norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
              Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)})
⊢ Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}

Tactic:
refine Set.Finite.of_finite_image ?_ (coe_injective K).injOn

Premises used: Function.Injective.injOn, NumberField.Units.coe_injective, Set.Finite.of_finite_image
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ Set.Finite.{u_1} (α := K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) ''
      {x : (𝓞 K)ˣ |
        IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
          ∀ (φ : K →+* ℂ),
            norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
              Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)})

Tactic:
(Embeddings.finite_of_norm_le K ℂ
        (Real.exp ((Fintype.card (InfinitePlace K)) * r))).subset ?_

Premises used: HMul.hMul, Fintype.card, Set.Finite.subset, Real.exp, Nat.cast, NumberField.InfinitePlace, NumberField.Embeddings.finite_of_norm_le, Complex
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
inr :
  Subset.{u_1} (α := Set K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) ''
      {x : (𝓞 K)ˣ |
        IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
          ∀ (φ : K →+* ℂ),
            norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
              Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)})
    {x : K |
      IsIntegral ℤ x ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
⊢ Set.Finite.{u_1} (α := K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) ''
      {x : (𝓞 K)ˣ |
        IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
          ∀ (φ : K →+* ℂ),
            norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
              Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)})

Tactic:
refine (Embeddings.finite_of_norm_le K ℂ
        (Real.exp ((Fintype.card (InfinitePlace K)) * r))).subset ?_

Premises used: HMul.hMul, Fintype.card, Set.Finite.subset, Real.exp, Nat.cast, NumberField.InfinitePlace, NumberField.Embeddings.finite_of_norm_le, Complex
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
x : (𝓞 K)ˣ
h_int : IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)
h_le :
  ∀ (φ : K →+* ℂ),
    norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
      Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)
⊢ Membership.mem (γ := Set K)
    {x : K |
      IsIntegral ℤ x ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
    ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) x)

Tactic:
⟨h_int, h_le⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
x : (𝓞 K)ˣ
h_int : IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)
h_le :
  ∀ (φ : K →+* ℂ),
    norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
      Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)
⊢ Membership.mem (γ := Set K)
    {x : K |
      IsIntegral ℤ x ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
    ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) x)

Tactic:
exact ⟨h_int, h_le⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
⊢ Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)

Tactic:
have hx' := RingOfIntegers.coe_ne_zero_iff.mpr hx
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
w : InfinitePlace K
⊢ LE.le (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
obtain :
  ∀ (g : InfinitePlace K → ℝ≥0) (h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w)
    (h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)),
    ∃ (y : 𝓞 K),
      y ≠ 0 ∧
        (∀ (w : InfinitePlace K),
            w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
          LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
⊢ ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)

Tactic:
obtain ⟨g, h_geqf, h_gprod⟩ := adjust_f K B this

Premises used: NumberField.mixedEmbedding.adjust_f, Nat.cast
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
rw : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑(∏ w : InfinitePlace K, g w ^ w.mult) : ENNReal)
⊢ minkowskiBound K 1 <
    ((MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
      (convexBodyLT K g)

Tactic:
rw [convexBodyLT_volume]

Premises used: NumberField.mixedEmbedding.convexBodyLT_volume
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
⊢ minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)

Tactic:
hB
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
h : (↑(∏ w : InfinitePlace K, g w ^ w.mult) : ENNReal) = (↑B : ENNReal)
⊢ minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑(∏ w : InfinitePlace K, g w ^ w.mult) : ENNReal)

Tactic:
convert! hB
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
⊢ (↑(∏ w : InfinitePlace K, g w ^ w.mult) : ENNReal) = (↑B : ENNReal)

Tactic:
congr_arg ((↑) : NNReal → ENNReal) h_gprod

Premises used: ENNReal.ofNNReal, WithTop.some, congr_arg
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
⊢ (↑(∏ w : InfinitePlace K, g w ^ w.mult) : ENNReal) = (↑B : ENNReal)

Tactic:
exact congr_arg ((↑) : NNReal → ENNReal) h_gprod

Premises used: ENNReal.ofNNReal, congr_arg
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
obtain :
  ∀ (y : 𝓞 K) (h_ynz : y ≠ 0) (h_yle : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑y : K) < (↑(g w) : ℝ)),
    ∃ (y : 𝓞 K),
      y ≠ 0 ∧
        (∀ (w : InfinitePlace K),
            w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
          LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
⊢ ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)

Tactic:
obtain ⟨y, h_ynz, h_yle⟩ := exists_ne_zero_mem_ringOfIntegers_lt K (f := g)
      (by rw [convexBodyLT_volume]; convert! hB; exact congr_arg ((↑) : NNReal → ENNReal) h_gprod)

Premises used: NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
y : 𝓞 K
h_ynz : y ≠ 0
h_yle : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑y : K) < (↑(g w) : ℝ)
⊢ ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)

Tactic:
⟨y, h_ynz, fun w hw ↦ (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
y : 𝓞 K
h_ynz : y ≠ 0
h_yle : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑y : K) < (↑(g w) : ℝ)
refine_1 : LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
refine_2 : ∀ (w : InfinitePlace K) (hw : w ≠ w₁), (↑(f w) : ℝ) < (w : (a : K) → ℝ) (↑x : K)
⊢ ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)

Tactic:
refine ⟨y, h_ynz, fun w hw ↦ (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
y : 𝓞 K
h_ynz : y ≠ 0
h_yle : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑y : K) < (↑(g w) : ℝ)
refine_1 : LE.le (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℝ) (↑B : ℝ)
⊢ LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)

Tactic:
rw [← Rat.cast_le (K := ℝ), Rat.cast_natCast]

Premises used: Rat.cast_natCast, Rat.cast_le
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
y : 𝓞 K
h_ynz : y ≠ 0
h_yle : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑y : K) < (↑(g w) : ℝ)
⊢ Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) y : K)| : ℝ)
    (∏ w : InfinitePlace K,
      HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) y : K) : ℝ) w.mult)

Tactic:
(prod_eq_abs_norm (algebraMap _ K y)).symm

Premises used: Algebra.algebraMap, NumberField.InfinitePlace.prod_eq_abs_norm, Eq.symm, DFunLike.coe