awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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) : ℝ)
h1 :
  ∀ (w : InfinitePlace K),
    Membership.mem (γ := Finset (InfinitePlace K)) univ w →
      (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → 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)

Tactic:
gcongr with w
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
h : Membership.mem (γ := Finset (InfinitePlace K)) univ w
⊢ (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) y : K) ≤ (↑(g w) : ℝ)

Tactic:
(h_yle w).le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
h : Membership.mem (γ := Finset (InfinitePlace K)) univ w
⊢ (w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) y : K) ≤ (↑(g w) : ℝ)

Tactic:
exact (h_yle w).le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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) : ℝ)
simp_rw : (↑(∏ a : InfinitePlace K, g a ^ a.mult) : ℝ) ≤ (↑B : ℝ)
⊢ LE.le (α := ℝ) (∏ w : InfinitePlace K, (↑(g w) : ℝ) ^ w.mult) (↑B : ℝ)

Tactic:
simp_rw [← NNReal.coe_pow, ← NNReal.coe_prod]

Premises used: NNReal.coe_prod, NNReal.coe_pow
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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) : ℝ)
⊢ (↑(∏ a : InfinitePlace K, g a ^ a.mult) : ℝ) ≤ (↑B : ℝ)

Tactic:
le_of_eq (congr_arg toReal h_gprod)

Premises used: congr_arg, le_of_eq, NNReal.toReal
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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) : ℝ)
⊢ (↑(∏ a : InfinitePlace K, g a ^ a.mult) : ℝ) ≤ (↑B : ℝ)

Tactic:
exact le_of_eq (congr_arg toReal h_gprod)

Premises used: congr_arg, le_of_eq, NNReal.toReal
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 (α := ℝ) (∏ w : InfinitePlace K, (↑(g w) : ℝ) ^ w.mult) (↑B : ℝ)
⊢ LE.le (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑y : K)| : ℝ) (↑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)

Premises used: Algebra.algebraMap, Nat.cast, NumberField.InfinitePlace, NumberField.InfinitePlace.prod_eq_abs_norm, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₁
⊢ LT.lt (α := ℝ) 1 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₁
refine_2 : LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
⊢ (↑(f w) : ℝ) < (w : (a : K) → ℝ) (↑x : K)

Tactic:
refine div_lt_self ?_ (by simp)

Premises used: div_lt_self
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₁
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)

Tactic:
pos_iff.mpr hx'

Premises used: Iff.mpr, NumberField.InfinitePlace.pos_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₁
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)

Tactic:
exact pos_iff.mpr hx'

Premises used: Iff.mpr, NumberField.InfinitePlace.pos_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : ℝ)) ⋯
suffices : ∀ (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 : ℚ) : ℚ)

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'
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
_ : w ≠ w₁ → f w ≠ 0
⊢ w ≠ w₁ → f w ≠ 0

Tactic:
_
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₁
rw : ¬(↑x : K) = 0 ∧ ¬Eq (α := ℝ) 2 0
⊢ f w ≠ 0

Tactic:
rw [ne_eq, Nonneg.mk_eq_zero, div_eq_zero_iff, map_eq_zero, not_or]

Premises used: map_eq_zero, ne_eq, not_or, Nonneg.mk_eq_zero, div_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₁
⊢ ¬Eq (α := ℝ) 2 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₁
⊢ ¬(↑x : K) = 0 ∧ ¬Eq (α := ℝ) 2 0

Tactic:
exact ⟨hx', by simp⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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)
⊢ Ne.{u_1 + 1} (α := 𝓞 K) 1 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : ℕ
⊢ Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) (0 : K)

Tactic:
RingOfIntegers.coe_ne_zero_iff.mpr (seq K w₁ hB n).prop

Premises used: Iff.mpr, Subtype.prop, NumberField.RingOfIntegers.coe_ne_zero_iff, NumberField.Units.dirichletUnitTheorem.seq
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
zero : False
⊢ 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:
exfalso
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
⊢ False

Tactic:
Nat.not_succ_le_zero n h

Premises used: Nat.not_succ_le_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
⊢ False

Tactic:
exact Nat.not_succ_le_zero n h

Premises used: Nat.not_succ_le_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
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) : ℝ)
⊢ 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:
rw [hr]
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 m) : 𝓞 K) : K) : ℝ)

Tactic:
(seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw

Premises used: Exists.choose_spec, NumberField.Units.dirichletUnitTheorem.seq_next, And.right, And.left, Subtype.prop, NumberField.Units.dirichletUnitTheorem.seq
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 m) : 𝓞 K) : K) : ℝ)

Tactic:
exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw

Premises used: Exists.choose_spec, NumberField.Units.dirichletUnitTheorem.seq_next, And.right, And.left, Subtype.prop, NumberField.Units.dirichletUnitTheorem.seq
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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) : ℝ)

Tactic:
lt_trans ?_ (m_ih hr)

Premises used: lt_trans
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
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) : ℝ)
⊢ 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:
refine lt_trans ?_ (m_ih hr)

Premises used: lt_trans
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 m) : 𝓞 K) : K) : ℝ)

Tactic:
(seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw

Premises used: Exists.choose_spec, NumberField.Units.dirichletUnitTheorem.seq_next, And.right, And.left, Subtype.prop, NumberField.Units.dirichletUnitTheorem.seq
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 m) : 𝓞 K) : K) : ℝ)

Tactic:
exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw

Premises used: Exists.choose_spec, NumberField.Units.dirichletUnitTheorem.seq_next, And.right, And.left, Subtype.prop, NumberField.Units.dirichletUnitTheorem.seq