-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem log_le_of_logEmbedding_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r)
    (h : ‖logEmbedding K (Additive.ofMul x)‖ ≤ r) (w : InfinitePlace K) :
    |Real.log (w x)| ≤ (Fintype.card (InfinitePlace K)) * r

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  (fun x => ‖x‖) (-↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))) ≤
    ∑ i : { w // w ≠ w₀ }, ‖(logEmbedding K) (Additive.ofMul x) i‖
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

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

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤
    ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
⊢ 1 ≤ ↑w.mult

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ↑w.mult

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

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  (fun x => ‖x‖) (-↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))) =
    (fun x => ‖x‖) (∑ w : { w // w ≠ w₀ }, (logEmbedding K) (Additive.ofMul x) w)
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
replace hyp := (le_of_eq hyp).trans (norm_sum_le _ _)

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  (fun x => ‖x‖) (-↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))) ≤
    ∑ i : { w // w ≠ w₀ }, ‖(logEmbedding K) (Additive.ofMul x) i‖
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
have hyp := logEmbedding_component_le hr h ⟨w, hw⟩

Result:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : |(logEmbedding K) (Additive.ofMul (Additive.ofMul x)) ⟨w, hw⟩| ≤ r
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

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 }

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ↑w.mult

Tactic:
rw [mult]

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ↑(if w.IsReal then 1 else 2)

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤
    ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

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

Result:
case pos.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤
    ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))|

case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤
    ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Proof state:
case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp :
  ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤
    ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ ↑(#univ) ≤ ↑(Fintype.card (InfinitePlace K))

Tactic:
simp

Result:
no goals

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : |(logEmbedding K) (Additive.ofMul (Additive.ofMul x)) ⟨w, hw⟩| ≤ r
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

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

Result:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r