-- 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 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

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

Result:
case neg.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, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤
    ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))|

case neg.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, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ r ≤ ↑(Fintype.card (InfinitePlace K)) * r

Proof state:
case neg.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, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ r ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
nth_rw 1 [← one_mul r]

Result:
case neg.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, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ 1 * r ≤ ↑(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
x : ℝ
hx : 0 ≤ x
⊢ x ≤ ↑w.mult * x

Tactic:
nth_rw 1 [← one_mul x]

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
x : ℝ
hx : 0 ≤ x
⊢ 1 * x ≤ ↑w.mult * x

Proof state:
case neg.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, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ 1 * r ≤ ↑(Fintype.card (InfinitePlace K)) * r

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

Result:
no goals

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 • r ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
rw [nsmul_eq_mul]

Result:
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) * r ≤ ↑(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
x : ℝ
hx : 0 ≤ x
⊢ 1 * x ≤ ↑w.mult * x

Tactic:
refine mul_le_mul ?_ le_rfl hx ?_

Result:
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

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 ≤ ↑(if w.IsReal then 1 else 2)

Tactic:
split_ifs <;> norm_num

Result:
no goals

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
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
by_cases hw : w = w₀

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₀
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

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

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|
⊢ ∑ x_1 : { w // w ≠ w₀ }, |(logEmbedding K) (Additive.ofMul x) x_1| ≤ ↑(Fintype.card (InfinitePlace K)) * r

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

Result:
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 • r ≤ ↑(Fintype.card (InfinitePlace K)) * r

Proof state:
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))|

Tactic:
rw [← hw]

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))|