-- 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)))
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)ˣ)
          (⋯.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 : ℝ)
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)ˣ)
          (⋯.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
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)ˣ)
          (⋯.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‖
⊢ Eq (α := Submodule ℝ (logSpace K)) (Submodule.span ℝ (↑(unitLattice K) : Set (logSpace K))) ⊤
have refine₆ : 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)ˣ);
∀ (w : { w : InfinitePlace K // w ≠ w₀ }), ∑ x ∈ erase univ w, |v w x| < |v w w|
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)