awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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
have 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)ˣ)
Tactic: rw [AddMonoidHom.mem_ker, ← ofMul_toMul x, logEmbedding_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : AddSubgroup (Additive (𝓞 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)
have rw : Eq (α := AddSubgroup (logSpace K))
  (AddSubgroup.map (logEmbedding K) (s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K)))
  (AddSubgroup.map (logEmbedding K) s)
Tactic: rw [← logEmbedding_ker, AddSubgroup.map_eq_map_iff, sup_right_idem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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)
⊢ Eq (α := AddSubgroup (logSpace K))
    (AddSubgroup.map (logEmbedding K)
      (s ⊔ (Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ)) (torsion K)))
    (AddSubgroup.map (logEmbedding K) s)
have rw₁ : s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K) ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K) =
  s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K)
Tactic: rw [← logEmbedding_ker, AddSubgroup.map_eq_map_iff, sup_right_idem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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)
⊢ Eq (α := AddSubgroup (logSpace K))
    (AddSubgroup.map (logEmbedding K)
      (s ⊔ (Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ)) (torsion K)))
    (AddSubgroup.map (logEmbedding K) s)
have rw₂ : s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K) = s ⊔ AddMonoidHom.ker (M := logSpace K) (logEmbedding K)
Tactic: rw [← logEmbedding_ker, AddSubgroup.map_eq_map_iff, sup_right_idem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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₀ }
⊢ |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w| ≤
    r
have 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 : ℝ)
Tactic: lift r to NNReal using hr
Cleared hypotheses: r, hr, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
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 : ℝ)
⊢ |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w| ≤
    (↑r : ℝ)
have 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 : ℝ)
Tactic: simp_rw [Pi.norm_def, NNReal.coe_le_coe, Finset.sup_le_iff, ← NNReal.coe_le_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
⊢ x ≤ (↑w.mult : ℝ) * x
have nth_rw : 1 * x ≤ (↑w.mult : ℝ) * x
Tactic: nth_rw 1 [← one_mul x]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
have refine_1 : LE.le (α := ℝ) 1 (↑w.mult : ℝ)
Tactic: refine mul_le_mul ?_ le_rfl hx ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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 : ℝ)
⊢ 1 * x ≤ (↑w.mult : ℝ) * x
have refine_2 : LE.le (α := ℝ) 0 (↑w.mult : ℝ)
Tactic: refine mul_le_mul ?_ le_rfl hx ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
⊢ LE.le (α := ℝ) 1 (↑(if w.IsReal then 1 else 2) : ℝ)
have pos : w.IsReal → LE.le (α := ℝ) 1 (↑1 : ℝ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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 : ℝ)
⊢ LE.le (α := ℝ) 1 (↑(if w.IsReal then 1 else 2) : ℝ)
have neg : ¬w.IsReal → LE.le (α := ℝ) 1 (↑2 : ℝ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
⊢ LE.le (α := ℝ) 1 (↑w.mult : ℝ)
have refine_1 : LE.le (α := ℝ) 1 (↑(if w.IsReal then 1 else 2) : ℝ)
Tactic: { rw [mult]; split_ifs <;> norm_num }
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
⊢ LE.le (α := ℝ) 0 (↑(if w.IsReal then 1 else 2) : ℝ)
have pos : w.IsReal → LE.le (α := ℝ) 0 (↑1 : ℝ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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 : ℝ)
⊢ LE.le (α := ℝ) 0 (↑(if w.IsReal then 1 else 2) : ℝ)
have neg : ¬w.IsReal → LE.le (α := ℝ) 0 (↑2 : ℝ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
⊢ LE.le (α := ℝ) 0 (↑w.mult : ℝ)
have refine_2 : LE.le (α := ℝ) 0 (↑(if w.IsReal then 1 else 2) : ℝ)
Tactic: { rw [mult]; split_ifs <;> norm_num }
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
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
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
have tool : ∀ (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 }
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
have 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
Tactic: by_cases hw : w = w₀
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
have 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
Tactic: by_cases hw : w = w₀
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
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₀
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
have 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))
Tactic: have hyp := congr_arg (‖·‖) (sum_logEmbedding_component x).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
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))
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
have 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))
Tactic: replace hyp := (le_of_eq hyp).trans (norm_sum_le _ _)
Cleared hypotheses: hyp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
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))
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
have 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|
Tactic: simp_rw [norm_mul, norm_neg, Real.norm_eq_abs, Nat.abs_cast] at hyp
Cleared hypotheses: hyp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
have 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))|
Tactic: refine (le_trans ?_ hyp).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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))|
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
have 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
Tactic: refine (le_trans ?_ hyp).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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))| ≤
    (↑(mult.{u_1} (K := K) w₀) : ℝ) *
      |Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))|
have 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))|
Tactic: rw [← hw]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
have pos : card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ • r ≤ (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
Tactic: refine (sum_le_card_nsmul univ _ _
        (fun w _ ↦ logEmbedding_component_le hr h w)).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
have pos : (↑(card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ) : ℝ) * r ≤
  (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
Tactic: rw [nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
have pos : LE.le (α := ℝ) (↑(card.{u_1} (α := { w : InfinitePlace K // w ≠ w₀ }) univ) : ℝ)
  (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ)
Tactic: refine mul_le_mul ?_ le_rfl hr (Fintype.card (InfinitePlace K)).cast_nonneg