-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem logEmbedding_eq_zero_iff {x : (𝓞 K)ˣ} :
    logEmbedding K (Additive.ofMul x) = 0 ↔ x ∈ torsion K

Proof state:
case refine_2.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1
w : { w // w ≠ w₀ }
⊢ (logEmbedding K) (Additive.ofMul x) w = 0 w

Tactic:
rw [logEmbedding_component, h w.val, Real.log_one, mul_zero, Pi.zero_apply]

Result:
no goals

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1
⊢ (logEmbedding K) (Additive.ofMul x) = 0

Tactic:
ext w

Result:
case refine_2.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1
w : { w // w ≠ w₀ }
⊢ (logEmbedding K) (Additive.ofMul x) w = 0 w

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
⊢ -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x)) = 0

Tactic:
rw [← sum_logEmbedding_component, sum_eq_zero]

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
⊢ ∀ x_1 ∈ univ, (logEmbedding K) (Additive.ofMul x) x_1 = 0

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
suffices -mult w₀ * Real.log (w₀ (x : K)) = 0 by
  rw [neg_mul, neg_eq_zero, ← hw] at this
  exact mult_log_place_eq_zero.mp this

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
⊢ -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x)) = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
this : -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x)) = 0
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
rw [neg_mul, neg_eq_zero, ← hw] at this

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
this : ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ (logEmbedding K) (Additive.ofMul x) = 0 ↔ ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
refine ⟨fun h w => ?_, fun h => ?_⟩

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1
⊢ (logEmbedding K) (Additive.ofMul x) = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
this : ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
exact mult_log_place_eq_zero.mp this

Result:
no goals

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : ¬w = w₀
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
exact mult_log_place_eq_zero.mp (congrFun h ⟨w, hw⟩)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ (logEmbedding K) (Additive.ofMul x) = 0 ↔ x ∈ torsion K

Tactic:
rw [mem_torsion]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ (logEmbedding K) (Additive.ofMul x) = 0 ↔ ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
⊢ ∀ x_1 ∈ univ, (logEmbedding K) (Additive.ofMul x) x_1 = 0

Tactic:
exact fun w _ => congrFun h w

Result:
no goals

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
by_cases hw : w = w₀

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : ¬w = w₀
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1