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
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₀ }
⊢ LT.lt (α := ℝ) 0 (∑ x : { w : InfinitePlace K // w ≠ w₀ }, v w x)
have refine_2 : 0 <
  -(↑(mult.{u_1} (K := K) w₀) : ℝ) *
    Real.log
      ((w₀ : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(sorry.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: rw [sum_logEmbedding_component (exists_unit K w).choose]
-- 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 <
    -(↑(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))
have refine_2 : LT.lt (α := ℝ) (-(↑(mult.{u_1} (K := K) w₀) : ℝ)) 0
Tactic: refine mul_pos_of_neg_of_neg ?_ ((exists_unit K w).choose_spec _ w.prop.symm)
-- 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₀ }
⊢ LT.lt (α := ℝ) (-(↑(if IsReal.{u_1} (K := K) w₀ then 1 else 2) : ℝ)) 0
have pos : IsReal.{u_1} (K := K) w₀ → LT.lt (α := ℝ) (-(↑1 : ℝ)) 0
Tactic: split_ifs
-- 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₀ }
pos : IsReal.{u_1} (K := K) w₀ → LT.lt (α := ℝ) (-(↑1 : ℝ)) 0
⊢ LT.lt (α := ℝ) (-(↑(if IsReal.{u_1} (K := K) w₀ then 1 else 2) : ℝ)) 0
have neg : ¬IsReal.{u_1} (K := K) w₀ → LT.lt (α := ℝ) (-(↑2 : ℝ)) 0
Tactic: split_ifs
-- 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 x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
⊢ v w x < 0
have refine_1 : LT.lt (α := ℝ) 0 (↑(↑x : InfinitePlace K).mult : ℝ)
Tactic: refine mul_neg_of_pos_of_neg ?_ ((exists_unit K w).choose_spec x ?_)
-- 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 x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
refine_1 : LT.lt (α := ℝ) 0 (↑(↑x : InfinitePlace K).mult : ℝ)
⊢ v w x < 0
have refine_2 : (↑x : InfinitePlace K) ≠ (↑w : InfinitePlace K)
Tactic: refine mul_neg_of_pos_of_neg ?_ ((exists_unit K w).choose_spec x ?_)
-- 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 x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
⊢ LT.lt (α := ℝ) 0 (↑(if (↑x : InfinitePlace K).IsReal then 1 else 2) : ℝ)
have pos : (↑x : InfinitePlace K).IsReal → LT.lt (α := ℝ) 0 (↑1 : ℝ)
Tactic: split_ifs
-- 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 x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
pos : (↑x : InfinitePlace K).IsReal → LT.lt (α := ℝ) 0 (↑1 : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑(if (↑x : InfinitePlace K).IsReal then 1 else 2) : ℝ)
have neg : ¬(↑x : InfinitePlace K).IsReal → LT.lt (α := ℝ) 0 (↑2 : ℝ)
Tactic: split_ifs
-- 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: classical
  refine le_antisymm le_top ?_
  -- The standard basis
  let B := Pi.basisFun ℝ {w : InfinitePlace K // w ≠ w₀}
  -- The image by log_embedding of the family of units constructed above
  let v := fun w : { w : InfinitePlace K // w ≠ w₀ } ↦
    logEmbedding K (Additive.ofMul (exists_unit K w).choose)
  -- To prove the result, it is enough to prove that the family `v` is linearly independent
  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⟩
  rw [Basis.det_apply]
  -- We use a specific lemma to prove that this determinant is nonzero
  refine det_ne_zero_of_sum_col_lt_diag (fun w ↦ ?_)
  simp_rw [Real.norm_eq_abs, B, Basis.coePiBasisFun.toMatrix_eq_transpose, Matrix.transpose_apply]
  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]
  · refine add_pos_of_nonneg_of_pos ?_ ?_
    · rw [sub_nonneg]
      exact le_abs_self _
    · rw [sum_logEmbedding_component (exists_unit K w).choose]
      refine mul_pos_of_neg_of_neg ?_ ((exists_unit K w).choose_spec _ w.prop.symm)
      rw [mult]; split_ifs <;> norm_num
  · refine mul_neg_of_pos_of_neg ?_ ((exists_unit K w).choose_spec x ?_)
    · rw [mult]; split_ifs <;> norm_num
    · exact Subtype.ext_iff.not.mp (ne_of_mem_erase hx)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
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)))
refine₁ refine₂ : LE.le (α := Submodule ℝ (logSpace K)) ⊤ (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K)))
⊢ Eq (α := Submodule ℝ (logSpace K)) (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K))) ⊤
have refine₃ : let B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ };
let 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)ˣ)
        (sorry.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)ˣ);
