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

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 x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ 0 < ↑(if (↑x).IsReal then 1 else 2)

Tactic:
split_ifs <;> norm_num

Result:
no goals

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 x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ ↑x ≠ ↑w

Tactic:
exact Subtype.ext_iff_val.not.mp (ne_of_mem_erase hx)

Result:
no goals

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 x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ 0 < ↑(↑x).mult

Tactic:
rw [mult]

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 < ↑(if (↑x).IsReal then 1 else 2)

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 : B.det v ≠ 0
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)

Tactic:
rw [← isUnit_iff_ne_zero, ← is_basis_iff_det] at this

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 ℝ ↑(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₀ }
⊢ v w w ≤ |v w w|

Tactic:
exact le_abs_self _

Result:
no goals

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₀ }
⊢ -↑w₀.mult < 0

Tactic:
rw [mult]

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₀ }
⊢ -↑(if w₀.IsReal then 1 else 2) < 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.toMatrix v).det ≠ 0

Tactic:
refine det_ne_zero_of_sum_col_lt_diag (fun w => ?_)

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)
w : { w // w ≠ w₀ }
⊢ ∑ i ∈ univ.erase w, ‖B.toMatrix v i w‖ < ‖B.toMatrix 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)
this : LinearIndependent ℝ v ∧ Submodule.span ℝ (Set.range v) = ⊤
⊢ Submodule.span ℝ (Set.range v) ≤ Submodule.span ℝ ↑(unitLattice K)

Tactic:
refine  Submodule.span_monotone fun _ ⟨w, hw⟩ ↦ ⟨(exists_unit K w).choose, trivial, hw⟩

Result:
no goals

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

Tactic:
let B := Pi.basisFun ℝ {w : InfinitePlace K // w ≠ w₀}

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
⊢ ⊤ ≤ 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 : { w // w ≠ w₀ }
⊢ ∑ i ∈ univ.erase w, ‖B.toMatrix v i w‖ < ‖B.toMatrix v w w‖

Tactic:
simp_rw [Real.norm_eq_abs, B, Basis.coePiBasisFun.toMatrix_eq_transpose, Matrix.transpose_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)
w : { w // w ≠ w₀ }
⊢ ∑ x ∈ univ.erase w, |v w x| < |v w 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₀ }
⊢ -↑(if w₀.IsReal then 1 else 2) < 0

Tactic:
split_ifs <;> norm_num

Result:
no goals

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₀ }
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)

Tactic:
let v := fun w : { w : InfinitePlace K // w ≠ w₀ } =>
  logEmbedding K (Additive.ofMul (exists_unit K w).choose)

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)
⊢ ⊤ ≤ 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 : { w // w ≠ w₀ }
⊢ ∑ x ∈ univ.erase w, |v w x| < |v w w|

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

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)
w : { w // w ≠ w₀ }
⊢ 0 < |v w w| - v w w + ∑ x : { w // w ≠ w₀ }, v w x

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