-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem unitLattice_inter_ball_finite (r : ℝ) :
    ((unitLattice K : Set ({ w : InfinitePlace K // w ≠ w₀} → ℝ)) ∩
      Metric.closedBall 0 r).Finite

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ (↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite

Tactic:
convert Set.finite_empty

Result:
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ ↑(unitLattice K) ∩ Metric.closedBall 0 r = ∅

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ (fun x => (algebraMap (𝓞 K) K) ↑x) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)} ⊆
    {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}

Tactic:
rintro _ ⟨x, ⟨⟨h_int, h_le⟩, rfl⟩⟩

Result:
case inr.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
x : (𝓞 K)ˣ
h_int : IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x)
h_le : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)
⊢ (fun x => (algebraMap (𝓞 K) K) ↑x) x ∈
    {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}

Proof state:
case intro.intro.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
x : Additive (𝓞 K)ˣ
left✝ : x ∈ ↑⊤
hx : ‖(logEmbedding K).toIntLinearMap x‖ ≤ r
w : InfinitePlace K
⊢ Real.log (w ((algebraMap (𝓞 K) K) ↑x)) ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
exact (le_abs_self _).trans (log_le_of_logEmbedding_le hr hx w)

Result:
no goals

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
x : Additive (𝓞 K)ˣ
left✝ : x ∈ ↑⊤
hx : (logEmbedding K).toIntLinearMap x ∈ Metric.closedBall 0 r
⊢ (logEmbedding K).toIntLinearMap x ∈
    ⇑(logEmbedding K) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}

Tactic:
refine ⟨x, ⟨x.val.prop, (le_iff_le _ _).mp (fun w => (Real.log_le_iff_le_exp ?_).mp ?_)⟩, rfl⟩

Result:
case intro.intro.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
x : Additive (𝓞 K)ˣ
left✝ : x ∈ ↑⊤
hx : (logEmbedding K).toIntLinearMap x ∈ Metric.closedBall 0 r
w : InfinitePlace K
⊢ 0 < w ((algebraMap (𝓞 K) K) ↑x)

case intro.intro.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
x : Additive (𝓞 K)ˣ
left✝ : x ∈ ↑⊤
hx : (logEmbedding K).toIntLinearMap x ∈ Metric.closedBall 0 r
w : InfinitePlace K
⊢ Real.log (w ((algebraMap (𝓞 K) K) ↑x)) ≤ ↑(Fintype.card (InfinitePlace K)) * r

Proof state:
case inr.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
x : (𝓞 K)ˣ
h_int : IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x)
h_le : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)
⊢ (fun x => (algebraMap (𝓞 K) K) ↑x) x ∈
    {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}

Tactic:
exact ⟨h_int, h_le⟩

Result:
no goals

Proof state:
case intro.intro.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
x : Additive (𝓞 K)ˣ
left✝ : x ∈ ↑⊤
hx : (logEmbedding K).toIntLinearMap x ∈ Metric.closedBall 0 r
w : InfinitePlace K
⊢ Real.log (w ((algebraMap (𝓞 K) K) ↑x)) ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
rw [mem_closedBall_zero_iff] at hx

Result:
case intro.intro.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
x : Additive (𝓞 K)ˣ
left✝ : x ∈ ↑⊤
hx : ‖(logEmbedding K).toIntLinearMap x‖ ≤ r
w : InfinitePlace K
⊢ 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 : ℝ
⊢ (↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite

Tactic:
obtain hr | hr := lt_or_le r 0

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ (↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ (↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite

Proof state:
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ ↑(unitLattice K) ∩ Metric.closedBall 0 r = ∅

Tactic:
rw [Metric.closedBall_eq_empty.mpr hr]

Result:
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ ↑(unitLattice K) ∩ ∅ = ∅

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
⊢ (↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite

Tactic:
refine (Set.Finite.image (logEmbedding K) this).subset ?_

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
⊢ ↑(unitLattice K) ∩ Metric.closedBall 0 r ⊆
    ⇑(logEmbedding K) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}

Proof state:
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ ↑(unitLattice K) ∩ ∅ = ∅

Tactic:
exact Set.inter_empty _

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
⊢ ↑(unitLattice K) ∩ Metric.closedBall 0 r ⊆
    ⇑(logEmbedding K) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}

Tactic:
rintro _ ⟨⟨x, ⟨_, rfl⟩⟩, hx⟩

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
x : Additive (𝓞 K)ˣ
left✝ : x ∈ ↑⊤
hx : (logEmbedding K).toIntLinearMap x ∈ Metric.closedBall 0 r
⊢ (logEmbedding K).toIntLinearMap x ∈
    ⇑(logEmbedding K) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}