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)
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
⊢ ∃ (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 : ℕ),
  n < m ∧ Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})
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) }))
-- 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 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
have hu : Associated (↑(seq K w₁ hB n) : 𝓞 K) (↑(seq K w₁ hB m) : 𝓞 K)
Tactic: have hu := Ideal.span_singleton_eq_span_singleton.mp 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 : ℕ
hnm : n < m
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})
hu : Associated (↑(seq K w₁ hB n) : 𝓞 K) (↑(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
have refine : ∀ (w : InfinitePlace K) (hw : w ≠ w₁),
  LT.lt (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    (1 : ℝ)
Tactic: refine ⟨hu.choose, fun w hw ↦ Real.log_neg (pos_at_place hu.choose 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)
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)})
hu : Associated (↑(seq K w₁ hB n) : 𝓞 K) (↑(seq K w₁ hB m) : 𝓞 K)
w : InfinitePlace K
hw : w ≠ w₁
⊢ Eq (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    ((w : (a : K) → ℝ)
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K)
          (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)) :
      ℝ)
have rw : Eq (α := ℝ)
  ((w : (a : K) → ℝ)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                hu) :
            𝓞 K) :
        K) :
    ℝ)
  ((w : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            ((↑(seq K w₁ hB n) : 𝓞 K) *
              (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦
                    (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K)) hu) :
                𝓞 K)) :
          K)
        (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)) :
    ℝ)
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]
-- 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 : ℕ
hnm : n < m
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})
hu : Associated (↑(seq K w₁ hB n) : 𝓞 K) (↑(seq K w₁ hB m) : 𝓞 K)
w : InfinitePlace K
hw : w ≠ w₁
rw :
  Eq (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    ((w : (a : K) → ℝ)
        (HMul.hMul (α := K) (β := K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              ((↑(seq K w₁ hB n) : 𝓞 K) *
                (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦
                      (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K)) hu) :
                  𝓞 K)) :
            K)
          (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)) :
      ℝ)
⊢ Eq (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    ((w : (a : K) → ℝ)
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K)
          (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)) :
      ℝ)
have rw₁ : Eq (α := ℝ)
  ((w : (a : K) → ℝ)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                hu) :
            𝓞 K) :
        K) :
    ℝ)
  ((w : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            ((↑(seq K w₁ hB n) : 𝓞 K) *
              (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦
                    (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K)) hu) :
                𝓞 K)) :
          K)) :
    ℝ)
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]
-- 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 : ℕ
hnm : n < m
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})
hu : Associated (↑(seq K w₁ hB n) : 𝓞 K) (↑(seq K w₁ hB m) : 𝓞 K)
w : InfinitePlace K
hw : w ≠ w₁
⊢ HMul.hMul (α := ℝ) (β := ℝ)
      ((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) : ℝ) <
    1
have rw : 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) : ℝ)
Tactic: rw [map_inv₀, mul_inv_lt_iff₀' (pos_iff.mpr (seq_ne_zero K w₁ hB n)), mul_one]
-- 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 : ℕ
hnm : n < m
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})
hu : Associated (↑(seq K w₁ hB n) : 𝓞 K) (↑(seq K w₁ hB m) : 𝓞 K)
w : InfinitePlace K
hw : w ≠ w₁
⊢ LT.lt (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    (1 : ℝ)
have _ : Eq (α := ℝ)
  ((w : (a : K) → ℝ)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                hu) :
            𝓞 K) :
        K) :
    ℝ)
  ((w : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K)
        (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)) :
    ℝ)
