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
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
this :
  Ne (α := ℝ) ((B.det : (a : { w : InfinitePlace K // w ≠ w₀ } → { w : InfinitePlace K // w ≠ w₀ } → ℝ) → ℝ) v : ℝ)
    (0 : ℝ)
⊢ LinearIndependent ℝ v ∧
    Eq (α := Submodule ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ)) (Submodule.span ℝ (Set.range v)) ⊤

Tactic:
rw [← isUnit_iff_ne_zero, ← Basis.is_basis_iff_det] at this

Premises used: isUnit_iff_ne_zero, Module.Basis.is_basis_iff_det
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
this :
  LinearIndependent ℝ v ∧
    Eq (α := Submodule ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ)) (Submodule.span ℝ (Set.range v)) ⊤
rw :
  LE.le (α := Submodule ℝ (logSpace K)) (Submodule.span ℝ (Set.range v))
    (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))
⊢ LE.le (α := Submodule ℝ (logSpace K)) ⊤ (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))

Tactic:
rw [← this.2]

Premises used: And.right
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
this :
  LinearIndependent ℝ v ∧
    Eq (α := Submodule ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ)) (Submodule.span ℝ (Set.range v)) ⊤
⊢ LE.le (α := Submodule ℝ (logSpace K)) (Submodule.span ℝ (Set.range v))
    (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))

Tactic:
Submodule.span_monotone fun _ ⟨w, hw⟩ ↦ ⟨(exists_unit K w).choose, trivial, hw⟩

Premises used: trivial, Set.Mem, _private.0.NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top.match_1, setOf, Membership.mem, SetLike.coe, NumberField.Units.unitLattice, And.intro, Exists.intro, Exists.choose, Submodule.span_monotone, Subtype.val, NumberField.Units.dirichletUnitTheorem.exists_unit
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
this :
  LinearIndependent ℝ v ∧
    Eq (α := Submodule ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ)) (Submodule.span ℝ (Set.range v)) ⊤
⊢ LE.le (α := Submodule ℝ (logSpace K)) (Submodule.span ℝ (Set.range v))
    (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))

