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 : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : w = w₀
hyp :
  (↑(mult.{u_1} (K := K) w₀) : ℝ) *
      |Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    ∑ x_1 : { w : InfinitePlace K // w ≠ w₀ },
      |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) x_1|
pos : card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ • r ≤ (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
⊢ ∑ x_1 : { w : InfinitePlace K // w ≠ w₀ },
      |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) x_1| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
refine (sum_le_card_nsmul univ _ _
        (fun w _ ↦ logEmbedding_component_le hr h w)).trans ?_

Premises used: Finset.univ, NumberField.Units.dirichletUnitTheorem.logEmbedding_component_le, Finset.sum_le_card_nsmul, LE.le.trans
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : w = w₀
hyp :
  (↑(mult.{u_1} (K := K) w₀) : ℝ) *
      |Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    ∑ x_1 : { w : InfinitePlace K // w ≠ w₀ },
      |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) x_1|
pos :
  (↑(card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ) : ℝ) * r ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
⊢ card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ • r ≤ (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
rw [nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : w = w₀
hyp :
  (↑(mult.{u_1} (K := K) w₀) : ℝ) *
      |Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    ∑ x_1 : { w : InfinitePlace K // w ≠ w₀ },
      |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) x_1|
⊢ (↑(card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ) : ℝ) * r ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
mul_le_mul ?_ le_rfl hr (Fintype.card (InfinitePlace K)).cast_nonneg

Premises used: le_rfl, Nat.cast_nonneg, Fintype.card, mul_le_mul, NumberField.InfinitePlace
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : w = w₀
hyp :
  (↑(mult.{u_1} (K := K) w₀) : ℝ) *
      |Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    ∑ x_1 : { w : InfinitePlace K // w ≠ w₀ },
      |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) x_1|
pos :
  LE.le (α := ℝ) (↑(card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ) : ℝ)
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ)
⊢ (↑(card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ) : ℝ) * r ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
refine mul_le_mul ?_ le_rfl hr (Fintype.card (InfinitePlace K)).cast_nonneg

Premises used: le_rfl, Nat.cast_nonneg, Fintype.card, mul_le_mul, NumberField.InfinitePlace
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : w = w₀
hyp :
  (↑(mult.{u_1} (K := K) w₀) : ℝ) *
      |Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    ∑ x_1 : { w : InfinitePlace K // w ≠ w₀ },
      |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) x_1|
⊢ LE.le (α := ℝ) (↑(card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ) : ℝ)
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : ¬w = w₀
⊢ |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) :
          Additive (𝓞 K)ˣ)
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw)| ≤
    r

Tactic:
have hyp := logEmbedding_component_le hr h ⟨w, hw⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : ¬w = w₀
hyp :
  |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) :
          Additive (𝓞 K)ˣ)
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw)| ≤
    r
⊢ (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r

Tactic:
rw [logEmbedding_component, abs_mul, Nat.abs_cast] at hyp

Premises used: Nat.abs_cast, abs_mul, NumberField.Units.dirichletUnitTheorem.logEmbedding_component
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : ¬w = w₀
hyp :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
(le_trans ?_ hyp).trans ?_

Premises used: LE.le.trans, le_trans
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : ¬w = w₀
hyp :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r
neg :
  |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) : K))|
neg₁ : r ≤ (↑(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:
refine (le_trans ?_ hyp).trans ?_

Premises used: LE.le.trans, le_trans
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : ¬w = w₀
hyp :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) : K))|

Tactic:
tool _ (abs_nonneg _)

Premises used: abs_nonneg
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : ¬w = w₀
hyp :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) : K))|

Tactic:
exact tool _ (abs_nonneg _)

Premises used: abs_nonneg
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : ¬w = w₀
hyp :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r
neg : 1 * r ≤ (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
⊢ r ≤ (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
nth_rw 1 [← one_mul r]

Premises used: one_mul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : ¬w = w₀
hyp :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r
⊢ 1 * r ≤ (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
mul_le_mul (Nat.one_le_cast.mpr Fintype.card_pos) (le_of_eq rfl) hr (Nat.cast_nonneg _)

Premises used: Iff.mpr, Nat.cast_nonneg, Nat.one_le_cast, mul_le_mul, le_of_eq, Fintype.card_pos, rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x
hw : ¬w = w₀
hyp :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r
⊢ 1 * r ≤ (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r

Tactic:
exact mul_le_mul (Nat.one_le_cast.mpr Fintype.card_pos) (le_of_eq rfl) hr (Nat.cast_nonneg _)

Premises used: Iff.mpr, Nat.cast_nonneg, Nat.one_le_cast, mul_le_mul, le_of_eq, Fintype.card_pos, rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
inl : ∀ (hr : r < 0), ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
inr : ∀ (hr : 0 ≤ r), ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite

Tactic:
obtain hr | hr := lt_or_ge r 0

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : r < 0
⊢ Set.Finite.{u_1} (α := logSpace K) ∅

Tactic:
Set.finite_empty

Premises used: Set.finite_empty
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : r < 0
h : (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r = ∅
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite

Tactic:
convert! Set.finite_empty

Premises used: Set.finite_empty
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : r < 0
h : (↑(unitLattice K) : Set (logSpace K)) ∩ ∅ = ∅
⊢ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r = ∅

Tactic:
rw [Metric.closedBall_eq_empty.mpr hr]

Premises used: Iff.mpr, Metric.closedBall_eq_empty
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : r < 0
⊢ (↑(unitLattice K) : Set (logSpace K)) ∩ ∅ = ∅

Tactic:
Set.inter_empty _

Premises used: Set.inter_empty
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : r < 0
⊢ (↑(unitLattice K) : Set (logSpace K)) ∩ ∅ = ∅

Tactic:
exact Set.inter_empty _

Premises used: Set.inter_empty
-- 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)}
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite

Tactic:
(Set.Finite.image (logEmbedding K) this).subset ?_

Premises used: Set.Finite.subset, Set.Finite.image, NumberField.Units.logEmbedding, DFunLike.coe
-- 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)}
refine :
  (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r ⊆
    Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace 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:
refine (Set.Finite.image (logEmbedding K) this).subset ?_

Premises used: Set.Finite.subset, Set.Finite.image, NumberField.Units.logEmbedding, DFunLike.coe
-- 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)
⊢ Membership.mem (α := logSpace K) (γ := Set (logSpace K))
    (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace 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)})
    ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K)

Tactic:
⟨x, ⟨x.val.prop, (le_iff_le _ _).mp (fun w ↦ (Real.log_le_iff_le_exp ?_).mp ?_)⟩, rfl⟩

Premises used: Units.val, NumberField.InfinitePlace.le_iff_le, Set.Mem, setOf, Real.log_le_iff_le_exp, Subtype.prop, And.intro, Exists.intro, Iff.mp, Set.image, rfl
-- 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)
refine_1 :
  ∀ (w : InfinitePlace K),
    LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ)
refine_2 :
  ∀ (w : InfinitePlace K),
    Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) ≤
      (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
⊢ Membership.mem (α := logSpace K) (γ := Set (logSpace K))
    (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace 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)})
    ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K)

Tactic:
refine ⟨x, ⟨x.val.prop, (le_iff_le _ _).mp (fun w ↦ (Real.log_le_iff_le_exp ?_).mp ?_)⟩, rfl⟩
-- 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:
pos_iff.mpr (coe_ne_zero x)

Premises used: Iff.mpr, NumberField.InfinitePlace.pos_iff, NumberField.Units.coe_ne_zero