-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem exists_unit (w₁ : InfinitePlace K) :
    ∃ u : (𝓞 K)ˣ, ∀ w : InfinitePlace K, w ≠ w₁ → Real.log (w u) < 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
⊢ ∃ x, minkowskiBound K 1 < ↑x * ↑(convexBodyLTFactor K)

Tactic:
exact ENNReal.exists_nat_mul_gt (ENNReal.coe_ne_zero.mpr (convexBodyLTFactor_ne_zero K))
  (ne_of_lt (minkowskiBound_lt_top K 1))

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 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))

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
⊢ ((Algebra.norm ℤ) ↑(seq K w₁ hB n)).natAbs ≤ B

Tactic:
exact seq_norm_le K w₁ hB n

Result:
no goals

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

Tactic:
refine ⟨hu.choose, fun w hw => Real.log_neg ?_ ?_⟩

Result:
case intro.intro.intro.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ 0 < w ((algebraMap (𝓞 K) K) ↑(Exists.choose hu))

case intro.intro.intro.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(Exists.choose hu)) < 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ∃ n m, n < m ∧ Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}

Tactic:
refine Set.Finite.exists_lt_map_eq_of_forall_mem (t := {I : Ideal (𝓞 K) | Ideal.absNorm I ≤ B})
  (fun n ↦ ?_) (Ideal.finite_setOf_absNorm_le B)

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
⊢ Ideal.span {↑(seq K w₁ hB n)} ∈ {I | Ideal.absNorm I ≤ B}

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))

Tactic:
exact seq_decreasing K w₁ hB hnm w hw

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
⊢ ∃ B, minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B

Tactic:
conv => congr; ext; rw [mul_comm]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
⊢ ∃ x, minkowskiBound K 1 < ↑x * ↑(convexBodyLTFactor K)

Proof state:
case intro.intro.intro.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ 0 < w ((algebraMap (𝓞 K) K) ↑(Exists.choose hu))

Tactic:
exact pos_iff.mpr (coe_ne_zero _)

Result:
no goals

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

Tactic:
have hu := Ideal.span_singleton_eq_span_singleton.mp h

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
⊢ Ideal.span {↑(seq K w₁ hB n)} ∈ {I | Ideal.absNorm I ≤ B}

Tactic:
rw [Set.mem_setOf_eq, Ideal.absNorm_span_singleton]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
⊢ ((Algebra.norm ℤ) ↑(seq K w₁ hB n)).natAbs ≤ B

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) * w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))⁻¹ < 1

Tactic:
rw [map_inv₀, mul_inv_lt_iff₀' (pos_iff.mpr (seq_ne_zero K w₁ hB n)), mul_one]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(Exists.choose hu)) =
    w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m) * ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))⁻¹)

Tactic:
rw [← congr_arg (algebraMap (𝓞 K) K) hu.choose_spec, mul_comm, map_mul (algebraMap _ _),
← mul_assoc, inv_mul_cancel₀ (seq_ne_zero K w₁ hB n), one_mul]

Result:
no goals