awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : ℝ)
refine_1 : LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
⊢ ∃ (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_2 : ∀ (w : InfinitePlace K) (hw : w ≠ w₁), (↑(f w) : ℝ) < (w : (a : K) → ℝ) (↑x : K)
Tactic: refine ⟨y, h_ynz, fun w hw ↦ (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩
-- 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) : ℝ)
⊢ LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℚ) ((↑B : ℚ) : ℚ)
have refine_1 : LE.le (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℝ) (↑B : ℝ)
Tactic: rw [← Rat.cast_le (K := ℝ), Rat.cast_natCast]
-- 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) : ℝ)
⊢ LE.le (α := ℝ)
    (∏ w : InfinitePlace K,
      HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) y : K) : ℝ) w.mult)
    (∏ w : InfinitePlace K, (↑(g w) : ℝ) ^ w.mult)
have h1 : ∀ (w : InfinitePlace K),
  Membership.mem (γ := Finset (InfinitePlace K)) univ w →
    (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) y : K) ≤ (↑(g w) : ℝ)
Tactic: gcongr with w
-- 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) : ℝ)
⊢ LE.le (α := ℝ) (∏ w : InfinitePlace K, (↑(g w) : ℝ) ^ w.mult) (↑B : ℝ)
have simp_rw : (↑(∏ a : InfinitePlace K, g a ^ a.mult) : ℝ) ≤ (↑B : ℝ)
Tactic: simp_rw [← NNReal.coe_pow, ← NNReal.coe_prod]
-- 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) : ℝ)
⊢ LE.le (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℝ) (↑B : ℝ)
have _ : LE.le (α := ℝ)
  (∏ w : InfinitePlace K,
    HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) y : K) : ℝ) w.mult)
  (∏ w : InfinitePlace K, (↑(g w) : ℝ) ^ w.mult)
Tactic: calc
        _ = ∏ w : InfinitePlace K, w (algebraMap _ K y) ^ mult w :=
          (prod_eq_abs_norm (algebraMap _ K y)).symm
        _ ≤ ∏ w : InfinitePlace K, (g w : ℝ) ^ mult w := by gcongr with w; exact (h_yle w).le
        _ ≤ (B : ℝ) := by
          simp_rw [← NNReal.coe_pow, ← NNReal.coe_prod]
          exact le_of_eq (congr_arg toReal 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) : ℝ)
_ :
  LE.le (α := ℝ)
    (∏ w : InfinitePlace K,
      HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) y : K) : ℝ) w.mult)
    (∏ w : InfinitePlace K, (↑(g w) : ℝ) ^ w.mult)
⊢ LE.le (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℝ) (↑B : ℝ)
have _₁ : LE.le (α := ℝ) (∏ w : InfinitePlace K, (↑(g w) : ℝ) ^ w.mult) (↑B : ℝ)
Tactic: calc
        _ = ∏ w : InfinitePlace K, w (algebraMap _ K y) ^ mult w :=
          (prod_eq_abs_norm (algebraMap _ K y)).symm
        _ ≤ ∏ w : InfinitePlace K, (g w : ℝ) ^ mult w := by gcongr with w; exact (h_yle w).le
        _ ≤ (B : ℝ) := by
          simp_rw [← NNReal.coe_pow, ← NNReal.coe_prod]
          exact le_of_eq (congr_arg toReal 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) : ℝ)
w : InfinitePlace K
hw : w ≠ w₁
⊢ (↑(f w) : ℝ) < (w : (a : K) → ℝ) (↑x : K)
have refine_2 : LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
Tactic: refine div_lt_self ?_ (by simp)
-- 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 : ℝ)) ⋯
⊢ ∃ (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 suffices : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
Tactic: suffices ∀ w, w ≠ w₁ → f w ≠ 0 by
    obtain ⟨g, h_geqf, h_gprod⟩ := adjust_f K B this
    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)
    refine ⟨y, h_ynz, fun w hw ↦ (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩
    · rw [← Rat.cast_le (K := ℝ), Rat.cast_natCast]
      calc
        _ = ∏ w : InfinitePlace K, w (algebraMap _ K y) ^ mult w :=
          (prod_eq_abs_norm (algebraMap _ K y)).symm
        _ ≤ ∏ w : InfinitePlace K, (g w : ℝ) ^ mult w := by gcongr with w; exact (h_yle w).le
        _ ≤ (B : ℝ) := by
          simp_rw [← NNReal.coe_pow, ← NNReal.coe_prod]
          exact le_of_eq (congr_arg toReal h_gprod)
    · refine div_lt_self ?_ (by simp)
      exact pos_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 : ℝ)) ⋯
