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
x : Additive (𝓞 K)ˣ
h :
  Membership.mem (α := (𝓞 K)ˣ) (γ := Subgroup (𝓞 K)ˣ) (torsion K)
      ((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x : (𝓞 K)ˣ) ↔
    Membership.mem (α := Additive (𝓞 K)ˣ) (γ := AddSubgroup (Additive (𝓞 K)ˣ))
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ)) (torsion K) :
        AddSubgroup (Additive (𝓞 K)ˣ))
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) ((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x) :
        Additive (𝓞 K)ˣ)
⊢ Membership.mem (γ := AddSubgroup (Additive (𝓞 K)ˣ)) (AddMonoidHom.ker (M := logSpace K) (logEmbedding K)) x ↔
    Membership.mem (γ := AddSubgroup (Additive (𝓞 K)ˣ))
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ)) (torsion K) :
        AddSubgroup (Additive (𝓞 K)ˣ))
      x

Tactic:
rw [AddMonoidHom.mem_ker, ← ofMul_toMul x, logEmbedding_eq_zero_iff]

Premises used: NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, ofMul_toMul, AddMonoidHom.mem_ker
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : Additive (𝓞 K)ˣ
⊢ Membership.mem (α := (𝓞 K)ˣ) (γ := Subgroup (𝓞 K)ˣ) (torsion K)
      ((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x : (𝓞 K)ˣ) ↔
    Membership.mem (α := Additive (𝓞 K)ˣ) (γ := AddSubgroup (Additive (𝓞 K)ˣ))
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ)) (torsion K) :
        AddSubgroup (Additive (𝓞 K)ˣ))
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) ((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x) :
        Additive (𝓞 K)ˣ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : AddSubgroup (Additive (𝓞 K)ˣ)
rw :
  Eq (α := AddSubgroup (logSpace K))
    (AddSubgroup.map (logEmbedding K) (s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K)))
    (AddSubgroup.map (logEmbedding K) s)
rw₁ :
  s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K) ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K) =
    s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K)
rw₂ rw₃ :
  s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K) = s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K)
⊢ Eq (α := AddSubgroup (logSpace K))
    (AddSubgroup.map (logEmbedding K)
      (s ⊔ (Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ)) (torsion K)))
    (AddSubgroup.map (logEmbedding K) s)

Tactic:
rw [← logEmbedding_ker, AddSubgroup.map_eq_map_iff, sup_right_idem]

Premises used: AddSubgroup.map_eq_map_iff, sup_right_idem, NumberField.Units.dirichletUnitTheorem.logEmbedding_ker
-- 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) x : logSpace K) ≤ r
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ 0 ≤ r

Tactic:
hr
-- 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) x : logSpace K) ≤ r
w : { w : InfinitePlace K // w ≠ w₀ }
lift :
  ∀ (r : NNReal)
    (h : norm (E := logSpace K) ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K) ≤ (↑r : ℝ)),
    |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w| ≤
      (↑r : ℝ)
⊢ |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w| ≤
    r

Tactic:
lift r to NNReal using hr

