-- 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)))
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‖
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)ˣ)
          (⋯.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|
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)ˣ)
          (⋯.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
refine₈ 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)ˣ)
          (⋯.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
⊢ Eq (α := 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)

Premises used: sub_pos, Finset.mem_univ, le_abs_self, abs_of_neg, NumberField.InfinitePlace.mult, le_antisymm, Finset.sum_erase_eq_sub, Module.Basis.coePiBasisFun.toMatrix_eq_transpose, add_pos_of_nonneg_of_pos, add_comm_sub, le_top, det_ne_zero_of_sum_col_lt_diag, Matrix.transpose_apply, Finset.sum_neg_distrib, sub_nonneg, Finset.sum_congr, Module.Basis.det_apply, sub_neg_eq_add, rfl, Real.norm_eq_abs