w : InfinitePlace K
h : w ≠ w₁
⊢ f w ≠ 0
have rw : ¬(↑x : K) = 0 ∧ ¬Eq (α := ℝ) 2 0
Tactic: rw [ne_eq, Nonneg.mk_eq_zero, div_eq_zero_iff, map_eq_zero, not_or]
-- 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)
n : ℕ
w : InfinitePlace K
hw : w ≠ w₁
h : n < 0
⊢ LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB 0) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
have zero : False
Tactic: exfalso
-- 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)
n : ℕ
w : InfinitePlace K
hw : w ≠ w₁
m : ℕ
m_ih :
  ∀ (h : n < m),
    LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
      ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
h : n < m + 1
hr : n = m
⊢ LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB (m + 1)) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
have succ : LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB (m + 1)) : 𝓞 K) : K) : ℝ)
  ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
Tactic: rw [hr]
-- 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)
n : ℕ
w : InfinitePlace K
hw : w ≠ w₁
m : ℕ
m_ih :
  ∀ (h : n < m),
    LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
      ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
h : n < m + 1
hr : n < m
⊢ LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB (m + 1)) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
have succ : LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB (m + 1)) : 𝓞 K) : K) : ℝ)
  ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
Tactic: refine lt_trans ?_ (m_ih hr)
-- 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)
n : ℕ
w : InfinitePlace K
hw : w ≠ w₁
m : ℕ
m_ih :
  ∀ (h : n < m),
    LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
      ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
h : n < m + 1
⊢ LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB (m + 1)) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
have x : n = m ∨ n < m
Tactic: cases eq_or_lt_of_le (Nat.le_of_lt_succ h) with
      | inl hr =>
          rw [hr]
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw
      | inr hr =>
          refine lt_trans ?_ (m_ih hr)
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw
-- 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)
n m : ℕ
h : n < m
w : InfinitePlace K
hw : w ≠ w₁
⊢ LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
have zero : ∀ (h : n < 0),
  LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB 0) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
Tactic: induction m with
  | zero =>
      exfalso
      exact Nat.not_succ_le_zero n h
  | succ m m_ih =>
      cases eq_or_lt_of_le (Nat.le_of_lt_succ h) with
      | inl hr =>
          rw [hr]
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw
      | inr hr =>
          refine lt_trans ?_ (m_ih hr)
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw
Cleared hypotheses: m, h
-- 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)
n m : ℕ
h : n < m
w : InfinitePlace K
hw : w ≠ w₁
zero :
  ∀ (h : n < 0),
    LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB 0) : 𝓞 K) : K) : ℝ)
      ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
⊢ LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
have succ : ∀ (m : ℕ)
  (m_ih :
    ∀ (h : n < m),
      LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
        ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ))
  (h : n < m + 1),
  LT.lt (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB (m + 1)) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)
Tactic: induction m with
  | zero =>
      exfalso
      exact Nat.not_succ_le_zero n h
  | succ m m_ih =>
      cases eq_or_lt_of_le (Nat.le_of_lt_succ h) with
      | inl hr =>
          rw [hr]
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw
      | inr hr =>
          refine lt_trans ?_ (m_ih hr)
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw
Cleared hypotheses: m, h
-- 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)
⊢ 1 ≤ B
have contrapose! : ∀ (hB : B < 1), (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal) ≤ minkowskiBound K 1
Tactic: contrapose! hB
Cleared hypotheses: hB
-- 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)
⊢ Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB 0) : 𝓞 K)) ≤ B
have this : 1 ≤ B
Tactic: have : 1 ≤ B := by
        contrapose! hB
        simp only [Nat.lt_one_iff.mp hB, CharP.cast_eq_zero, mul_zero, zero_le]
