awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) :
        Additive (𝓞 K)ˣ)
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw)| ≤
  r
Tactic: have hyp := logEmbedding_component_le hr h ⟨w, hw⟩
-- 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 :
  |(logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) :
          Additive (𝓞 K)ˣ)
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw)| ≤
    r
⊢ |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
have hyp₁ : (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
    |Real.log
        (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) : K))| ≤
  r
Tactic: rw [logEmbedding_component, abs_mul, 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 :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              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 : |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
    |Real.log
        (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 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 :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r
neg :
  |Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))| ≤
    (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 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 neg₁ : r ≤ (↑(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 :
  (↑(↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K).mult : ℝ) *
      |Real.log
          (((↑(Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw) : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x) : 𝓞 K) :
              K))| ≤
    r
⊢ r ≤ (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
have neg : 1 * r ≤ (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
Tactic: nth_rw 1 [← one_mul r]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
have inl : ∀ (hr : r < 0), ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
Tactic: obtain hr | hr := lt_or_ge r 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
inl : ∀ (hr : r < 0), ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
have inr : ∀ (hr : 0 ≤ r), ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
Tactic: obtain hr | hr := lt_or_ge r 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : r < 0
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
have h : (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r = ∅
Tactic: convert! Set.finite_empty
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : r < 0
⊢ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r = ∅
have h : (↑(unitLattice K) : Set (logSpace K)) ∩ ∅ = ∅
Tactic: rw [Metric.closedBall_eq_empty.mpr hr]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
have refine : (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r ⊆
  Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
Tactic: refine (Set.Finite.image (logEmbedding K) this).subset ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
x : Additive (𝓞 K)ˣ
left : x ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hx :
  Membership.mem (α := logSpace K) (γ := Set (logSpace K)) (Metric.closedBall 0 r)
    ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K)
⊢ Membership.mem (α := logSpace K) (γ := Set (logSpace K))
    (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K)
      {x : (𝓞 K)ˣ |
        IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
          ∀ (φ : K →+* ℂ),
            norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
              Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)})
    ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K)
have refine_1 : ∀ (w : InfinitePlace K),
  LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ)
Tactic: refine ⟨x, ⟨x.val.prop, (le_iff_le _ _).mp (fun w ↦ (Real.log_le_iff_le_exp ?_).mp ?_)⟩, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
x : Additive (𝓞 K)ˣ
left : x ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hx :
  Membership.mem (α := logSpace K) (γ := Set (logSpace K)) (Metric.closedBall 0 r)
    ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K)
refine_1 :
  ∀ (w : InfinitePlace K),
    LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ)
⊢ Membership.mem (α := logSpace K) (γ := Set (logSpace K))
    (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K)
      {x : (𝓞 K)ˣ |
        IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
          ∀ (φ : K →+* ℂ),
            norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
              Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)})
    ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K)
have refine_2 : ∀ (w : InfinitePlace K),
  Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) ≤
    (↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r
Tactic: refine ⟨x, ⟨x.val.prop, (le_iff_le _ _).mp (fun w ↦ (Real.log_le_iff_le_exp ?_).mp ?_)⟩, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
x : Additive (𝓞 K)ˣ
left : x ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hx :
  Membership.mem (α := logSpace K) (γ := Set (logSpace K)) (Metric.closedBall 0 r)
    ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : logSpace K)
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 refine_2 : ∀
  (hx :
    norm (E := logSpace K)
        ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) x : 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