Tactic: calc
      _ = w (algebraMap (𝓞 K) K (seq K w₁ hB m) * (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹) := by
        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]
      _ = w (algebraMap (𝓞 K) K (seq K w₁ hB m)) * w (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹ :=
        map_mul _ _ _
      _ < 1 := by
        rw [map_inv₀, mul_inv_lt_iff₀' (pos_iff.mpr (seq_ne_zero K w₁ hB n)), mul_one]
        exact seq_decreasing K w₁ hB hnm 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 : ℕ
hnm : n < m
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})
hu : Associated (↑(seq K w₁ hB n) : 𝓞 K) (↑(seq K w₁ hB m) : 𝓞 K)
w : InfinitePlace K
hw : w ≠ w₁
_ :
  Eq (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    ((w : (a : K) → ℝ)
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : 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)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    (1 : ℝ)
have _₁ : HMul.hMul (α := ℝ) (β := ℝ) ((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) : ℝ) <
  1
Tactic: calc
      _ = w (algebraMap (𝓞 K) K (seq K w₁ hB m) * (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹) := by
        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]
      _ = w (algebraMap (𝓞 K) K (seq K w₁ hB m)) * w (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹ :=
        map_mul _ _ _
      _ < 1 := by
        rw [map_inv₀, mul_inv_lt_iff₀' (pos_iff.mpr (seq_ne_zero K w₁ hB n)), mul_one]
        exact seq_decreasing K w₁ hB hnm 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 : ℕ),
    n < m ∧ Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})
have refine : ∀ (n : ℕ),
  Membership.mem (γ := Set (Ideal (𝓞 K))) {I : Ideal (𝓞 K) | (Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) I ≤ B}
    (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)})
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)
-- 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 : ℕ
⊢ Membership.mem (γ := Set (Ideal (𝓞 K))) {I : Ideal (𝓞 K) | (Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) I ≤ B}
    (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)})
have rw : Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB n) : 𝓞 K)) ≤ B
Tactic: rw [Set.mem_setOf_eq, Ideal.absNorm_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Submodule ℝ (logSpace K)) (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K))) ⊤
have refine : LE.le (α := Submodule ℝ (logSpace K)) ⊤ (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))
Tactic: refine le_antisymm le_top ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
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 : ℝ)
⊢ LE.le (α := Submodule ℝ (logSpace K)) ⊤ (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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 ℝ (↑(unitLattice K) : Set (logSpace K)))
have rw : LE.le (α := Submodule ℝ (logSpace K)) (Submodule.span ℝ (Set.range v))
  (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))
Tactic: rw [← this.2]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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)ˣ)
⊢ LE.le (α := Submodule ℝ (logSpace K)) ⊤ (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))
have suffices : Ne (α := ℝ) ((B.det : (a : { w : InfinitePlace K // w ≠ w₀ } → { w : InfinitePlace K // w ≠ w₀ } → ℝ) → ℝ) v : ℝ)
  (0 : ℝ)
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⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
have refine : ∀ (w : { w : InfinitePlace K // w ≠ w₀ }), ∑ i ∈ erase univ w, ‖B.toMatrix v i w‖ < ‖B.toMatrix v w w‖
Tactic: refine det_ne_zero_of_sum_col_lt_diag (fun w ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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₀ }
⊢ ∑ i ∈ erase univ w, ‖B.toMatrix v i w‖ < ‖B.toMatrix v w w‖
have simp_rw : ∑ x ∈ erase univ w, |v w x| < |v w w|
Tactic: simp_rw [Real.norm_eq_abs, B, Basis.coePiBasisFun.toMatrix_eq_transpose, Matrix.transpose_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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₀ }
⊢ ∑ x ∈ erase univ w, |v w x| < |v w w|
have rw : 0 < |v w w| - v w w + ∑ x : { w : InfinitePlace K // w ≠ w₀ }, v w x
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
⊢ ∑ x ∈ erase univ w, |v w x| < |v w w|
have rw₁ : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }) (hx : x ∈ erase univ w), v w x < 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
have refine_1 : 0 ≤ |v w w| - v w w
Tactic: refine add_pos_of_nonneg_of_pos ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
⊢ 0 < |v w w| - v w w + ∑ x : { w : InfinitePlace K // w ≠ w₀ }, v w x
have refine_2 : LT.lt (α := ℝ) 0 (∑ x : { w : InfinitePlace K // w ≠ w₀ }, v w x)
Tactic: refine add_pos_of_nonneg_of_pos ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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
have refine_1 : v w w ≤ |v w w|
Tactic: rw [sub_nonneg]