-- 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)
n : ℕ
⊢ Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB (n + 1)) : 𝓞 K)) ≤ B
have succ : LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑(↑(seq K w₁ hB (n + 1)) : 𝓞 K) : K)| : ℚ) ((↑B : ℚ) : ℚ)
Tactic: rw [← Nat.cast_le (α := ℚ), Nat.cast_natAbs, Int.cast_abs, Algebra.coe_norm_int]
-- 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)
n : ℕ
⊢ Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB n) : 𝓞 K)) ≤ B
have zero : Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB 0) : 𝓞 K)) ≤ B
Tactic: cases n with
  | zero =>
      have : 1 ≤ B := by
        contrapose! hB
        simp only [Nat.lt_one_iff.mp hB, CharP.cast_eq_zero, mul_zero, zero_le]
      simp only [ne_eq, seq, map_one, Int.natAbs_one, this]
  | succ n =>
      rw [← Nat.cast_le (α := ℚ), Nat.cast_natAbs, Int.cast_abs, Algebra.coe_norm_int]
      exact (seq_next K w₁ hB (seq K w₁ hB n).prop).choose_spec.2.2
Cleared hypotheses: n
-- 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)
n : ℕ
zero : Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB 0) : 𝓞 K)) ≤ B
⊢ Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB n) : 𝓞 K)) ≤ B
have succ : ∀ (n : ℕ), Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB (n + 1)) : 𝓞 K)) ≤ B
Tactic: cases n with
  | zero =>
      have : 1 ≤ B := by
        contrapose! hB
        simp only [Nat.lt_one_iff.mp hB, CharP.cast_eq_zero, mul_zero, zero_le]
      simp only [ne_eq, seq, map_one, Int.natAbs_one, this]
  | succ n =>
      rw [← Nat.cast_le (α := ℚ), Nat.cast_natAbs, Int.cast_abs, Algebra.coe_norm_int]
      exact (seq_next K w₁ hB (seq K w₁ hB n).prop).choose_spec.2.2
Cleared hypotheses: n
-- 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 : ℕ), minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
have p : fun (B : ℕ) ↦ minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
Tactic: congr
-- 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
| fun (B : ℕ) ↦ minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
have p : ∀ (x : ℕ), minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑x : ENNReal)
Tactic: ext
-- 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
x : ℕ
| minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑x : ENNReal)
have p : minkowskiBound K 1 < (↑x : ENNReal) * (↑(convexBodyLTFactor K) : ENNReal)
Tactic: rw [mul_comm]
-- 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 : ℕ), minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
have p : ∀ (x : ℕ), minkowskiBound K 1 < (↑x : ENNReal) * (↑(convexBodyLTFactor K) : ENNReal)
Tactic: congr; ext; rw [mul_comm]
-- 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 : ℕ), minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
have conv : ∃ (x : ℕ), minkowskiBound K 1 < (↑x : ENNReal) * (↑(convexBodyLTFactor K) : ENNReal)
Tactic: conv => congr; ext; rw [mul_comm]
-- 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
⊢ ∃ (u : (𝓞 K)ˣ),
    ∀ (w : InfinitePlace K),
      w ≠ w₁ → Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0
have obtain : ∀ (B : ℕ) (hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)),
  ∃ (u : (𝓞 K)ˣ),
    ∀ (w : InfinitePlace K),
      w ≠ w₁ → Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0
Tactic: obtain ⟨B, hB⟩ : ∃ B : ℕ, minkowskiBound K 1 < (convexBodyLTFactor K) * B := by
    conv => congr; ext; rw [mul_comm]
    exact ENNReal.exists_nat_mul_gt (ENNReal.coe_ne_zero.mpr (convexBodyLTFactor_ne_zero K))
      (ne_of_lt (minkowskiBound_lt_top K 1))
-- 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)
⊢ ∃ (u : (𝓞 K)ˣ),
    ∀ (w : InfinitePlace K),
      w ≠ w₁ → Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0
have rsuffices : ∀ (n m : ℕ) (hnm : n < m)
  (h : Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})),
  ∃ (u : (𝓞 K)ˣ),
    ∀ (w : InfinitePlace K),
      w ≠ w₁ → Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0
Tactic: rsuffices ⟨n, m, hnm, h⟩ : ∃ n m, n < m ∧
      (Ideal.span ({ (seq K w₁ hB n : 𝓞 K) }) = Ideal.span ({ (seq K w₁ hB m : 𝓞 K) }))