Ne (α := ℝ) ((B.det : (a : { w : InfinitePlace K // w ≠ w₀ } → { w : InfinitePlace K // w ≠ w₀ } → ℝ) → ℝ) v : ℝ)
  (0 : ℝ)
Tactic: classical
  refine le_antisymm le_top ?_
  -- The standard basis
  let B := Pi.basisFun ℝ {w : InfinitePlace K // w ≠ w₀}
  -- The image by log_embedding of the family of units constructed above
  let v := fun w : { w : InfinitePlace K // w ≠ w₀ } ↦
    logEmbedding K (Additive.ofMul (exists_unit K w).choose)
  -- To prove the result, it is enough to prove that the family `v` is linearly independent
  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⟩
  rw [Basis.det_apply]
  -- We use a specific lemma to prove that this determinant is nonzero
  refine det_ne_zero_of_sum_col_lt_diag (fun w ↦ ?_)
  simp_rw [Real.norm_eq_abs, B, Basis.coePiBasisFun.toMatrix_eq_transpose, Matrix.transpose_apply]
  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]
  · refine add_pos_of_nonneg_of_pos ?_ ?_
    · rw [sub_nonneg]
      exact le_abs_self _
    · rw [sum_logEmbedding_component (exists_unit K w).choose]
      refine mul_pos_of_neg_of_neg ?_ ((exists_unit K w).choose_spec _ w.prop.symm)
      rw [mult]; split_ifs <;> norm_num
  · refine mul_neg_of_pos_of_neg ?_ ((exists_unit K w).choose_spec x ?_)
    · rw [mult]; split_ifs <;> norm_num
    · exact Subtype.ext_iff.not.mp (ne_of_mem_erase hx)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ DiscreteTopology.{u_1} ↥(unitLattice K)
have refine : IsOpen (X := ↥(unitLattice K)) {0}
Tactic: refine discreteTopology_of_isOpen_singleton_zero ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsOpen (X := ↥(unitLattice K)) {0}
have refine_1 : Membership.mem (γ := Filter ↥(unitLattice K)) (nhds 0) (Metric.closedBall 0 1)
Tactic: refine isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 : Membership.mem (γ := Filter ↥(unitLattice K)) (nhds 0) (Metric.closedBall 0 1)
⊢ IsOpen (X := ↥(unitLattice K)) {0}
have refine_2 : Set.Finite.{u_1} (α := ↥(unitLattice K)) (Metric.closedBall 0 1)
Tactic: refine isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Set.Finite.{u_1} (α := ↥(unitLattice K)) (Metric.closedBall 0 1)
have refine_2 : Set.Finite.{u_1} (α := logSpace K)
  (Set.image (α := ↥(unitLattice K))
    (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
    (Metric.closedBall 0 1))
Tactic: refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Set.Finite.{u_1} (α := logSpace K)
    (Set.image (α := ↥(unitLattice K))
      (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
      (Metric.closedBall 0 1))
have h : Set.image (α := ↥(unitLattice K))
    (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
    (Metric.closedBall 0 1) =
  (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1
Tactic: convert! unitLattice_inter_ball_finite K 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Set.image (α := ↥(unitLattice K))
      (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
      (Metric.closedBall 0 1) =
    (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1
have h : ∀ (x : logSpace K),
  Membership.mem (γ := Set (logSpace K))
      (Set.image (α := ↥(unitLattice K))
        (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
        (Metric.closedBall 0 1))
      x ↔
    x ∈ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : logSpace K
⊢ Membership.mem (γ := Set (logSpace K))
      (Set.image (α := ↥(unitLattice K))
        (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
        (Metric.closedBall 0 1))
      x ↔
    x ∈ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1
have h : Membership.mem (γ := Set (logSpace K))
    (Set.image (α := ↥(unitLattice K))
      (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
      (Metric.closedBall 0 1))
    x →
  x ∈ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1
Tactic: refine ⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ DiscreteTopology.{u_1} ↥(unitLattice K)
have refine : IsOpen (X := ↥(unitLattice K)) {0}
Tactic: classical
  refine discreteTopology_of_isOpen_singleton_zero ?_
  refine isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_
  · exact Metric.closedBall_mem_nhds _ (by simp)
  · refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)
    convert! unitLattice_inter_ball_finite K 1
    ext x
    refine ⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩
    rintro ⟨x, hx, rfl⟩
    exact ⟨Subtype.mem x, hx⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : IsOpen (X := ↥(unitLattice K)) {0}
⊢ DiscreteTopology.{u_1} ↥(unitLattice K)
have refine_1 : Membership.mem (γ := Filter ↥(unitLattice K)) (nhds 0) (Metric.closedBall 0 1)
Tactic: classical
  refine discreteTopology_of_isOpen_singleton_zero ?_
  refine isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_
  · exact Metric.closedBall_mem_nhds _ (by simp)
  · refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)
    convert! unitLattice_inter_ball_finite K 1
    ext x
    refine ⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩
    rintro ⟨x, hx, rfl⟩
    exact ⟨Subtype.mem x, hx⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : IsOpen (X := ↥(unitLattice K)) {0}
refine_1 : Membership.mem (γ := Filter ↥(unitLattice K)) (nhds 0) (Metric.closedBall 0 1)
⊢ DiscreteTopology.{u_1} ↥(unitLattice K)
have refine_2 : Set.Finite.{u_1} (α := ↥(unitLattice K)) (Metric.closedBall 0 1)
Tactic: classical
  refine discreteTopology_of_isOpen_singleton_zero ?_
  refine isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_
  · exact Metric.closedBall_mem_nhds _ (by simp)
  · refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)
    convert! unitLattice_inter_ball_finite K 1
    ext x
    refine ⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩
    rintro ⟨x, hx, rfl⟩
    exact ⟨Subtype.mem x, hx⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ finrank.{0, u_1} ℤ ↥(unitLattice K) = rank K
have rw : finrank.{0, u_1} ℤ ↥(unitLattice K) = finrank.{0, u_1} ℝ (logSpace K)
Tactic: rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : finrank.{0, u_1} ℤ ↥(unitLattice K) = finrank.{0, u_1} ℝ (logSpace K)
⊢ finrank.{0, u_1} ℤ ↥(unitLattice K) = rank K
have rw₁ : finrank.{0, u_1} ℝ (logSpace K) = finrank.{0, u_1} ℝ (logSpace K)
Tactic: rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ finrank.{0, u_1} ℤ ↥(unitLattice K) = rank K
have rw : finrank.{0, u_1} ℤ ↥(unitLattice K) = finrank.{0, u_1} ℝ (logSpace K)
Tactic: classical
  rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : finrank.{0, u_1} ℤ ↥(unitLattice K) = finrank.{0, u_1} ℝ (logSpace K)
⊢ finrank.{0, u_1} ℤ ↥(unitLattice K) = rank K
have rw₁ : finrank.{0, u_1} ℝ (logSpace K) = finrank.{0, u_1} ℝ (logSpace K)
Tactic: classical
  rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (torsion K)
    (MonoidHom.ker (M := Multiplicative (logSpace K))
      ((AddMonoidHom.toMultiplicativeRight :
          (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
        (logEmbedding K)))
have h : ∀ (x : (𝓞 K)ˣ),
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ)
      (MonoidHom.ker (M := Multiplicative (logSpace K))
        ((AddMonoidHom.toMultiplicativeRight :
            (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
          (logEmbedding K)))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ)
      (MonoidHom.ker (M := Multiplicative (logSpace K))
        ((AddMonoidHom.toMultiplicativeRight :
            (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
          (logEmbedding K)))
      x
have h : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
  Eq (α := Multiplicative (logSpace K))
    ((((AddMonoidHom.toMultiplicativeRight :
                (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
              (logEmbedding K) :
            (𝓞 K)ˣ →* Multiplicative (logSpace K)) :
          (a : (𝓞 K)ˣ) → Multiplicative (logSpace K))
        x :
      Multiplicative (logSpace K))
    (1 : Multiplicative (logSpace K))
Tactic: rw [MonoidHom.mem_ker, AddMonoidHom.toMultiplicativeRight_apply_apply, ofAdd_eq_one,
          ← logEmbedding_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
    Eq (α := Multiplicative (logSpace K))
      ((((AddMonoidHom.toMultiplicativeRight :
                  (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                (logEmbedding K) :
              (𝓞 K)ˣ →* Multiplicative (logSpace K)) :
            (a : (𝓞 K)ˣ) → Multiplicative (logSpace K))
          x :
        Multiplicative (logSpace K))
      (1 : Multiplicative (logSpace K))
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ)
      (MonoidHom.ker (M := Multiplicative (logSpace K))
        ((AddMonoidHom.toMultiplicativeRight :
            (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
          (logEmbedding K)))
      x
have h₁ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
  Eq (α := Multiplicative (logSpace K))
    ((Multiplicative.ofAdd : (a : logSpace K) → Multiplicative (logSpace K))
        ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
          logSpace K) :
      Multiplicative (logSpace K))
    (1 : Multiplicative (logSpace K))
Tactic: rw [MonoidHom.mem_ker, AddMonoidHom.toMultiplicativeRight_apply_apply, ofAdd_eq_one,
          ← logEmbedding_eq_zero_iff]