Tactic:
refine Submodule.span_monotone fun _ ⟨w, hw⟩ ↦ ⟨(exists_unit K w).choose, trivial, hw⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
suffices :
  Ne (α := ℝ) ((B.det : (a : { w : InfinitePlace K // w ≠ w₀ } → { w : InfinitePlace K // w ≠ w₀ } → ℝ) → ℝ) v : ℝ)
    (0 : ℝ)
⊢ LE.le (α := Submodule ℝ (logSpace K)) ⊤ (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))

Tactic:
suffices B.det v ≠ 0 by
    rw [← isUnit_iff_ne_zero, ← Basis.is_basis_iff_det] at this
    rw [← this.2]
    refine Submodule.span_monotone fun _ ⟨w, hw⟩ ↦ ⟨(exists_unit K w).choose, trivial, hw⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
⊢ (B.toMatrix v).det ≠ 0

Tactic:
det_ne_zero_of_sum_col_lt_diag (fun w ↦ ?_)

Premises used: det_ne_zero_of_sum_col_lt_diag
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
refine : ∀ (w : { w : InfinitePlace K // w ≠ w₀ }), ∑ i ∈ erase univ w, ‖B.toMatrix v i w‖ < ‖B.toMatrix v w w‖
⊢ (B.toMatrix v).det ≠ 0

Tactic:
refine det_ne_zero_of_sum_col_lt_diag (fun w ↦ ?_)

Premises used: det_ne_zero_of_sum_col_lt_diag
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
simp_rw : ∑ x ∈ erase univ w, |v w x| < |v w w|
⊢ ∑ i ∈ erase univ w, ‖B.toMatrix v i w‖ < ‖B.toMatrix v w w‖

Tactic:
simp_rw [Real.norm_eq_abs, B, Basis.coePiBasisFun.toMatrix_eq_transpose, Matrix.transpose_apply]

Premises used: Module.Basis.coePiBasisFun.toMatrix_eq_transpose, Matrix.transpose_apply, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
rw : 0 < |v w w| - v w w + ∑ x : { w : InfinitePlace K // w ≠ w₀ }, v w x
rw₁ : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }) (hx : x ∈ erase univ w), v w x < 0
⊢ ∑ x ∈ erase univ w, |v w x| < |v w w|

Tactic:
rw [← sub_pos, sum_congr rfl (fun x hx ↦ abs_of_neg ?_), sum_neg_distrib, sub_neg_eq_add,
    sum_erase_eq_sub (mem_univ _), ← add_comm_sub]

Premises used: sub_pos, Finset.mem_univ, abs_of_neg, Finset.sum_erase_eq_sub, add_comm_sub, Finset.sum_neg_distrib, Finset.sum_congr, sub_neg_eq_add, rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ 0 < |v w w| - v w w + ∑ x : { w : InfinitePlace K // w ≠ w₀ }, v w x

Tactic:
add_pos_of_nonneg_of_pos ?_ ?_

Premises used: add_pos_of_nonneg_of_pos
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
refine_1 : 0 ≤ |v w w| - v w w
refine_2 : LT.lt (α := ℝ) 0 (∑ x : { w : InfinitePlace K // w ≠ w₀ }, v w x)
⊢ 0 < |v w w| - v w w + ∑ x : { w : InfinitePlace K // w ≠ w₀ }, v w x

Tactic:
refine add_pos_of_nonneg_of_pos ?_ ?_

Premises used: add_pos_of_nonneg_of_pos
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
refine_1 : v w w ≤ |v w w|
⊢ 0 ≤ |v w w| - v w w

Tactic:
rw [sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ v w w ≤ |v w w|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ v w w ≤ |v w w|

Tactic:
exact le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
refine_2 :
  0 <
    -(↑(mult.{u_1} (K := K) w₀) : ℝ) *
      Real.log
        ((w₀ : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
                    ∀ (w_1 : InfinitePlace K),
                      w_1 ≠ (↑w : InfinitePlace K) →
                        Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
                𝓞 K) :
            K))
⊢ LT.lt (α := ℝ) 0 (∑ x : { w : InfinitePlace K // w ≠ w₀ }, v w x)

Tactic:
rw [sum_logEmbedding_component (exists_unit K w).choose]

Premises used: NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, Exists.choose, Subtype.val, NumberField.Units.dirichletUnitTheorem.exists_unit
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ 0 <
    -(↑(mult.{u_1} (K := K) w₀) : ℝ) *
      Real.log
        ((w₀ : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
                    ∀ (w_1 : InfinitePlace K),
                      w_1 ≠ (↑w : InfinitePlace K) →
                        Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
                𝓞 K) :
            K))

Tactic:
mul_pos_of_neg_of_neg ?_ ((exists_unit K w).choose_spec _ w.prop.symm)

Premises used: Exists.choose_spec, Ne.symm, Subtype.prop, Subtype.val, mul_pos_of_neg_of_neg, NumberField.Units.dirichletUnitTheorem.exists_unit
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
refine_2 : LT.lt (α := ℝ) (-(↑(mult.{u_1} (K := K) w₀) : ℝ)) 0
⊢ 0 <
    -(↑(mult.{u_1} (K := K) w₀) : ℝ) *
      Real.log
        ((w₀ : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
                    ∀ (w_1 : InfinitePlace K),
                      w_1 ≠ (↑w : InfinitePlace K) →
                        Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
                𝓞 K) :
            K))

Tactic:
refine mul_pos_of_neg_of_neg ?_ ((exists_unit K w).choose_spec _ w.prop.symm)

Premises used: Exists.choose_spec, Ne.symm, Subtype.prop, Subtype.val, mul_pos_of_neg_of_neg, NumberField.Units.dirichletUnitTheorem.exists_unit
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
pos : IsReal.{u_1} (K := K) w₀ → LT.lt (α := ℝ) (-(↑1 : ℝ)) 0
neg : ¬IsReal.{u_1} (K := K) w₀ → LT.lt (α := ℝ) (-(↑2 : ℝ)) 0
⊢ LT.lt (α := ℝ) (-(↑(if IsReal.{u_1} (K := K) w₀ then 1 else 2) : ℝ)) 0

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
h : IsReal.{u_1} (K := K) w₀
⊢ LT.lt (α := ℝ) (-(↑1 : ℝ)) 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w : { w : InfinitePlace K // w ≠ w₀ }
h : ¬IsReal.{u_1} (K := K) w₀
⊢ LT.lt (α := ℝ) (-(↑2 : ℝ)) 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
⊢ v w x < 0

Tactic:
mul_neg_of_pos_of_neg ?_ ((exists_unit K w).choose_spec x ?_)

Premises used: Exists.choose_spec, Subtype.val, NumberField.Units.dirichletUnitTheorem.exists_unit, mul_neg_of_pos_of_neg
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
refine_1 : LT.lt (α := ℝ) 0 (↑(↑x : InfinitePlace K).mult : ℝ)
refine_2 : (↑x : InfinitePlace K) ≠ (↑w : InfinitePlace K)
⊢ v w x < 0

Tactic:
refine mul_neg_of_pos_of_neg ?_ ((exists_unit K w).choose_spec x ?_)

Premises used: Exists.choose_spec, Subtype.val, NumberField.Units.dirichletUnitTheorem.exists_unit, mul_neg_of_pos_of_neg