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)
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
⊢ 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

Premises used: Exists.choose_spec, NumberField.Units.dirichletUnitTheorem.seq_next, eq_or_lt_of_le, And.right, And.left, Nat.le_of_lt_succ, 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 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) : ℝ)
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) : ℝ)
⊢ 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:
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

Premises used: Exists.choose_spec, NumberField.Units.dirichletUnitTheorem.seq_next, eq_or_lt_of_le, And.right, And.left, Nat.le_of_lt_succ, 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)
contrapose! : ∀ (hB : B < 1), (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal) ≤ minkowskiBound K 1
⊢ 1 ≤ B

Tactic:
contrapose! hB
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : B < 1
⊢ (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal) ≤ minkowskiBound K 1

Tactic:
simp only [Nat.lt_one_iff.mp hB, CharP.cast_eq_zero, mul_zero, zero_le]

Premises used: CharP.cast_eq_zero, zero_le, MulZeroClass.mul_zero, Nat.lt_one_iff, Iff.mp
-- 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)
⊢ 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]
-- 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)
this : 1 ≤ B
⊢ Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB 0) : 𝓞 K)) ≤ B

Tactic:
simp only [ne_eq, seq, map_one, Int.natAbs_one, this]

Premises used: Int.natAbs_one, ne_eq, map_one, 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 : ℕ
succ : LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑(↑(seq K w₁ hB (n + 1)) : 𝓞 K) : K)| : ℚ) ((↑B : ℚ) : ℚ)
⊢ Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB (n + 1)) : 𝓞 K)) ≤ B

Tactic:
rw [← Nat.cast_le (α := ℚ), Nat.cast_natAbs, Int.cast_abs, Algebra.coe_norm_int]

Premises used: Int.cast_abs, Algebra.coe_norm_int, Nat.cast_natAbs, Nat.cast_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)
n : ℕ
⊢ LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑(↑(seq K w₁ hB (n + 1)) : 𝓞 K) : K)| : ℚ) ((↑B : ℚ) : ℚ)

Tactic:
(seq_next K w₁ hB (seq K w₁ hB n).prop).choose_spec.2.2

Premises used: Exists.choose_spec, NumberField.Units.dirichletUnitTheorem.seq_next, And.right, 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 : ℕ
⊢ LE.le (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) (↑(↑(seq K w₁ hB (n + 1)) : 𝓞 K) : K)| : ℚ) ((↑B : ℚ) : ℚ)

Tactic:
exact (seq_next K w₁ hB (seq K w₁ hB n).prop).choose_spec.2.2

Premises used: Exists.choose_spec, NumberField.Units.dirichletUnitTheorem.seq_next, And.right, 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 : ℕ
zero : Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB 0) : 𝓞 K)) ≤ B
succ : ∀ (n : ℕ), Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB (n + 1)) : 𝓞 K)) ≤ B
⊢ Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB n) : 𝓞 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

Premises used: Exists.choose_spec, Int.cast_abs, Int.natAbs_one, NumberField.Units.dirichletUnitTheorem.seq_next, Algebra.coe_norm_int, Nat.cast_natAbs, ne_eq, And.right, map_one, Subtype.prop, Nat.cast_le, 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
p : fun (B : ℕ) ↦ minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
| ∃ (B : ℕ), minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
p : ∀ (x : ℕ), minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑x : ENNReal)
| fun (B : ℕ) ↦ minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
x : ℕ
p : minkowskiBound K 1 < (↑x : ENNReal) * (↑(convexBodyLTFactor K) : ENNReal)
| minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑x : ENNReal)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
p : ∀ (x : ℕ), minkowskiBound K 1 < (↑x : ENNReal) * (↑(convexBodyLTFactor K) : ENNReal)
| ∃ (B : ℕ), minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)

Tactic:
congr; ext; rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
conv : ∃ (x : ℕ), minkowskiBound K 1 < (↑x : ENNReal) * (↑(convexBodyLTFactor K) : ENNReal)
⊢ ∃ (B : ℕ), minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)

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

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
⊢ ∃ (x : ℕ), minkowskiBound K 1 < (↑x : ENNReal) * (↑(convexBodyLTFactor K) : ENNReal)

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

Premises used: ENNReal.exists_nat_mul_gt, Iff.mpr, NumberField.mixedEmbedding.convexBodyLTFactor_ne_zero, ENNReal.coe_ne_zero, NumberField.mixedEmbedding.minkowskiBound_lt_top, OfNat.ofNat, ne_of_lt
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
⊢ ∃ (x : ℕ), minkowskiBound K 1 < (↑x : ENNReal) * (↑(convexBodyLTFactor K) : ENNReal)

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

