-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem unitLattice_span_eq_top :
    Submodule.span ℝ (unitLattice K : Set ({w : InfinitePlace K // w ≠ w₀} → ℝ)) = ⊤

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < |v w w| - v w w + ∑ x : { w // w ≠ w₀ }, v w x

Tactic:
refine add_pos_of_nonneg_of_pos ?_ ?_

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 ≤ |v w w| - v w w

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < ∑ x : { w // w ≠ w₀ }, v w x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Submodule.span ℝ ↑(unitLattice K) = ⊤

Tactic:
refine le_antisymm le_top ?_

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 ≤ |v w w| - v w w

Tactic:
rw [sub_nonneg]

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ v w w ≤ |v w w|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)

Tactic:
suffices B.det v ≠ 0 by
  rw [← isUnit_iff_ne_zero, ← is_basis_iff_det] at this
  rw [← this.2]
  refine  Submodule.span_monotone fun _ ⟨w, hw⟩ ↦ ⟨(exists_unit K w).choose, trivial, hw⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
⊢ B.det v ≠ 0

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑⋯.choose))

Tactic:
refine mul_pos_of_neg_of_neg ?_ ((exists_unit K w).choose_spec _ w.prop.symm)

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ -↑w₀.mult < 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
⊢ B.det v ≠ 0

Tactic:
rw [Basis.det_apply]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
⊢ (B.toMatrix v).det ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
this : LinearIndependent ℝ v ∧ Submodule.span ℝ (Set.range v) = ⊤
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)

Tactic:
rw [← this.2]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
this : LinearIndependent ℝ v ∧ Submodule.span ℝ (Set.range v) = ⊤
⊢ Submodule.span ℝ (Set.range v) ≤ Submodule.span ℝ ↑(unitLattice K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ v w x < 0

Tactic:
refine mul_neg_of_pos_of_neg ?_ ((exists_unit K w).choose_spec x ?_)

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ 0 < ↑(↑x).mult

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ ↑x ≠ ↑w

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < ∑ x : { w // w ≠ w₀ }, v w x

Tactic:
rw [sum_logEmbedding_component (exists_unit K w).choose]

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑⋯.choose))