Tactic: rw [mem_closedBall_zero_iff] at hx
Cleared hypotheses: hx, 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 : ℝ
hr : 0 ≤ r
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 r).Finite
have inr : Set.Finite.{u_1} (α := (𝓞 K)ˣ)
  {x : (𝓞 K)ˣ |
    IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
      ∀ (φ : K →+* ℂ),
        norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
          Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
Tactic: suffices {x : (𝓞 K)ˣ | IsIntegral ℤ (x : K) ∧
        ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ Real.exp ((Fintype.card (InfinitePlace K)) * r)}.Finite by
      refine (Set.Finite.image (logEmbedding K) this).subset ?_
      rintro _ ⟨⟨x, ⟨_, rfl⟩⟩, hx⟩
      refine ⟨x, ⟨x.val.prop, (le_iff_le _ _).mp (fun w ↦ (Real.log_le_iff_le_exp ?_).mp ?_)⟩, rfl⟩
      · exact pos_iff.mpr (coe_ne_zero x)
      · rw [mem_closedBall_zero_iff] at hx
        exact (le_abs_self _).trans (log_le_of_logEmbedding_le hr hx 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 : ℝ
hr : 0 ≤ r
⊢ Set.Finite.{u_1} (α := (𝓞 K)ˣ)
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
have inr : Set.Finite.{u_1} (α := K)
  ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) ''
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)})
Tactic: refine Set.Finite.of_finite_image ?_ (coe_injective K).injOn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ Set.Finite.{u_1} (α := K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) ''
      {x : (𝓞 K)ˣ |
        IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
          ∀ (φ : K →+* ℂ),
            norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
              Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)})
have inr : Subset.{u_1} (α := Set K)
  ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) ''
    {x : (𝓞 K)ˣ |
      IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) ∧
        ∀ (φ : K →+* ℂ),
          norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) ≤
            Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)})
  {x : K |
    IsIntegral ℤ x ∧
      ∀ (φ : K →+* ℂ),
        norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ Real.exp ((↑(Fintype.card.{u_1} (InfinitePlace K)) : ℝ) * r)}
Tactic: refine (Embeddings.finite_of_norm_le K ℂ
        (Real.exp ((Fintype.card (InfinitePlace K)) * r))).subset ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
⊢ ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
have hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
Tactic: have hx' := RingOfIntegers.coe_ne_zero_iff.mpr hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
⊢ ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
have obtain : ∀ (g : InfinitePlace K → ℝ≥0) (h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w)
  (h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)),
  ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
Tactic: obtain ⟨g, h_geqf, h_gprod⟩ := adjust_f K B this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
⊢ minkowskiBound K 1 <
    ((MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
      (convexBodyLT K g)
have rw : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑(∏ w : InfinitePlace K, g w ^ w.mult) : ENNReal)
Tactic: rw [convexBodyLT_volume]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
⊢ minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑(∏ w : InfinitePlace K, g w ^ w.mult) : ENNReal)
have h : (↑(∏ w : InfinitePlace K, g w ^ w.mult) : ENNReal) = (↑B : ENNReal)
Tactic: convert! hB
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
⊢ ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
have obtain : ∀ (y : 𝓞 K) (h_ynz : y ≠ 0) (h_yle : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑y : K) < (↑(g w) : ℝ)),
  ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
Tactic: obtain ⟨y, h_ynz, h_yle⟩ := exists_ne_zero_mem_ringOfIntegers_lt K (f := g)
      (by rw [convexBodyLT_volume]; convert! hB; exact congr_arg ((↑) : NNReal → ENNReal) h_gprod)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
x : 𝓞 K
hx : x ≠ 0
hx' : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K)
f : InfinitePlace K → ℝ≥0 :=
  fun (w : InfinitePlace K) ↦
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (2 : ℝ)) ⋯
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : Eq (α := ℝ≥0) (∏ w : InfinitePlace K, g w ^ w.mult) (↑B : ℝ≥0)
y : 𝓞 K
h_ynz : y ≠ 0
h_yle : ∀ (w : InfinitePlace K), (w : (a : K) → ℝ) (↑y : K) < (↑(g w) : ℝ)
⊢ ∃ (y : 𝓞 K),
    y ≠ 0 ∧
      (∀ (w : InfinitePlace K),
          w ≠ w₁ → LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑y : K) : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)) ∧
        LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
have refine_1 : LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
Tactic: refine ⟨y, h_ynz, fun w hw ↦ (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