Premises used: ENNReal.exists_nat_mul_gt, Iff.mpr, NumberField.mixedEmbedding.convexBodyLTFactor_ne_zero, ENNReal.coe_ne_zero, NumberField.mixedEmbedding.minkowskiBound_lt_top, OfNat.ofNat, ne_of_lt
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
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
⊢ ∃ (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))

Premises used: NumberField.mixedEmbedding.minkowskiBound, NumberField.mixedEmbedding.convexBodyLTFactor, OfNat.ofNat
-- 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)
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
rsuffices₁ :
  ∃ (n : ℕ) (m : ℕ),
    n < m ∧ 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) }))
-- 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 m : ℕ
hnm : n < m
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})
⊢ Associated (↑(seq K w₁ hB n) : 𝓞 K) (↑(seq K w₁ hB m) : 𝓞 K)

Tactic:
have hu := Ideal.span_singleton_eq_span_singleton.mp h
-- 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 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

Tactic:
⟨hu.choose, fun w hw ↦ Real.log_neg (pos_at_place hu.choose w) ?_⟩

Premises used: NumberField.Units.pos_at_place, Exists.intro, Exists.choose, Real.log_neg
-- 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 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)
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 : ℝ)
⊢ ∃ (u : (𝓞 K)ˣ),
    ∀ (w : InfinitePlace K),
      w ≠ w₁ → Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0

Tactic:
refine ⟨hu.choose, fun w hw ↦ Real.log_neg (pos_at_place hu.choose 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)
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₁
⊢ (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)) =
    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) : ℝ)

Tactic:
map_mul _ _ _

Premises used: map_mul
-- 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 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 :
  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) : ℝ)
⊢ 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:
rw [map_inv₀, mul_inv_lt_iff₀' (pos_iff.mpr (seq_ne_zero K w₁ hB n)), mul_one]

Premises used: Iff.mpr, NumberField.InfinitePlace.pos_iff, map_inv₀, NumberField.Units.dirichletUnitTheorem.seq_ne_zero, mul_inv_lt_iff₀', mul_one
-- 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 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) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)

Tactic:
seq_decreasing K w₁ hB hnm w hw

Premises used: NumberField.Units.dirichletUnitTheorem.seq_decreasing
-- 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 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) (↑(seq K w₁ hB m) : 𝓞 K) : K) : ℝ)
    ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K) : ℝ)

Tactic:
exact seq_decreasing K w₁ hB hnm w hw

Premises used: NumberField.Units.dirichletUnitTheorem.seq_decreasing
-- 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 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)) :
      ℝ)
_₁ :
  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
⊢ 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:
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

Premises used: HMul.hMul, Algebra.algebraMap, map_mul, Inv.inv, NumberField.RingOfIntegers, Subtype.val, DFunLike.coe, 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 : ℕ) (m : ℕ),
    n < m ∧ Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})

Tactic:
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)

Premises used: Set.Finite.exists_lt_map_eq_of_forall_mem, Ideal.finite_setOf_absNorm_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)
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)})
⊢ ∃ (n : ℕ) (m : ℕ),
    n < m ∧ Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 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)

Premises used: Set.Finite.exists_lt_map_eq_of_forall_mem, Ideal.finite_setOf_absNorm_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)
n : ℕ
rw : Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB n) : 𝓞 K)) ≤ B
⊢ Membership.mem (γ := Set (Ideal (𝓞 K))) {I : Ideal (𝓞 K) | (Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) I ≤ B}
    (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)})

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

Premises used: Set.mem_setOf_eq, Ideal.absNorm_span_singleton
-- 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 : ℕ
⊢ Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB n) : 𝓞 K)) ≤ B

Tactic:
seq_norm_le K w₁ hB n

Premises used: NumberField.Units.dirichletUnitTheorem.seq_norm_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)
n : ℕ
⊢ Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(seq K w₁ hB n) : 𝓞 K)) ≤ B

Tactic:
exact seq_norm_le K w₁ hB n

Premises used: NumberField.Units.dirichletUnitTheorem.seq_norm_le
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Submodule ℝ (logSpace K)) (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K))) ⊤

Tactic:
le_antisymm le_top ?_

Premises used: le_antisymm, le_top
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : LE.le (α := Submodule ℝ (logSpace K)) ⊤ (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))
⊢ Eq (α := Submodule ℝ (logSpace K)) (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K))) ⊤

Tactic:
refine le_antisymm le_top ?_

Premises used: le_antisymm, le_top