Premises used: NNReal
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
w : { w : InfinitePlace K // w ≠ w₀ }
r : NNReal
h : norm (E := logSpace K) ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K) ≤ (↑r : ℝ)
⊢ ∀ (b : { w : InfinitePlace K // w ≠ w₀ }),
    Membership.mem (γ := Finset { w : InfinitePlace K // w ≠ w₀ }) univ b →
      (↑(nnnorm (E := ℝ) ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K) x b)) : ℝ) ≤ (↑r : ℝ)

Tactic:
simp_rw [Pi.norm_def, NNReal.coe_le_coe, Finset.sup_le_iff, ← NNReal.coe_le_coe] at h

Premises used: Pi.norm_def, Finset.sup_le_iff, NNReal.coe_le_coe
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
w : { w : InfinitePlace K // w ≠ w₀ }
r : NNReal
h :
  ∀ (b : { w : InfinitePlace K // w ≠ w₀ }),
    Membership.mem (γ := Finset { w : InfinitePlace K // w ≠ w₀ }) univ b →
      (↑(nnnorm (E := ℝ) ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K) x b)) : ℝ) ≤ (↑r : ℝ)
⊢ |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w| ≤
    (↑r : ℝ)

Tactic:
h w (mem_univ _)

Premises used: Finset.mem_univ, abs, NNReal.toReal
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
w : { w : InfinitePlace K // w ≠ w₀ }
r : NNReal
h :
  ∀ (b : { w : InfinitePlace K // w ≠ w₀ }),
    Membership.mem (γ := Finset { w : InfinitePlace K // w ≠ w₀ }) univ b →
      (↑(nnnorm (E := ℝ) ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K) x b)) : ℝ) ≤ (↑r : ℝ)
⊢ |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w| ≤
    (↑r : ℝ)

Tactic:
exact h w (mem_univ _)

Premises used: Finset.mem_univ
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
nth_rw : 1 * x ≤ (↑w.mult : ℝ) * x
⊢ x ≤ (↑w.mult : ℝ) * x

Tactic:
nth_rw 1 [← one_mul x]

Premises used: one_mul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
⊢ 1 * x ≤ (↑w.mult : ℝ) * x

Tactic:
mul_le_mul ?_ le_rfl hx ?_

Premises used: le_rfl, mul_le_mul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
refine_1 : LE.le (α := ℝ) 1 (↑w.mult : ℝ)
refine_2 : LE.le (α := ℝ) 0 (↑w.mult : ℝ)
⊢ 1 * x ≤ (↑w.mult : ℝ) * x

Tactic:
refine mul_le_mul ?_ le_rfl hx ?_

Premises used: le_rfl, mul_le_mul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
pos : w.IsReal → LE.le (α := ℝ) 1 (↑1 : ℝ)
neg : ¬w.IsReal → LE.le (α := ℝ) 1 (↑2 : ℝ)
⊢ LE.le (α := ℝ) 1 (↑(if w.IsReal then 1 else 2) : ℝ)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h_1 : w.IsReal
⊢ LE.le (α := ℝ) 1 (↑1 : ℝ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h_1 : ¬w.IsReal
⊢ LE.le (α := ℝ) 1 (↑2 : ℝ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
refine_1 refine_1₁ refine_1₂ refine_1₃ : LE.le (α := ℝ) 1 (↑(if w.IsReal then 1 else 2) : ℝ)
⊢ LE.le (α := ℝ) 1 (↑w.mult : ℝ)

Tactic:
{ rw [mult]; split_ifs <;> norm_num }

Premises used: NumberField.InfinitePlace.mult
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
pos : w.IsReal → LE.le (α := ℝ) 0 (↑1 : ℝ)
neg : ¬w.IsReal → LE.le (α := ℝ) 0 (↑2 : ℝ)
⊢ LE.le (α := ℝ) 0 (↑(if w.IsReal then 1 else 2) : ℝ)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h_1 : w.IsReal
⊢ LE.le (α := ℝ) 0 (↑1 : ℝ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h_1 : ¬w.IsReal
⊢ LE.le (α := ℝ) 0 (↑2 : ℝ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
x_1 : (𝓞 K)ˣ
hr : 0 ≤ r
h :
  norm (E := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x_1 : Additive (𝓞 K)ˣ) :
        logSpace K) ≤
    r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
refine_2 refine_2₁ refine_2₂ refine_2₃ : LE.le (α := ℝ) 0 (↑(if w.IsReal then 1 else 2) : ℝ)
⊢ LE.le (α := ℝ) 0 (↑w.mult : ℝ)

Tactic:
{ rw [mult]; split_ifs <;> norm_num }

Premises used: NumberField.InfinitePlace.mult
-- 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
⊢ ∀ (x : ℝ), 0 ≤ x → x ≤ (↑w.mult : ℝ) * x

Tactic:
have tool : ∀ x : ℝ, 0 ≤ x → x ≤ mult w * x := fun x hx ↦ by
    nth_rw 1 [← one_mul x]
    refine mul_le_mul ?_ le_rfl hx ?_
    all_goals { rw [mult]; split_ifs <;> norm_num }
-- 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
pos :
  ∀ (hw : w = w₀),
    |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
      (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
neg :
  ∀ (hw : ¬w = w₀),
    |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:
by_cases hw : w = w₀

Premises used: NumberField.Units.dirichletUnitTheorem.w₀
-- 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₀
⊢ Eq (α := ℝ)
    ((fun (x : ℝ) ↦ ‖x‖)
      (-(↑(mult.{u_1} (K := K) w₀) : ℝ) *
        Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))))
    ((fun (x : ℝ) ↦ ‖x‖)
      (∑ w : { w : InfinitePlace K // w ≠ w₀ },
        (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w))

Tactic:
have hyp := congr_arg (‖·‖) (sum_logEmbedding_component x).symm
-- 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 :
  Eq (α := ℝ)
    ((fun (x : ℝ) ↦ ‖x‖)
      (-(↑(mult.{u_1} (K := K) w₀) : ℝ) *
        Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))))
    ((fun (x : ℝ) ↦ ‖x‖)
      (∑ w : { w : InfinitePlace K // w ≠ w₀ },
        (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w))
⊢ LE.le (α := ℝ)
    ((fun (x : ℝ) ↦ ‖x‖)
      (-(↑(mult.{u_1} (K := K) w₀) : ℝ) *
        Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))))
    (∑ i : { w : InfinitePlace K // w ≠ w₀ },
      norm (E := ℝ)
        ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) i))

Tactic:
replace hyp := (le_of_eq hyp).trans (norm_sum_le _ _)
-- 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 :
  LE.le (α := ℝ)
    ((fun (x : ℝ) ↦ ‖x‖)
      (-(↑(mult.{u_1} (K := K) w₀) : ℝ) *
        Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))))
    (∑ i : { w : InfinitePlace K // w ≠ w₀ },
      norm (E := ℝ)
        ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) i))
⊢ (↑(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|

Tactic:
simp_rw [norm_mul, norm_neg, Real.norm_eq_abs, Nat.abs_cast] at hyp

Premises used: Nat.abs_cast, norm_mul, norm_neg, Real.norm_eq_abs
-- 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|
⊢ |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 :
  (↑(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 :
  |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(mult.{u_1} (K := K) w₀) : ℝ) *
      |Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))|
pos₁ :
  ∑ 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
⊢ |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 :
  (↑(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 :
  |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑w.mult : ℝ) * |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))|
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(mult.{u_1} (K := K) w₀) : ℝ) *
      |Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))|

Tactic:
rw [← 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 :
  (↑(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|
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑w.mult : ℝ) * |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → 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 :
  (↑(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|
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑w.mult : ℝ) * |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → 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 :
  (↑(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|
⊢ ∑ 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:
(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